# The certificate calculus (path A)

For the verification reader. Nine stops. Results dated to the one-week
build campaign of July 2026 are marked as such; the
[campaign ledger](/md/campaign.md) keeps that record and never
retro-edits. Work has continued daily since, and the [book](/book.pdf)
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](https://github.com/maitria-coalition/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](/book.pdf) 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](https://github.com/maitria-coalition/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](https://github.com/maitria-coalition/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](https://github.com/maitria-coalition/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: $\mathsf{P}_{\ge p}$-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 $\varepsilon$ 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](/book.pdf) are the account.

## 9. Exhibits

One paragraph per section of the book's *Experiments* chapter, in the
chapter's own order; the [book](/book.pdf) carries the tables, and the
receipts live in
[qtsl-experiments](https://github.com/maitria-coalition/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 \propto B^{3.58}$ in container bytes ($r^2 = 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](/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 \ge 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.