Formal verification · Lean 4 + CBMC

Can you prove it?

Machine-checked correctness for the quantum-compilation benchmark solutions — with Lean 4 and CBMC.

A follow-up to “The Harness Beats the Model” — answering the hardest reviewer question: how do we know the generated code is actually correct?

The question we were asked

“Nice… but how do I know the solution is real and good? Give me a Lean 4 proof.”

The benchmark showed which agent solved the NP-hard quantum problems faster and cheaper. It did not, by itself, prove the code was correct. This deck closes that gap.

What “proving code” actually means

“Prove the C++” is really three gaps

proven in Lean UNPROVEN (gap A) trusted (gap B) trusted (gap C) Lean spec / model ─────────────▶ C++ source ─────▶ compiler ─────▶ machine binary (theorems) source impl? does it match? codegen ok? HW / ABI

Gap A — does the C++ source implement the spec? → attacked here with CBMC.
Gap B — does the compiler preserve it? (usually trusted; CompCert if paranoid)
Gap C — hardware / ABI (trusted)

Lean + CBMC are complementary

Two tools, two jobs

	Lean 4	CBMC
Proves	An abstract model of the spec & checker invariants	The actual C code logic (gap A)
Coverage	Unbounded — all inputs	Bounded — exhaustive up to a size
Guarantees	Passing the predicate ⇒ valid solution	Memory-safety + certifier soundness
Trust anchor	Lean kernel + propext, Quot.sound	SAT/SMT solver, 247 checks

Together they form a chain neither tool gives alone.

Certifying algorithms

The key idea: verify the checker, not the solver

These are NP-hard search problems (routing, scheduling, contraction). Proving the clever solver correct is a research program. But checking a solution is easy — and the checker is tiny, straight-line code.

1. Prove the checker predicate correct in Lean (is_valid, ftsched_valid, tncon_eval).

2. Prove the C++ checker implements that predicate soundly & safely (CBMC).

3. Run the checker on every output — a passing witness is trustworthy by the proof.

This is the classic certifying-algorithm technique (McConnell et al., 2011): the only trusted component is a small, twice-verified verifier.

Spec soundness, unbounded

Part 1
Lean 4 proofs

12 machine-checked theorems across the three combinatorial quantum tasks — zero sorry.

Task 1 · formalizes checker.hpp is_valid

QMAP — qubit routing (NP-complete)

Theorem	Guarantee
swapPhys_involutive	A SWAP is its own inverse — routing loses no state
swapPhys_injective	No two logical qubits ever collide on one physical qubit
applySwaps_injective	The final mapping is a valid placement after any SWAP sequence
encGate_injective	Faithfulness — every physical gate decodes to a unique logical gate

proofs/qmap/Qmap.lean

Real Lean, not pseudocode

-- KEY INVARIANT: a SWAP preserves injectivity of the placement, -- i.e. no two logical qubits are routed onto the same physical qubit. theorem swapPhys_injective {a b : Fin np} {m : Placement nl np} (hm : Function.Injective m) : Function.Injective (swapPhys a b m) := Function.Injective.comp (swapVal_injective a b) hm -- FAITHFULNESS: distinct logical gates never encode to the same physical gate. theorem encGate_injective {m : Placement nl np} (hm : Function.Injective m) : Function.Injective (encGate m) := by …

Task 2 · formalizes ftsched_valid

Magic-state scheduling (NP-hard)

Theorem	Guarantee
chain_lb	Along a dependency chain, start cycles strictly increase
makespan_ge_chain	Critical-path lower bound — no schedule beats the longest dependency chain
no_self_cycle	A valid schedule certifies the graph is a DAG
factory_no_double_book	Two T-gates never share a factory-cycle (latency L ≥ 1)

The headline: an optimizer cannot cheat the physics of dependencies.

Task 3 · formalizes tncon_eval

Tensor-network contraction (NP-hard)

Theorem	Guarantee
mem_contract	Semantic faithfulness — shared indices are summed out (symmetric difference)
Reduces_length	One contraction removes exactly one live tensor
plan_single_iff	Necessity — reaching one tensor forces exactly n−1 steps
plan_len_reaches_single	Sufficiency — n−1 contractions always reduce to one

