Theorem Proving

A machine-checked proof that a property holds for all inputs, not just the ones a test happened to exercise. Where contract & refinement types ask the compiler to discharge obligations automatically, theorem proving has a human write the proof and a checker verify it — the strongest oracle in the catalog, at the cost of the most human effort of any sensor here.

The distinction from model checking is the proof strategy: model checking exhausts a finite state space; theorem proving constructs a general argument that holds for all inputs, bounded or not. The distinction from statically checked invariants is the automation: Dafny and Liquid Haskell try to discharge obligations without human guidance; Coq, Lean, and Isabelle require the human to write the proof script, and the checker verifies each step. The human is the prover; the machine is the auditor.

In practice

You do not hand a proof assistant a finished proof. You steer it a step at a time, and after each step it prints where you have got to: the thing still to be proved, and the facts you are allowed to use in proving it. That display is the reading.

1 subgoal
a : nat
l : list nat
IHl : rev (rev l) = l
============================
rev (rev l ++ [a]) = a :: l

Below the line is the goal — what is still unproved. Above it is everything currently known.

The notation is ML-family, and four pieces carry it:

• rev l — the list l, reversed.
• l ++ k — the lists l and k joined end to end.
• [a] — the one-element list containing just a.
• a :: l — the list l with a added to the front.

So the hypotheses say: a is a number, l is a list of numbers, and IHl — the induction hypothesis — that reversing l twice already gives back l. And the goal says: reversing (l reversed, with a on the end) should give l with a on the front.

That is the standard proof that reversing a list twice returns the original, stopped where it always stops. The known fact is about rev (rev l). The goal is about rev applied to a list with something appended to its end — a shape nothing above the line mentions — so there is no way to get from one to the other. The human has to see that gap, break off, and prove the missing fact about appending separately.

Unlike a test failure, the verdict is not “this case broke” but “this step of the argument is missing.” The fix is almost always a lemma the human forgot to state, or an induction hypothesis applied at the wrong type. The checker is never wrong about whether a step closes; it is only silent about which step to try next.

Response playbook

When a proof goal fails to close:

1. Read the goal and the hypotheses. The gap between them is the missing step. The checker prints exactly what it knows and what it needs; the human’s job is to see the bridge.
2. Try the obvious induction first. Most failed goals are missing an induction hypothesis applied at a stronger type than the human stated.
3. If the goal is unprovable, the spec is wrong. A goal that cannot close after sustained effort is evidence the property is false, not that the prover is weak. Extract the counter-example and treat it as a failing test.
4. If the goal is provable but the proof is too long, state lemmas. A proof script that sprawls is a sign the argument is missing structure; lemmas are how proofs get smaller.

How it gets gamed

The checker cannot be gamed, but the proof can be degraded:

• admit and sorry. Every proof assistant has an escape hatch that discharges any goal with “trust me.” A proof that compiles with admit in it is not a proof; it is a claim. The count of admits is the meta-signal.
• Axioms that shouldn’t be axioms. Declaring a property as an axiom discharges it without proof. An axiom that is actually a theorem is a proof obligation the author skipped.
• Proofs of the wrong property. The spec is written by the same mind that writes the code, so a proof of a trivial restatement of the implementation is a proof that protects nothing. The spec’s strength is the meta-signal: does the proven property say what the system needs to be true, or does it say what the code already does?
• Verification off the merge path. A proof that runs nightly or on demand, rather than on every merge, is a proof nobody is waiting for.

The meta-signal is admit count and axiom inventory. A proof with zero admits and no unproven axioms is a proof; a proof with either is a claim wearing a proof’s clothes.

What it cannot detect

Theorem proving cannot detect that the spec matches the system’s actual requirements. A proof of forall n, n + 0 = n is a valid proof of a trivial property; the checker is satisfied, the system is unprotected. The gap between “the property holds” and “the property is the one the business needs” is exactly what business invariants measure from the other direction.

Theorem proving also cannot detect properties of the runtime environment that the proof target abstracts away. A proof that the algorithm is correct does not prove the allocator won’t return NULL, the network won’t drop the message, or the operator won’t misconfigure the deploy. Those belong to runtime invariants and observability events.

Related sensors

References

Publications

• seL4: Formal Verification of an OS Kernel — Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood · 2009 · case study · SOSP 2009
• Formal verification of a realistic compiler — Xavier Leroy · 2009 · case study · Communications of the ACM 52(7)
• Certified Programming with Dependent Types — Adam Chlipala · 2013 · argument

Tooling

• CoqProof assistant for constructive mathematics
• LeanTheorem prover and programming language
• Isabelle/HOLGeneric proof assistant
• Frama-C WPWeakest-precondition calculus plugin for C verification