The certificate calculus

For the verification reader. Nine stops. Results dated to the one-week build campaign of July 2026 are marked as such; the campaign ledger keeps that record and never retro-edits. Work has continued daily since, and the book is where the current record accumulates.

1.The niche

Bound-propagation verifiers for neural networks are quick, they scale to networks people actually deploy, and the engineering in them is good. What they hand back is a verdict. There is no separate object you can carry to someone who does not trust the tool, so the verifier sits inside the trusted base, and it is large, floating-point, and revised often. SMT solvers do better on that axis, since a proof-producing solver hands back something a stranger can check, and the formats are general enough to cover a great many theories. Generality has a price in this corner of the map. The fragment that dominates control and safety certificates is piecewise-polynomial inequalities over polyhedral complexes, which is to say thousands of structurally identical local obligations glued by combinatorial bookkeeping. Bernstein Logic is a certificate language shaped for that fragment and not for much else.

One consequence follows from the shape. The producer may be any search process whatsoever: floating point, GPU kernels, a learned proposal network, a graduate student with a hunch. The checker never asks how a certificate was found. Being wrong costs the producer a rejected certificate and costs the reader nothing. The producer side is public in mtk, which carries a float proposing tier and an exact certifying tier, with accelerated kernels emitting witnesses rather than bare verdicts. Its agent-facing session surface has arrived.

A measurement, so the trade is not just a story. The complete NeurIPS 2025 neural model-checking suite is certified in full: all 634 hardware-verification tasks, across its three claim classes, where the best published single tool completes 554 and the union of every tool in that paper’s own comparison completes 617. The Experiments chapter of the book carries the tables, and the tables regenerate from committed receipts.

2.The layer stack, from this side

QTSL specifications (the top layer, L3) compile to verification-condition towers (the middle layer, L2) by generator application. Towers compile to Bernstein Logic (the base layer, L1) by symbolic instantiation. Two guarantees hold across that stack. Probabilistic reasoning never reaches L1, which sees exact rational arithmetic and nothing else. And a new L2 logic adds no new L1 rules, so the base calculus is audited once for every specification logic anyone builds above it.

3.BernCone, and the rest is gluing

To certify a polynomial inequality on a cell, write the polynomial in the Bernstein basis for that cell and test its coefficient tensor against a conic predicate; that test is the one rule the calculus calls BernCone. Exact rational arithmetic throughout. No semidefinite program, no floating point, no tolerance parameter. Set beside a sums-of-squares witness, which arrives as a positive semidefinite Gram matrix and inherits the numerics of the solver that produced it, the Bernstein test is coarser cell by cell and exactly checkable, and it refines by subdivision until either the margin appears or the certificate is pressing against a true boundary of the property.

Everything else in the catalogue glues local facts together: Farkas combinations, cut, equation elimination, case split over cell complexes, and the composition rules (interface promise, syzygy, small gain). The catalogue has grown well past the size it had at the end of the campaign, and the Rule Catalogue chapter of the book is the current list. Each rule carries its soundness lemma, and each lemma’s status is stated per rule rather than inherited from its neighbours. That discipline has earned its keep. During the campaign four rules were found unsound as staged and repaired, and one claimed admissibility was refuted by a kernel-checked countermodel.

4.Refutation runs on the same machinery

Counterexample search does not call an SMT oracle. The certificate machinery refutes in three ways, all of them using parts already in the trusted path.

Bernstein subdivision on the claim itself is a decision procedure for strict polynomial claims on boxes. The loop that certifies is the loop that refutes, and a violating cell corner is a point counterexample that anyone can check by evaluating a polynomial.

LP duality handles families. An infeasible certificate family carries a Farkas ray, and verifying that ray in exact rational arithmetic refutes the whole family at once.

The checker’s own refusals are localized. A refusal names the cell, the coefficient, and the exact value that failed, rather than reporting that something somewhere went wrong.

Because refutations arrive as regions and not only as points, repair is differentiable. The defect integral over a refused cell is, in Bernstein form, the mean of the same coefficient tensor the checker tests, so a learner can push on the whole region by gradient descent in floating point with nothing to trust. Verdicts are pronounced only by the exact rational re-check.

Where the dynamics are genuinely non-polynomial, this machinery does not pretend to decide. That regime belongs to delta-complete solvers and rigorous enclosure front ends, and the boundary is kept visible rather than blurred.