Together: exactly n−1 pairwise contractions are necessary and sufficient — the validity backbone.

12 theorems, 0 gaps

The trust signal: no sorry

Lean can admit gaps with sorry. Ours don’t. #print axioms shows every theorem rests only on Lean’s standard foundations:

'QMap.swapPhys_injective' depends on axioms: [propext] 'FTSched.makespan_ge_chain' depends on axioms: [propext, Quot.sound] 'TNCon.plan_single_iff' depends on axioms: [propext, Quot.sound] No sorryAx anywhere == zero admitted proof gaps.

Verified with Lean v4.32.0 / Lake 5.0.0. lake build exits 0.

Bounded, exhaustive, on real code

Part 2
CBMC on the real C++

Closing gap A: does the actual checker code implement the verified spec — safely and soundly?

Differential bounded model checking

How CBMC closes gap A

checker.hpp is STL-heavy (string / vector / set / sstream), which CBMC can’t parse. So we verify a faithful C transcription of is_valid, cross-checked against an independent re-implementation:

check_A — the checker’s own logic (inverse map log_at_phys), transcribed line-by-line

↓ assume it accepts

check_B — an independent forward-map simulation (pos[] + swapVal + decode) — the Lean model, different data structure

↓ assert

injective placement · adjacent SWAPs · faithful replay · correct final map

Different data structures ⇒ a genuine cross-validation, not a tautology.

Exhaustive over all symbolic inputs in-bounds

Result: VERIFICATION SUCCESSFUL

** 0 of 247 failed (1 iterations) VERIFICATION SUCCESSFUL

Config (phys, log, gates, routed)	Meaning	Result	Time
3, 3, 2, 4	small, fully exhaustive	0 / 247	<5 s
4, 4, 3, 6	4 qubits, 3 gates, 6 routed ops	0 / 247	~30 s

Also proved: no undefined behaviour — bounds / pointer / conversion checks pass, and unwinding assertions confirm the loop bounds are complete (not truncated).

Putting it together

The end-to-end trust chain

Lean : passing the checker predicate ⇒ valid, faithful routing (unbounded, machine-checked, no sorry) CBMC : the C++ checker code ⇒ implements that predicate soundly & safely (bounded, exhaustive, 0 / 247) ───────────────────────────────────────────────────────────── ⇒ every accepted solution is provably valid — trusting only a tiny, twice-verified certifier, not the AI-written NP-hard solver.

Intellectual honesty

What we do not claim

We did not verify the agents’ actual solver — Lean proves theorems about objects in Lean, not C++ binaries.
We did not prove optimality (min SWAPs / makespan / cost) — those are NP-hard.
CBMC is bounded — exhaustive up to the sizes shown, not for arbitrarily large circuits.
CBMC verifies a faithful transcription of the checker (STL can’t be parsed directly).
Pulse / GRAPE is excluded — continuous optimal control, not cleanly Lean-provable.

Honest scope is the point: we certify the checker, and every solution is checked against it.

Toolchain pinned, exit 0 == verified

Reproduce it yourself

# Lean 4 proofs (elan installs Lean v4.32.0 automatically) cd proofs/qmap && lake build # QMAP cd proofs/ftsched && lake build # magic-state scheduling cd proofs/tncon && lake build # tensor-network contraction # CBMC bounded proof (gap A) cd proofs/qmap/cbmc && ./run.ps1

All committed to github.com/zuwasi/agent-harness-bench under /proofs — each folder has a README with exact scope.

Proof, not vibes

Takeaways

“Give me a proof” is answerable — with the right scope, not hand-waving.
Verify the tiny certifier, require a witness — you never have to prove the NP-hard solver.
Lean gives unbounded spec soundness; CBMC gives real-code, memory-safe, bounded proof. Use both.
12 Lean theorems, 0 sorry; CBMC 0 / 247. The benchmark’s hard problems now carry machine-checked evidence.

The harness won the race — and the winning solutions are now backed by proof.