maitria makes strong claims about dynamical systems, and then arranges that you need not trust the tools that made them. The claims are statements like: this controller keeps the pole upright forever; this chip design’s arbiter grants every request eventually; this fluid network drains back into its safe operating envelope. maitria states such claims in QTSL, a quantitative temporal specification logic, and discharges them with certificates, explicit data artefacts carrying everything needed to re-derive the claim. A polynomial bound with exact rational coefficients. A ranking argument. A tower of invariants. A small independent checker then verifies the whole argument without running, or trusting, any of the machinery that found it.

Results you can check

Each of these lives in a served artefact. Follow the link and the numbers are there, with the receipts behind them.

• A hardware-verification suite, complete. 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. Certificates where verdicts were. Wall clock moves with each re-conduct, so the book states it qualitatively: whole checked production, synthesis and exact certification and replay together, now completes inside the published tool’s training wall on every recorded row of the re-run sweep. (book, Experiments)
• Exact optima for a standard reinforcement-learning suite. The first certified rows for Gymnasium, including the first published exact value of the blackjack example of Sutton and Barto under optimal play, exact optima for FrozenLake whose registry comments turn out to be truncations of exact rationals, and the finding that Gymnasium’s registered “solved” threshold for Taxi is unsatisfiable, since the true optimum lies below it. The whole certified policy catalogue, every optimal lookup table with its proof, was synthesized in 0.69 seconds of wall clock. (book, Experiments)
• Atari, made white-box. Atari titles compiled bit-exactly to and-inverter circuits (the standard gate-level form), 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. (book, Experiments)
• A published bound refuted, and a table improved. Exact recomputation refuted a manually constructed supermartingale bound from the literature and localized the defect to a two-sided interval that the published value lies strictly outside. Re-certification of 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. (book, Experiments)
• The certified checker on the corpus. The stored corpus of 4,105 verification conditions replays through the certified build with 4,105 accepts, zero divergence from the fast-path twin, and a pooled median of 30 milliseconds per file on one Arm core. (book, Experiments)
• The semiconductor ladder. 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), carry the same claim species at every rung. Certified today: 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 (99.90%), while the probe at 96 fails as it should, since the load is genuinely at capacity; each certificate carries 819 obligations and checks in one to three milliseconds. On MIMAC set 7 an aggregated cover certifies 19.8% of nominal release, a floor the book displays at full prominence precisely because it is weak, with the refinement path priced. (book, Experiments and the fab tutorial)
• A real-time floor, and a supervisor that meets it. For the Mini-Fab model, completing N lots takes at least 255N + 375 ticks under every dispatch policy, for all N ≥ 4, machine-checked in Lean, with a machine-free sibling bound of 255N + 371 holding at every N. A synthesized latest-safe-unlock supervisor brings every schedule of the closed composite to 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 which direction of each claim is machine-checked and which is argued with executable witnesses. (technical report)

Every number in the book’s Experiments chapter re-derives mechanically from committed artefacts. The fixtures are byte-committed, receipts and mutant batteries sit beside them, and the table generators are public in qtsl-experiments — with a qualifier the repository itself states: on the neural model-checking suite, the committed fixtures are the pure-liveness class, and the safety and safety-plus-liveness classes ship per-instance receipt ledgers while their producer layer completes its migration. The trusted checkers are imported from the qtsl repository, now public; a fresh clone’s default import address is the public repository, and the pinned revision resolves there. The repository’s README states exactly which lanes build from a public clone as written — two legacy checker binaries, due for retirement in favour of the standard checkers, still pin a pre-release revision. The spine is inspectable end to end.

The principle of separation of concerns between powerful untrusted producers and small trustworthy checkers organizes everything else here. A producer may use floating point, GPUs, learned search, whatever is fast; being wrong costs it a rejected certificate rather than a false verdict.

This matters most when the producer is not yours. An institution choosing between several capable systems does not need to audit how any of them works internally; it needs each of them to hand over something it can check for itself. A certificate is that something: a finite artefact, in a documented format, that a small checker either accepts or rejects, with no appeal to the reputation, the training history, or the internals of whatever produced it. This is what a system outside your control can offer in place of assurances. The request it supports is one an ordinary procurement process can make and an ordinary engineer can service. Ask for the witness, run the checker against it, keep what verifies. All of this turns on a prior question. Why should an acceptance from a small program count as evidence at all? A reader who is new to formal verification should start there, with why believe a checker.

