yak.
yak.ad/research

Proof-driven development

George Agapov · Yak Software

I think AI agents change the economics of formal verification.

Not enough to prove everything or replace tests. But enough that, for some software, properties that used to be too expensive to prove can become part of normal development.

I've been experimenting with this at Yak. Molt Petit is the first substantial result.

thesis · first substantial example: Molt Petit · more work intended

Why now

Formal verification is attractive when a failure cannot be repaired after the fact. The problem has usually been cost: specifying properties, constructing proofs, and keeping them working as the implementation changes.

Agents make a surprising amount of that work cheaper. They are useful for proof search, following type errors, finding intermediate lemmas and repairing proofs after changes. The important part is that the final result is still accepted or rejected by a small deterministic checker, not by the model.

For selected properties, I now think this workflow is practical:

Two ways to build software

Test a few behaviours — or prove them all.

conventional
Works for what you test.
Finds bugs. Not their absence.
requirements
implementation
testssample behaviour
release
the behaviours someone thought to test
proof-driven
Prove what must always be true.
Stronger guarantees. Fewer surprises.
requirements
formal propertieswhat it must never do
implementation
+ proof searchlargely by agents
checked artifactthe theorem is about this
every behaviour, by proof

Two ways to build software

Conventional development tests a few behaviours. Proof-driven development proves them all.

conventional
Build, test what you thought of, then release.
requirements
implementation
testssample behaviour
release
the behaviours someone thought to test
proof-driven
State what must never happen, prove it, and get a checked artifact.
requirements
formal propertieswhat it must never do
implementation + proof searchlargely by agents
checked artifactthe theorem is about this
every behaviour, by proof

Tests remain better for many things: behaviour, integration, regressions and performance. Proofs become interesting when there is a compact property that must not be violated.

I also want the theorem connected as directly as possible to the executable code. A proof about a separate model is much less interesting if the production implementation can diverge from it.

Molt Petit

Molt Petit is the first substantial system I've built this way.

The validator is written in Rust and imported into Lean 4, where I prove its light-client safety. The proof development is about fifteen thousand lines of Lean, and much of the proof search and iteration was done with agents.

The same validator source also instantiates the recursive-proof circuit, reducing the number of independently maintained descriptions of the protocol.

The paper and artifact →

Next

The next test is the Ledger layer on top of Molt Petit: accounts, authorization rules, shards and committed state.

It is a harder problem than consensus, and that is partly why I want to try it.

I'm also interested in the practical question behind all of this: how much formal verification can become ordinary engineering when agents do much of the mechanical work?

I don't know the answer yet. Molt Petit gave me enough evidence to keep going.