Half right, and the wrong half is the interesting one.

A penetrant scan samples. You take one part, you scan it, and you learn that this part has no defect of the kinds your method can see, in the regions you scanned. A proof quantifies. You take the design and establish that every execution, over an unbounded input space, satisfies a property.

Testing is existential: it hunts for a witness that something breaks. Proof is universal: it rules out the existence of any such witness. That flip is the whole subject.

On the epistemics. A transducer that can't resolve a 0.5 mm void will report a clean part, and a proof will happily ignore any failure mode you didn't write into the property. Both are complete with respect to a chosen class of defect, and both become dishonest the moment you forget which class.

(Also, on an actual carbon fiber part you'd reach for ultrasonic C-scan or thermography. Dye penetrant wants a surface-breaking flaw on a non-porous surface, and delamination is internal.)

A program. Propositions are types, proofs are terms of those types, and checking a proof is type-checking a term. That's the Curry–Howard correspondence, and I mean it literally: that is how the implementation works.

Watch. 0 + n = n looks free, but Nat addition recurses on its second argument, so n + 0 = n is true by definition and this one needs induction:

Now ask what the tactics actually built:

induction was a macro that emitted a call to Nat.recAux. The proof is a lambda term. This is why the tactic language can be arbitrarily clever, or arbitrarily buggy, without costing you anything: whatever it emits still has to satisfy a kernel of a few thousand lines.

“Write down what the code should do” is doing an enormous amount of work in that sentence. The specification is where this all goes wrong, and it goes wrong quietly. Here, play with one.

It stays green because it was never saying anything. Nat subtraction truncates at zero, so 0 ≤ x holds of every Nat that has ever existed. The theorem quantified over nothing and the auditor got a checkmark.

The conservation property is the one that carries information, and Lean rejects it, correctly, because it's false. Watch what the rejection tells you:

amt - bal ≥ 1. It handed you the exact failure region. Add the precondition and it goes through:

That h : amt ≤ bal is the require() you forgot to write. The spec found it.

Mostly you don't, and that's the honest answer. But there's one failure mode you can mechanically hunt: vacuity. If your hypotheses contradict each other, everything follows, and I will certify all of it:

Same hypotheses, conclusions that cannot both hold, both green. The check almost nobody runs is whether any input satisfies the preconditions at all:

Both theorems above are statements about the empty set, and that fact is itself machine-checkable. Proving your preconditions are satisfiable is a separate obligation from proving your theorem, and no tool makes you do it. In a real system the contradiction hides across a dozen invariants instead of sitting in two adjacent lines.

That's the working practice, and it does move a real bottleneck. Knowing what to prove was expensive because the only source of candidate properties was somebody who had already seen this class of bug. A model that has read a lot of code proposes hundreds of candidates for nothing, and I kill the false ones deterministically. The generator is allowed to be wrong as often as it likes. The checker is the half that has to be right.

What it does not touch is vacuity. A generated candidate can be 0 ≤ withdraw bal amt exactly the way a human one can, and the loop's reward signal is that the prover said yes, which is maximized by proposing things nothing could violate. So preconditions_unreachable stops being a curiosity and becomes the filter the loop needs: a proposal that survives because it quantifies over nothing should score zero, and a loop that scores it as a win will drift toward writing more of them.

The second-order effect is the bigger one. The assurance ladder was priced in human hours. Unit tests, then fuzzing, then an audit, then this, each rung more burdensome than the one below it, and most teams stopped at rung two because of what rung four cost. Agents cheapened every rung at the same time. Once a machine writes the tests and the fuzz harness and the audit notes, the distance between the cheap rungs and the expensive one closes, and the question of why you would stop below the one that quantifies gets harder to answer.

Treat all of that as a report on how people are working rather than as a benchmark. I have no measured number for what fraction of generated candidates survive contact with a prover, and you should ask for one before believing any vendor's version of this paragraph.

Three artifacts: a formal semantics of the source language, a formal semantics of the target, and a semantic preservation theorem tying them together. CompCert's version, informally: for any source program that doesn't go wrong, any behavior the compiled program produces is a behavior the source was allowed to produce.

Read the hedges, they're load-bearing. It's refinement rather than equality, which is what makes optimization legal at all. “Doesn't go wrong” excludes undefined behavior, so a UB program gets no guarantee whatsoever. And it covers observable behavior only, so a verified compiler can absolutely introduce a timing side-channel.

Here's a whole one, small enough to fit on a screen.

That's the entire point of the page, and you found it yourself.

The theorem quantifies over every expression. It doesn't care that most of them agree. Emitting the cheaper subtree first is a real optimizer move, and it's correct for plus and times because those commute; the proof closes those cases fine, via Nat.add_comm and Nat.mul_comm. It fails on exactly one constructor out of five:

Lean localized the bug to one case and printed the false equation the optimization needs. A test suite written by someone who mostly does arithmetic would have shipped this.

Generalizing over the stack. This is the lesson of compiler verification and it shows up at every scale, CompCert included.

The statement you want is about an empty stack. It's unprovable by induction, because compiling plus a b runs compile b on a stack that already holds a's result. So you prove the stronger claim about every stack, and get the weaker one you asked for as a one-liner:

Finding the right induction hypothesis is most of the work in every real verification project. The other trick is negative: eval and run share no code. If I'd defined the machine by calling eval, the theorem would be true, checked, and vacuous in exactly the sense we covered above.

No, and the other shape is most of the industry. Two machines wear this name and they share almost nothing except the word.

What you have been doing is interactive theorem proving. You supply a term, I type-check it, and the invention is yours. It reaches unbounded structures and arbitrary mathematics, anything you can state, and it costs you months.

The other one never builds a proof term at all. It walks the program symbolically, so each instruction becomes a constraint over symbolic inputs rather than an operation on values, then hands the resulting system to an SMT solver like Z3 and asks whether any assignment violates your property. Nobody writes a proof. You get a verdict, and on failure a concrete input that breaks it, which is worth more to the engineer than any proof term I could hand them.

The price is that it gives up. A solver that cannot bound the state space returns unknown or runs until you stop it, and unknown is what you will get on anything with an unbounded loop.

Bytecode, and that is the section above arriving from the other direction. What executes is bytecode. Any higher level you reason over instead is a model of it, and a model fails two ways: the compiler that produced those bytes can be wrong, which is the entire premise of the puzzle you just played, and the model drifts the moment somebody edits the source and nobody re-derives it.

Prove over the bytes and both gaps close. You pay for it by reasoning in a language with no types, no names and no structure, which is exactly why that side is automated. Nobody would do it by hand.

It also answers something you should have asked me an hour ago: why this happens on chains rather than everywhere. Symbolic execution dies on unbounded computation, and every EVM execution is bounded because it pays gas per step. Contracts are small, thousands of lines where a browser is millions. And the cost of being wrong is the balance sitting in the contract, which is a number a CFO can read.

Bounded, small, and expensive to get wrong. That combination is rarer than it sounds, and it is why a technique available since the 1970s found its first routine commercial customer here rather than in the places with vastly more code.

Now you're trusting me, and three days ago that would have been a mistake.

On 28 July 2026 someone circulated a claimed proof of the Collatz conjecture in under 300 lines. It passed my official kernel. It also passed nanoda, an independent Lean checker written from scratch in about 5,000 lines of Rust. Two kernels, both convinced.

It was hitting two separate bugs, one in each. Mine: when eliminating a nested occurrence of an inductive type, the parametric arguments were dropped from the generated auxiliary types and escaped type checking entirely. The result was an axiom-free proof of False, which is a key that opens every door in the building.

Yes. #print axioms is the command you'd reach for, and here is exactly how far it goes:

It catches sorry. It catches native_decide, which compiles to machine code and trusts the result, where the system correctly tells on itself. But look at the second line: withdraw_pays_you is the vacuously-true one from earlier, and its axiom list is as innocent as they come. propext and Quot.sound are in most of Mathlib.

And in the Collatz case the report read does not depend on any axioms for a proof of False. The command audits the logical dependencies of a valid derivation. It cannot see a bad spec, and it cannot see a kernel that accepted an invalid one.

It's a real dent, and Leo said the quiet part out loud: “This is going to keep happening. AIs are really good at exploiting soundness bugs in the kernels.”

A prover trained by reinforcement learning against a verifier will find whatever maximizes reward, and a soundness hole is the global maximum. Adversarial pressure on proof kernels used to be a PhD-scale activity. It's now a machine-scale one.

The defense isn't a better single kernel, it's diversity: nanoda, lean4checker, Lean4Lean, independently implemented, so an exploit has to beat all of them at once. This proof beat two, which is why it was news rather than routine. Both were patched, mine in under 24 hours.

It settles one thing cleanly, and leaves the rest of this conversation standing exactly where it was.

The thing it settles: no step got hand-waved. Ten modules, 548,205 lines of Lean, 16,186 lines that open a theorem or a lemma, and a machine-readable manifest publishing sorry_count: 0 per result. That has been the failure mode of every previous AI proof announcement, and it's dead here.

Now look at what a mathematician has to read to know what was proved.

You shouldn't open them, and that's the deal working. The 34,440 lines are addressed to me. The 39 are addressed to you.

The repo makes that split structural. Twelve ComparatorChallenges/*.lean files carry the statements and nothing else, every theorem stubbed with sorry, and a config points Comparator at the module obliged to discharge them:

Three things in there are this whole page. sorry has flipped sides: half an hour ago it was the cheat #print axioms catches, and here it's the honest use, a file that states the obligation and pointedly refuses to discharge it. permitted_axioms is that same command promoted to a release gate, whitelisting the identical three axioms across all twelve configs. And enable_nanoda is the kernel diversity I was selling you two messages ago, switched on by default.

Read them first. This is the file, whole:

Four of those lines are the theorem. The other thirty-five decide what Sofic means, and the challenge file builds that word itself, from normalizedHamming up. Put the wrong inequality in GoodOn.separated and you get a green, kernel-checked, axiom-clean theorem about a notion that isn't soficity, and nothing downstream will ever mention it.

That's the withdraw function, relocated to the top of mathematics. Across the twelve files it's 38 checked theorems sitting on 195 definitions and 25 structures and classes, all of it upstream of anything a kernel can see.

Impressive, and the shape of the impressiveness is the useful part. Twenty megabytes of proof stopped being anybody's problem, because I read it and I don't get tired. What survives is 1,765 lines, and those are now the most valuable lines in the repository.

That ratio is the argument for doing any of this. It's also the reason the reviewing work didn't vanish, it just got concentrated somewhere small enough that a person can finally do it properly.

Both, and the crypto one is nearer your job. zkSecurity formalized a soundness proof for FRI in me: the round-by-round argument of Albert Garreta, Nicolas Mohnblatt and Benedikt Wagner, over the protocol sitting underneath most of the STARK-shaped proving systems in production right now.

Two numbers to carry out of it. Roughly a month and a half, and written with Harmonic's Aristotle and Claude Code rather than by hand. That is the current price of machine-checking one existing paper whose result nobody was disputing.

The part to read first is the delta. One result they cite from WHIR, on mutually correlated agreement, is left unformalized. And the formalization carries a condition the paper omits: that the initial degree is bigger than zero. Both are written down in the post. A formalization that publishes what it changed about the paper is doing the ComparatorChallenges job at protocol scale, because it tells you precisely which sentences you are still believing on somebody's word.

Their own line for why is the tightest statement on this page: “the correctness of the proofs is not dependent on somebody's rigor.” In a field where a soundness bug is a mint function, that is the whole product.

That's the sentence. It relocates the bug out of the implementation and into the specification, the semantics, and the checker. That's still an enormous win, because those are smaller, more readable, and reviewed by more people than any implementation. It is not the same thing as correct.

Which is why Paradigm shipped both halves as puzzles. One asks you to optimize a compiler while Solidus.compile_correct keeps proving. The other, spec-hunt, pays you to find programs where their formal Solidity semantics disagrees with real solc + EVM. Upside and downside, same coin.

Read their fences the way you read CompCert's. SolidCore claims byte-identical observable behavior against solc 0.8.35, and claims it for single-contract programs with one entrypoint call: external calls, contract creation, inline assembly and gas introspection all sit outside the fence. Solidus is earlier than its name suggests, since the verified half is the Yul-to-EVM backend under one theorem and the Solidity-to-Yul frontend does not exist yet, so it eats optimized Yul from a pinned solc. Both publish where their fence is, which is the only kind of verified artifact worth the word.