5.Read a certificate

A certificate is not a proof file. It arrives as ordinary rows in a signed, content-addressed geolog commit, on the same data plane that stores everything else, so there is no proof-file format to version and no side channel for proof bytes. (A binary bridge format served during the campaign while the data plane was being built, and was retired once certificates could be born as rows.)

The rows carry a hypernet, which is the shared wire and term structure; a sequent, which is the claim and the cells it ranges over; and a proof-term tree naming catalogue rules. Payloads carry only what the checker cannot cheaply recompute. Real certificates are small. The cartpole decrease certificate is 197 proof-term nodes, a few kilobytes of rows. The encoding offers a producer no way to smuggle in a conclusion the checker did not derive.

You can read fixtures today. They are byte-committed in qtsl-experiments beside receipts, mutant batteries, and the table generators, with one make target per section of the book’s Experiments chapter. One caveat, stated so that nobody loses an afternoon to it. That repository imports its trusted checkers from the companion qtsl repository — now public — rather than vendoring them, and a fresh clone’s default import address is the public repository, at a pinned revision it carries; two legacy checker binaries, due for retirement in favour of the standard checkers, still pin a pre-release revision, and the repository’s README states exactly which lanes build from a public clone as written. The whole reproduction spine is public, inspectable end to end, and every number in the Experiments chapter re-derives mechanically from the committed artefacts.

6.Three ways to check the same bytes

The same rows are consumed by three checkers that share no implementation and no compiler, so a defect in one has no particular reason to appear in the others. Each is, on its own terms, an answer to “why should I believe this?”

The fast path. geolog-alpha with the qtsl plugin computes the entailments of a geolog theory incrementally, as commits arrive: deriving consequences, surfacing violations as reported judgments, and gating admission on axioms marked enforced. Its numeric kernels use hand-written PTX inside XLA-compiled fragments on NVIDIA hardware and SIMD lanes elsewhere, all under one conformance discipline (kernels is public, and a lane may change cost, never verdicts). The fast path carries no mechanized soundness story, and it is nonetheless required to be sound in practice. For certificate species outside the Bernstein-Logic fragment, including hypernets, proof nodes, and claims carrying coefficient tensors, it is today the only checker there is, so a gap that fools it is a soundness failure of the assurance story rather than a lesser class of bug. Its correctness instruments are engineering-grade and not theorems: an exact reference floor that is always on, differential batteries on every acceleration lane, adversarial fooling campaigns, and rebuild-invariance checks in continuous integration.

The certified checker, qtslab. A standalone binary built around one target theorem, whose shape is this. Feed the binary the encoding of a QTSL conclusion followed by an arbitrary stream of bytes; if it prints ACCEPT, the conclusion is semantically true. The arbitrary-bytes clause does real work, since decode totality is part of the obligation and malformed input can only produce a refusal with a witness. The theorem is machine-checked in HOL4 and grounded, through the CakeML verified compiler, in the semantics of the Arm instruction set, so nothing in the producer stack, the database engine, or the operating environment needs to be trusted. It is expected to be the slow path, and horizontal scale is designed in: a checking obligation is designed to split into pinned shards, checked on separate machines and reassembled under a composition theorem, so “slow” means throughput you can buy rather than a wall. One measurement that exists today. The certified build has replayed the stored corpus of 4,105 verification conditions with 4,105 accepts, zero divergence from the fast-path twin, and a pooled median of 30 milliseconds per file on a single Arm core. Stop 7 states what the landed theorem covers and where it stops.

The Lean route. The same bytes, loaded into Lean, where the route's checker is defined once — consumed compiled (a native executable built by the Lean compiler) and, for small certificates, accepted by the kernel itself as a theorem via reflection. The rule lemmas live in a Lean development whose soundness theorem closes sorry-free at the standard axioms (propositional extensionality, choice, quotient soundness), with the axiom footprint printed rather than asserted. Checking by reflection is expected to be too slow at machine scale, and the point is to demonstrate that with measurements instead of asserting it. A prior measurement on the predecessor certificate format makes it concrete. A 43-million-node neural-network verification certificate, 1.24 GB as a binary, projects to roughly 7 GB of Lean source and about 66 million declarations, roughly a hundred times mathlib’s declaration count, and years of single-threaded elaboration. The experiment re-runs against the final byte format once the repositories freeze. None of this counts against Lean. Those soundness lemmas are load-bearing here. A kernel built for mathematics and a checker built for machine-scale certificates are different tools, and the measurement says so without anyone needing to argue.

