Why believe a checker

This page is for readers with no background in formal verification. It explains why a small program’s verdict can be worth more than a large system’s assurance, and what that verdict does not cover.

A claim you cannot audit

Suppose a system hands you a controller for a chemical plant, together with a claim. The temperature will stay below the stated limit, for every disturbance in the stated range, indefinitely. The claim is worth a great deal if it is true. How would you find out?

You could examine the system that produced it. In practice you cannot. The internals are enormous, the training data is not yours to inspect, and what the system “intends” is not a question you can settle by looking. Even with full access, studying the producer tells you about the producer. It tells you nothing about the controller.

You could test the controller. Testing finds real faults and you should do it. But testing can only sample; it cannot cover all possible cases (except in small finite domains, which are rare in industrial practice). A suite that passes tells you about the cases you tried, and the disturbance that matters may not be among them.

So the ordinary options run out early, which leaves a better question. What could evidence look like, when the thing producing it is neither trustworthy nor inspectable?

Checking is easier than finding

Mathematics has had an answer for a long time, and it is simpler than it sounds. Take the number 8633. Is it prime? Settling that takes work. Now suppose someone hands you 8633 = 89 × 97. One multiplication settles it. You do not need to know how the factors were found, whether the finder was clever or lucky, or whether the finder wishes you well.

The pattern turns up everywhere. A finished sudoku takes a minute to check, by reading each row, each column, and each box, no matter how long the solving took or who did it. Long division is checked by one multiplication and one comparison. In each case the work of finding an answer and the work of checking it come apart, and checking is the cheap side.

A certificate generalizes this. It is the worked solution, shipped together with the claim, arranged so that checking is mechanical rather than persuasive. A fixed procedure reads the claim and the certificate and reports accept or reject. Nothing in that procedure consults the reputation of whoever wrote the certificate.

The asymmetry is what makes the arrangement useful. Producing certificates may take search, learning, and any amount of machinery nobody can audit. Checking one does not. The powerful part of the system need not be trusted, and the trusted part need not be powerful.

What a checker is

A checker is a small program. It reads a certificate and re-derives the claim from it, one licensed step at a time, by rules simple enough that a person can read all of them.

Small is not an accident here; it is the design goal. In this project a deliberate diet took the checker core’s emitted-C closure, meaning the whole body of C that its build produces and depends on, from 3.58 million lines to 34,311. That is a quantity of code a determined team can read, argue about, and come to understand.

Compare the alternative. Trusting a producer is not a one-time cost. You pay it again on every output, and every retraining resets whatever you thought you had established. Once a certification logic and format are frozen, auditing its checker is a one-time cost, and it covers every certificate that checker can accept. The more general-purpose the checker, the more that cost can be spread out over many use-cases and application domains, which is a big part of why we obsess over generality.

Reading the code is not where the assurance stops. Each checking rule here carries a machine-checked soundness lemma, a proof that whenever the rule’s premises hold, its conclusion holds. Those proofs are checked in Lean, a proof assistant that admits no step it has not verified for itself; qtslab, the certified checker, has its own end-to-end theorem, described next, checked in HOL4.

The guarantee then goes one level lower. The qtslab checker’s end-to-end theorem is carried through the CakeML verified compiler down into the semantics of the Arm instruction set, so what is proved concerns the machine code that runs, not a source listing that resembles it. The composed theorem is landed and covers the Bernstein-Logic fragment, which is the polynomial-certificate core: claims that reduce to bounds on polynomials over a region; the certified build replays the project’s stored corpus of 4,105 verification conditions with zero refusals. Binding the full “this system satisfies this specification” statement arrives when the wire format grows the remaining rule tags and the checker grows the matching arms.

A certificate that reaches past the covered fragment is refused loudly, never accepted silently. That is the property that makes a partial guarantee usable rather than misleading.

Malformed input is not a way around any of this. Decode totality is proven: any string of bytes whatsoever either fails closed, with a witness naming what went wrong, or yields a well-sorted structure the checker can work on. There is no third outcome in which a corrupt file quietly becomes a valid one.

What a refusal looks like

A checker that could only say no would be a poor tool. Refusals here are specific. When a polynomial bound fails, the message names the cell, the coefficient, and the value that failed, which turns a rejection into a repair instruction.

This has teeth against existing work as well as new work. A bound published in the literature and constructed by hand was refuted by exact recomputation. The arithmetic runs on exact rational numbers, so no rounding error hides in a margin.

“But what if an AI discovers new mathematics?”

This is the objection people reach for, and it deserves an answer rather than a reassurance. If a system is cleverer than the people who wrote the checker, why should the checker’s rules keep up with it?

