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.

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.

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.

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.