7.The assurance edifice

The accountant’s question is not “is it verified” but “what exactly must I trust, and what is the smallest version of that?” The answer is layered, and the layers fail differently.

Trusted-core diet. Splitting the checker core from the proof development took the emitted-C closure from 3.58 million lines to 34,311, a factor of 104, with no external packages (campaign).

Verified compilation, in both directions. The first Lean-emitted C went through CompCert, 9 of 9 translation units, with output byte-identical to production. Independently, the machine-code route was proven on an existing verified checker first (cake_lpr), whose machine-code soundness theorem replayed from source at pinned revisions in 4 h 15 m on 32 cores, and the campaign’s own HOL4 and CakeML port followed as a real binary, bytes on stdin and verdict on stdout, with four named proof debts discharged at 17 of 17 receipts (campaign).

Decorrelation. An independent second kernel re-checks the same export. A three-path comparator cross-checks the compiled, interpreted, and replayed routes at a measured 15.2-fold margin over serial full replay, which is cheap enough to leave switched on.

Receipts. An acceptance can be emitted as an ed25519-signed verification receipt over content-addressed inputs, governed by an explicit trust-roots file. Path C, stop 5, has that side of the story.

What the composed theorem binds today. Decode totality of the wire format is proven, so any byte string either fails closed with a witness or yields a well-sorted structure. The composed soundness theorem is landed and ties an ACCEPT to semantic validity for the Bernstein-Logic fragment, the polynomial-certificate core; the certified build replays the stored corpus of 4,105 verification conditions with zero refusals at a pooled median of 30 milliseconds per file on one Arm core. The certificate schema has since grown System and Spec vocabulary, and complete system-level claims are checked today by the fast-path engine, at that route’s engineering-grade assurance; through the certified checker they are not yet, and a certificate that reaches for them there is refused loudly rather than accepted silently. For the certified route the shortfall is a completeness gap and not a soundness debt: full System-satisfies-Spec binding arrives when the wire format grows the remaining rule tags and the checker grows the matching arms.

Residual trust. Your chosen prover kernel (Lean or HOL4, and the routes are decorrelated), the soundness statement itself, and the hardware.

8.QTSL above it

QTSL, the Quantitative Temporal Specification Logic, is where probabilistic-temporal claims are stated: probability-bounded deadline reachability, invariance, until, Streett acceptance. Its proof theory unpacks a formula into verification-condition towers whose leaves are the polynomial obligations the calculus discharges.

Negation is handled by normal form and then polarity-directed rounding. Open literals close outward where over-approximation is sound and free, and inward by a producer-chosen rational epsilon where under-approximation is required. Forms with no sound target in this fragment are type errors with the reason named, which covers negated Streett (Rabin), negated bounded until, and probability upper bounds. The last of those is the stated successor fragment.

What has changed since the campaign is the presentation and its mechanization. The Specification Language is given as deduction rules over a formation judgment, in the metanotation tradition of Guy Steele, rather than as a BNF grammar; a formation judgment says which specifications are well formed and why, and the rules are then available to reason with. Its elaboration into the Semantic Universe carries machine-checked adequacy layer by layer. The rewrite layer ships eighteen rewrite rules mechanized twice over, statement for statement in Lean and in HOL4, and the four wrong-polarity siblings of those rules are refuted by machine-checked countermodels. The calculus knows what it must not simplify. The Specification Language, Rule Catalogue, and Semantic Universe chapters of the book are the account.

9.Exhibits

One paragraph per section of the book’s Experiments chapter, in the chapter’s own order; the book carries the tables, and the receipts live in qtsl-experiments.

What a certified experiment claims. The chapter reports what happens when the toolkit is pointed at benchmarks it does not own. Each campaign produces certified results: a concrete policy, controller, or ranking function together with a machine-checkable certificate that a stated quantitative claim holds. A result earns its row by improving on at least one axis — bound tightness, soundness level, or the cost of checking — while regressing on none that matters; where the coalition’s own result is weak or missing, it appears in the same tables at the same prominence.

How to read the tables. The conventions are genre features rather than footnotes. Rounding is directed, always in the claim-weakening direction, so a displayed number is never stronger than the certified one. Check time is the headline cost, reported separately from the much larger, freely sloppy cost of finding a certificate. Every wall-clock cell traces to a named machine in the repository’s receipts.