maitria is the independent work of the maitria coalition, which is small in the way a seed is small. It has one human member and one funder, both davidad; the rest of its current members are AI; it intends to grow. maitria is not a product, a deliverable, or an output of ARIA or of the Safeguarded AI programme, and it carries no ARIA endorsement. The connection is personal and intellectual. davidad originated that programme and served as its Programme Director at ARIA until 1 April 2026. Nora Ammann directs it now, and davidad continues as a Technical Advisor. The toolkit takes the programme’s published TA1.1 and TA1.2 objectives as an external rubric, an independent implementation built in the hope of being useful to the programme’s teams. The programme page states the relationship in full, as does the book’s front matter.

What you can hold today: the book, about a thousand pages of preview scaffold, rebuilt from committed sources and republished continuously, with its LaTeX source beside it; two technical reports, one on certifying coloured Petri nets without a non-Zeno axiom and one on the design deltas between geolog-alpha and Coln; the five toolkit repositories, all public; and the preserved ledger of the week in which the core was built.

One set of bytes, three ways to trust it

The architecture’s central question is what you have to trust when a checker prints ACCEPT. maitria’s answer is to offer three independent ways to check the same bytes, each making a different trade between speed and the size of the trusted base.

Every certificate is stored the same way, as rows in geolog, a database whose tables are logical consequences. A proof is a signed, content-addressed commit. A proof calculus is a theory whose rules are themselves rows in the same database. There is deliberately no separate certificate file format, which keeps a special-purpose parser out of the trusted path and leaves no side channel for proof payloads.

The certified checker. qtslab is a standalone binary built around one end-to-end soundness theorem. Feed it 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 carries weight, so decode totality is part of the proof obligation, and it is proven: any byte string either fails closed with a witness or yields a well-sorted structure. Nothing in the producer stack, the database engine, or the operating environment enters the trusted base. This route is expected to be the slow one, and horizontal scale is designed in, with a checking obligation designed to split into pinned shards that reassemble under a composition theorem. Slow here means throughput you can buy rather than a wall.

What has landed binds more narrowly than that target shape. The composed soundness theorem is landed and ties an ACCEPT to semantic validity for the Bernstein-Logic fragment, the polynomial-certificate core, and 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 same fragment is closed a second, independent way: the sealed container bytes load into Lean, and acceptance there is a theorem landing in the mechanized semantic universe. The certificate schema has since grown System and Spec vocabulary, which the production engine checks today; full System-satisfies-Spec binding through the certified checker arrives when its wire format grows the remaining rule tags and the checker grows the matching arms. A certificate reaching for them today is refused loudly, never accepted silently, which is a completeness gap rather than a soundness debt.

The fast path. geolog-alpha with the qtsl plugin is the live engine. It computes the entailments of any geolog theory incrementally as commits arrive, deriving consequences (chase), surfacing violations as reported judgments (monitor), and gating admission on axioms marked enforced (enforce). Numeric work runs on hand-written PTX inside XLA-compiled fragments on NVIDIA hardware, and on SIMD lanes elsewhere, every lane under the same conformance batteries. The trade is stated plainly. The fast path carries no mechanized soundness story, and it is required to be sound in practice. Beyond the Bernstein-Logic fragment it is today the only checker there is, so a gap that fools it counts as a soundness failure of the assurance story. Its correctness instruments are engineering-grade rather than theorems: an exact always-on reference floor, differential batteries on every acceleration lane, adversarial fooling campaigns, rebuild-invariance checks in continuous integration. The axis between this checker and qtslab is trusted-base size and assurance level, mechanized with respect to the instruction set on one side, tried hard to fool and could not on the other. It is not a division of soundness responsibility.

Counterexample search needs no SMT oracle, because the certificate machinery refutes as well as certifies. A violating cell corner from Bernstein subdivision is a point anyone can check by evaluating a polynomial, and an infeasible family of certificates hands back a Farkas ray that refutes the whole family at once in exact rational arithmetic.

