George Agapov
Technical architect and leader · Andorra

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.

George Agapov, portrait on the coast at Étretat
Étretat, France

NOW

2026
o1Labs

Technical 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.

Yak Software

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.

2026agent-cageRun AI coding agents unattended on your own servers without giving the code they execute access to all of your credentials. The system separates the agent, executor and privileged components using ordinary Unix security boundaries.Public release 1 October.2026Molt PetitA research paper, in draft. A consensus protocol simple enough to explain in a minute, with deterministic fast finality — and a thorough treatment of what goes wrong with keys in practice. A rotated key, a stolen key and a key briefly in the wrong hands are three different events; the protocol handles each gracefully. Its safety is a machine-checked theorem.2021 –Mina protocolFive years of protocol engineering at o1Labs: re-architecting networking, introducing automated cluster-scale release testing, and later taking on broader technical leadership.2019 – 21StakerBridgeChief architect and technical lead for a token bridge across Algorand, Ethereum and Tezos, built around a custom DoS-resilient version of the usual cross-chain swap protocol.2019 – 20Pont.eeCo-founder of a small SaaS startup, and its project manager rather than its engineer: product definition, planning and delivery to launch.2016 – 18Cardano SLLed the team that implemented Cardano SL from inception through its mainnet launch. I was responsible for most of the development, quality and delivery across the ledger, consensus and networking work.

CODE

most days

I 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 →