Because novelty lives in the proof object, not in the rules of inference. A checker does not recognize theorems and has no sense of what is familiar. It licenses steps. Soundness is a property of the checking rules, and those rules do not care whether the statement they are applied to is centuries old or was invented this morning. A proof kernel verifies mathematics it has never seen, for that reason.

So consider the alien proof. Brilliant, unprecedented, produced by something far cleverer than the checker’s authors. There are two cases. Either every step it takes is licensed by the rules, in which case it checks, and its conclusion holds for the same reason any checked conclusion holds. Or somewhere it takes a step the rules do not license, and there it is refused, with a witness pointing at the step.

Surprise is confined to the question of what gets proved. It never reaches the question of whether a checked proof holds.

One case remains. The new mathematics might arrive as a proposed new rule rather than as a new proof. Here rules are data: each one is a row carrying its own soundness lemma. For the fast-path engine, a new specification logic enters as new rows and no new engine code; the certified checker is the deliberate converse — it accepts a new rule family only once the matching proved code lands, so its coverage grows exactly as fast as its soundness proof does. Either way a new rule is a visible event. Someone proposes it, its lemma is on the table, and the trusted base changes where people can watch it change. It is not a quiet capability gain.

What you still have to trust

No arrangement removes trust altogether. This one moves it into four places small enough to name.

The statement. A certificate is only as meaningful as the property it certifies. “The temperature stays below the limit” and “the temperature stays below the limit whenever the sensor is working” are different claims, and the second can be certified while the plant burns. Specifications need reading. maitria writes them in QTSL, a language for saying, with quantities and over time, what a system must do, and a person still has to read the specification and agree that it says the right thing.

The model of the world. A specification is checked against a definition of the system it governs — the plant, its dynamics, what the model treats as possible — and that definition must also be correct, or trusted. Given enough data, candidate system definitions can be made to fight it out over the record, an adversarial tournament of hypotheses scored on how well each explains what was observed. Even then, a principal should want policies certified against a system definition more ambiguous than the data to date would warrant, because a capable policy is exactly the kind of thing that drives a system into regimes where data is sparse. So system definitions ought to be grounded in physical principles that people can understand and endorse. What makes this tractable is an old asymmetry: Occam’s razor genuinely works in science — simple explanations are unreasonably effective at predicting fundamental dynamics — while in engineering the best design, as opposed to the best explanation, commonly has billions of dynamic components and is unauditable. The division of labour follows: the human team audits the system definition, a far more manageable burden than auditing the policy. The Mini-Fab exhibit on the front page is the pattern in miniature. Looking at its Petri net and agreeing that it represents the situation is easy; looking at the hypernet that denotes the optimal policy — the toolkit’s dataflow form of it — and agreeing that it is optimal is very hard, and that is where the checker pays its rent.

The checker you run. You have to obtain the binary you believe you have, and run it on a machine you control. That is a supply-chain problem rather than a mathematical one, and proving theorems does not make it go away.

The hardware. A proof about instructions is worth nothing if the instructions that execute are not the ones proved about. Faulty silicon, a stray cosmic ray, and a compromised machine all sit outside every theorem on this site.

Diversity is the mitigation for the last two. Three checking routes exist here, and they share no implementation and no compiler: a certified binary, a fast incremental engine, and a Lean route running by reflection (compiled from kernel-evaluable definitions, with the kernel itself checking small certificates). A defect that fools one has no particular reason to fool the others.

The fast route runs inside geolog, a database whose tables hold logical consequences, together with the QTSL plugin. It has no mechanized soundness story, and that is deliberate. It is still required to be sound in practice. For certificate species outside the polynomial core it is at present the only checker there is, so a gap that fools it counts as a soundness failure of the assurance story, not as a licensed shortcut. What separates the routes is the size of the trusted base and the kind of assurance behind it, “mechanized with respect to the instruction set” on one side and “we tried hard to fool it and could not” on the other. Responsibility for being right is not divided between them.

Running two routes over one certificate does not add up to a proof. Disagreement between them is still a loud signal, and the cheapness of checking is what makes running all three affordable.

Where to go next

For the technical version of this page, the certificate calculus covers the same ground with the mathematics in place, and the book preview at /book.pdf develops it at length.

For something to check today, the front page lists current results, and the five toolkit repositories are public: kernels, mtk, qtsl-experiments, geolog-alpha, and qtsl.

For this page’s argument turned back on the project that wrote it, the colophon applies the same standard to the site itself: what is claimed, what is not, and how a reader would check the difference.

None of this asks you to believe the producer, and none of it asks you to believe this page. It asks you to run something and read what it says.