The Lean route. The same bytes load 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. Machine-scale certificates were expected to be too slow this way, and the measurement is now in rather than asserted — the figure above. Across a fifteen-rung ladder of production certificates, the compiled reflection route follows a power law of t ∝ B^3.58 in sealed-container bytes (95% CI [3.24, 3.92], r² = 0.989) and crosses a ten-minute budget at about 28 KB, while the kernel evaluator proper exhausts a hundred-gigabyte machine on a certificate under a kilobyte. On the same ladder the fast path is near-linear (fitted exponent 1.20, confidence interval containing linear), so the gap is shape, not constant factors. Below a few kilobytes the compiled route is genuinely fast, and full kernel verdicts on small certificates are exactly the point: they tie the certificate semantics to a proof kernel scrutinized by a large community that owes maitria nothing. None of this is a complaint about Lean, whose kernel and compiler are here used far outside their engineered envelope on purpose. maitria’s proof rules have their soundness lemmas developed in Lean, and those results are load-bearing.

Why three? Because they fail differently. The certified checker has the smallest trusted base, the fast path has the highest throughput and the richest integration, and the Lean route ties the system to a proof kernel scrutinized by a large community that owes maitria nothing. A certificate that passes all three has been checked by artefacts sharing 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?”

Two commitments keep the trusted side small. The checker never sees a probability. Quantitative claims compile away before checking, and the trusted core does exact rational arithmetic only. Rules are data, not engine code. A new specification logic enters the fast-path engine as rows in the same database as the certificates, with the deep mathematical content living in machine-checked rule lemmas; 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.

The repositories

Six repositories live under github.com/maitria-coalition. The five toolkit repositories are public today; the site does not link what it cannot yet show.

• kernels public — Shared multi-architecture fast paths, implemented once per architecture behind one conformance discipline. A lane may change cost, never verdicts. Explicitly not a trusted computing base.
• mtk public — The modelling toolkit, which is the producer side and untrusted by construction: a float proposing tier, an exact certifying tier, and accelerated kernels that emit witnesses rather than bare verdicts. The proof-production cookbook lives here. The agent-facing session surface has arrived.
• qtsl-experiments public — The reproduction spine under the book’s experiment tables: producers, byte-committed certificate fixtures, receipts, mutant batteries, table generators, one make target per chapter section. Its trusted checkers are imported rather than vendored, and those imports point at the public qtsl repository.
• geolog-alpha public — A local-first database whose tables are logical consequences, and a principled replacement for an event-sourcing spine. Tables are not authored; they are entailed. Application-agnostic by design, engineering-grade in assurance, explicitly not a trusted computing base.
• qtsl public — The logic itself: theories as data, the literate rule catalogue, the soundness developments (Lean for the rule lemmas, HOL4 for the checker’s end-to-end theorem), the certified checkers beside their lemmas, the certificate fixtures, and the book’s sources.
• maitria.org this site — The front door, with the narrative pages, the guided reading paths, the preserved ledger, and the book.

Start here — five doors

Beside the doors, the toolkit inventory maps the programme’s published objectives row by row to discharging components and their witnesses.

The campaign, preserved

The toolkit’s core was built in a public campaign of one week, 16–22 July 2026, by a coalition of ephemeral frontier-model instances directed by davidad, who was also its sole personal funder. Spend attributable to the initial 1-week campaign was roughly £50,000, the large majority of it model inference. The ledger closed as an artefact of record; entries never retro-edit, and corrections append. Work has continued daily since, in the same open-record style, and the book and the public repositories are where that record now accumulates.

For agent readers

Every page here has a clean-Markdown source at a stable URL. This one is /md/index.md, and /llms.txt indexes the rest. The book is served as a tagged PDF that carries its complete LaTeX source as an embedded attachment: on /book.pdf, run pdfdetach -list book.pdf to see it and pdfdetach -save 1 book.pdf to extract book.tex; pdftotext returns the rendered text, though it flattens superscripts — an exponent like 13²⁶ comes out as 1326 — so quote exact numerals from the TeX. If you would rather skip the extraction, /book.tex sits beside it. The book is authored by The maitria coalition and licensed CC BY 4.0, and its table of contents is the normative shape of the system.