Warm-up: re-certifying a published table. A manually constructed supermartingale bound from the literature was refuted by exact recomputation and localized to a two-sided interval that the published value lies strictly outside. Re-certifying a published 17-row supermartingale table improved all 17 rows, and the accumulated corpus now runs to 28,569 certificates, re-verified under two checker generations with zero refusals. This line of work builds on the quantitative supermartingale certificate literature of Alessandro Abate, Mirco Giacobbe, and coauthors.

Gymnasium: first certified rows for a standard RL suite. Certified rows for Gymnasium include the first published exact value of the blackjack example of Sutton and Barto under optimal play, and exact optima for FrozenLake, whose registry comments turn out to be truncations of exact rationals. The registered “solved” threshold for Taxi is unsatisfiable: the true optimum lies below it. An entire certified policy catalogue, every optimal lookup table with its proof, was synthesized in 0.69 seconds of wall clock.

Hardware model checking: certificates where verdicts were. All 634 tasks of the NeurIPS 2025 neural model-checking suite are certified, across its three claim classes; the paper’s own comparison records 554 tasks for its strongest single tool and 617 for the union of every tool it compares. Timing is reported qualitatively, because the numbers move with every re-run: on every recorded row of the re-run sweep, whole checked production — synthesis, exact certification, and replay together — completes inside the published tool’s training wall.

Atari as a circuit: making the environment white-box. Atari titles compiled bit-exactly to and-inverter circuits, validated frame for frame against the reference emulator, carrying, so far as the coalition can determine, the first certified episode returns for any Atari game, including a machine-checked score of exactly 400 on Montezuma’s Revenge.

Process control: the semiconductor ladder. A fixed progression of eleven public fab models, from the Intel Mini-Fab through the seven SEMATECH MIMAC testbed fabs and the two SMT2020 scenario fabs to SMAT2022, the same scenario fabs extended with automated material handling, carrying the same claim species at every rung. For the Mini-Fab’s fluid model under named static-priority dispatch policies, with all residual scheduling freedom resolved adversarially, linear-Lyapunov drain certificates hold at release rates up to 95.9 of the 96 lots per week of fluid capacity, which is 99.90%, and the probe at 96 correctly fails because the load is genuinely at capacity; each certificate carries 819 obligations and checks in one to three milliseconds. On MIMAC set 7 the current result is an aggregated-cover certificate at 19.8% of nominal release. That is a floor, and the book displays it at full prominence because it is weak, with the refinement path priced.

The Lean route: how much Lean? The same sealed bytes every other checker consumes, loaded into Lean, where the route's checker is defined once — consumed compiled (a native executable built by the Lean compiler) and, for small certificates, by the kernel itself via reflection; measured rather than asserted. Across a fifteen-rung ladder of production certificates the compiled reflection route follows a power law of t ∝ B^3.58 in container bytes (r² = 0.989) and crosses a ten-minute budget near 28 KB, while the fast path is near-linear on the same ladder; the kernel evaluator proper exhausts a hundred-gigabyte machine on a certificate under a kilobyte. Small certificates are where the route earns its keep: full kernel verdicts tie the certificate semantics to a proof kernel scrutinized by a community that owes maitria nothing.

Reproduction. Every campaign ships its evidence in the experiments repository: certificates committed byte-for-byte, mutant batteries beside them, machine-readable receipts from which the chapter’s tables re-derive mechanically, and one make target per family. The trusted checkers are imported from the qtsl repository at pinned revisions — now public, and the default import address points there, with the one legacy-binary caveat stop 5 states; the spine itself is public and inspectable end to end.

Two claims of a different flavour live in the technical report on non-Zeno certification and variadic footprints (/TR_zeno_variadic.pdf). A real-time floor over every dispatch policy for the Mini-Fab model, 255N + 375 ticks to complete N lots for all N ≥ 4, is machine-checked in Lean, and a machine-free sibling bound of 255N + 371 holds at every N. Under a synthesized latest-safe unlock supervisor, every schedule of the closed composite reaches all-arrivals at exactly 626N counting steps against the open plant’s worst case of 638N − 12, a certified throughput-floor gain of +1.9% at the weekly lot count. The report states for each claim which direction is machine-checked and which is argued with executable witnesses, and this page defers to its grading.

Continue to: the logical framework · replication & authority · programme orientation.