I build software where correctness matters, and I lead the teams that build it.
I've spent more than a decade building distributed systems, protocols and other software where mistakes can be expensive. My work has ranged from writing the implementation to architecture and the technical leadership of several engineering teams.
Today I'm Technical Architect at o1Labs, through Yak Software, and I also build my own products and research through Yak. Recently I've been spending a lot of time on what AI changes about software engineering, particularly when the result still needs strong guarantees.

NOW
2026Technical Architect. o1Labs is a client of Yak Software. Through that engagement I work on the technical architecture of o1Labs products and projects, and consult on execution and delivery across several engineering teams.
Earlier, I spent five years working directly on Mina, including a re-architecture of its networking layer and the automated, cluster-scale stress testing used for core releases.
Founder. Yak Software is my independent engineering and research company in Andorra. It is where I develop my own products and research: Diane, agent-cage and Molt Petit. On top of Molt Petit I am designing a financial integrity layer — records that stay correct even when the systems around them are compromised.
yak.ad →SELECTED WORK
all work →A few things I've built or led that still explain how I work today.
CODE
most daysI still write code on the systems I'm responsible for. Recent work has included Rust, Go, Kotlin, OCaml and Lean 4, plus a long tail I would have to look up.
I move between implementation, architecture and technical leadership rather than treating them as separate jobs.
WHAT I'M THINKING ABOUT
Engineering when the code is generated
AI has made implementation dramatically faster. It also makes it easy to produce plausible code without understanding every failure mode.
I've therefore been moving more of my attention to what surrounds the implementation: writing down the properties that matter, isolating components so that mistakes stay local, and using checks that are independent of whoever produced the code — and that fail differently from one another, so a disagreement shows up rather than being averaged away.
A lot of my recent work, including agent-cage, was built this way.
Formal methods at AI speed
Formal verification has always had an economics problem: for most software, writing and maintaining proofs costs too much.
I think agents may change that. I've been using them to help construct proofs and iterate on formal specifications, while the trusted checker remains small and deterministic.
Molt Petit is my first substantial experiment in this direction. The thesis, at Yak →
The AI insider
Companies are about to run AI agents inside their own infrastructure: wide access, machine speed, and motives that are not fully legible and can be altered from outside. We learned, more or less, how to hire people without fearing them. With AI insiders that is still open.
The question I'm working on: how do you keep a company's most important records correct, and private, when something inside — with access to every server — may be wrong or turned?
Ledger, at Yak →