Verification was always the answer.
The candidates were the bottleneck.
Eight panels. From the asymmetry to the unlock. Scroll.
Mathematical proofs are hard to write.
Easy to check.
This is why formal methods have stayed niche for fifty years. The asymmetry has always been here. What changed is the cost of the candidate side: an LLM produces a million plausible annotations a minute. Whether they are right is a separate, mechanically-decidable question.
scroll to continue
Every milestone took an army of PhDs and years.
A quiet garden. The proofs are real, the artifacts beautiful, the price unaffordable for anyone outside aerospace, kernels, or eight-figure DeFi protocols.
- Lean / CoqCompCertVerified C compiler$5M11 yr
- Isabelle/HOLseL4Verified microkernel$25M12 yr
- SMT + expertsCertoraDeFi audits$50–500kper contract
- HOL4CakeMLVerified ML compiler$8M+8 yr
- DafnyIron FleetDistributed protocols$3M+4 yr
- F* / Low*Project EverestTLS stack$10M+ongoing
A million candidate annotations per minute.
LLMs are cheap, fast, plausible guessers. Hallucinations are a problem when their output is trusted. Not when their output is verified.
- • grey particle = proposed annotation
- • unbounded supply, unbounded variation
- • zero correctness guarantee at the source
Hallucinations die at the boundary.
The verifier is uninterested in plausibility. It only accepts what is true. About 80% pass. The 20% that fail were wrong — and nobody downstream sees them.
Each cell narrows the others.
Without composition, sudoku would be brute-force search. With it, every fill prunes its row, column, and 3×3 box. Verification works the same way — each verified annotation narrows the next.
Same shape. The codebase is the grid. AG-equation dependencies are the rows, columns, and boxes.
See the morph → /sudokuEach verified fact narrows the abstract state.
The narrowed state makes the next guess cheaper. The cheaper guesses narrow further. This is the composition multiplier — the reason the curve bends.
Three rules. One counterexamplethe team didn't know existed.
The lattice from Panel 6 is checked against each customer rule. PROVED rules light green. A REFUTED rule drops a counterexample trace.
Your codebase, reframed as a constellation.
Every lit node is a customer-authored property, compile-time-checked. Year 1: 30. Year 2: 80. Year 3: 200+. This is the asset. It is yours. No competitor has it.
This is the asset. It is your codebase. It is yours forever. No competitor has it.