maitria start here · programme orientation

Programme orientation

For the reader arriving from the Safeguarded AI programme side, holding the thesis and the technical-area structure. Five stops. The first is the reason this page exists.

1.What the relationship is, and what it is not

maitria is the independent work of the maitria coalition. It is not a product of ARIA, not a deliverable or official output of the Safeguarded AI programme, and not ARIA-funded. It carries no endorsement from either, and it speaks for its authors and for no one else.

The connection is personal and intellectual. David “davidad” Dalrymple originated the Safeguarded AI programme and served as its Programme Director at ARIA until 1 April 2026. The programme is now directed by Nora Ammann, with davidad continuing as a Technical Advisor. He also directs this coalition and funds it personally. That overlap is why the page states the relationship plainly rather than leaving it to inference.

What the programme supplies to this work is a rubric. The toolkit takes TA1.1’s and TA1.2’s published objectives as the standard it measures itself against, because those objectives were written down in public, in advance, by people thinking carefully about what such a toolkit would have to do. maitria is an independent implementation against that standard, built in the hope of being useful to the programme’s teams. The point of borrowing someone else’s rubric is that you cannot move the bar once the results are in.

One boundary is kept deliberately, and the book states it in its front matter. maitria builds on nothing ARIA-funded that its creators have not themselves made public. What it does build on, gratefully, is public work by others:

2.The thesis, instantiated

The programme’s thesis document sketches its verification story in a footnote. Establish quantitative safety bounds by Noetherian induction over a finite partition of the state space, refining obligations down to compact pieces, each discharged by a primitive quantitative bounding certificate. The target property shape is a bounded conditional probability with parameters.

This toolkit is that footnote made structural. QTSL states the quantitative temporal property. Judgment unpacking, inside QTSL’s own proof theory, turns a specification into a tower of verification conditions, so the partition and the induction structure become explicit data rather than an implementer’s private plan. Tower assembly composes per-region obligations with composition rules (small-gain, syzygy) that are themselves certificate nodes. Bernstein Logic discharges each compact obligation by exact-rational reasoning over Bernstein coefficients on polyhedral cells.

One narrowing, named as a narrowing. In the thesis’s picture a verified checker checks probabilistic claims. Here probability compiles away above the checker. Supermartingale and occupation arguments live in the certificate calculus, and the bytes that reach the trusted kernel carry exact rational arithmetic and nothing else. The checker you are asked to audit is small, discrete, and free of floating point.

3.The technical-area map

TA1.1, representation requirements. The campaign-era answer was that geolog’s design is requirements-first, with the meta-schema (theories as delta rows against one fixed homoiconic schema) as the representational core. That remains true and is no longer the whole answer. The book’s chapter The Semantic Universe is the representation story with the mechanization attached, a single universe of semantics into which the model-type catalogue’s formers include with machine-checked adequacy statements. The formers covered are ordinary, partial, delay, stochastic, and random differential equations, jump-diffusions, Markov chains in both time styles, Markov decision processes, Markov automata, and bags of interchangeable units. Several of the stochastic ones are connected down to a martingale-problem floor, with the remaining gap named in the module rather than papered over. Open hypernets include into the same universe as a single machine-checked lax double functor, strictness on the identity-carrying locus proved as a theorem rather than assumed.

TA1.2, the backend. The objective map preserves the campaign’s day-six assessment against TA1.2’s own quoted objectives. Read it as a dated snapshot rather than a status page. The current account is the book, whose table of contents is the normative shape of the system, together with the repositories: kernels, mtk, qtsl-experiments, and geolog-alpha are public today, and so is the qtsl repository. For the flavour of what the backend produces, the book’s Experiments chapter certifies all 634 tasks of the NeurIPS 2025 neural model-checking suite, 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.

TA2’s deductive end (TA2 is the programme’s oracle-and-agent area). This toolkit builds the deductive terminus of the oracle story, namely the certificates a producer must emit for its claims to be checkable by someone who does not trust it. Producer-side search may be heuristic, learned, or lucky. The checker does not care, and that indifference is the interface.

4.The campaign, and what came after

The toolkit’s core was built in a public one-week campaign, 16 to 22 July 2026, by a coalition of ephemeral frontier-model instances. The campaign ledger is the primary record of that week, one entry per day, receipts and refusals included. It closed as an artefact of record and has not been retro-edited since; corrections append. Work has continued daily in the same open-record style, and the record now accumulates in the book and in the public repositories.

5.How to audit us

Every load-bearing claim on this site is one of three kinds, and the pages are written so you can tell which.

Machine-checked claims state the theorem or the checker verdict, name the exact artefact, and name the prover. Rule-level soundness lemmas and the adequacy statements are developed in Lean. The certified checker qtslab has its end-to-end theorem developed in HOL4 and grounded, through the CakeML verified compiler, in the semantics of the Arm instruction set. What has landed binds narrower than the target shape: the composed 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 — and full System-satisfies-Spec binding arrives when the wire format grows the remaining rule tags and checker arms. A certificate reaching for those today is refused loudly, never accepted silently. The five toolkit repositories are public, the book and two technical reports are served here, and each statement names the artefact and the invocation, so a description is a check you can run.

Measured claims come with a recipe, nulls included. The reproduction spine under the book’s Experiments chapter is public in qtsl-experiments: byte-committed fixtures, receipts, mutant batteries beside the positive controls, table generators, one make target per chapter section. Every number in that chapter re-derives mechanically from committed artefacts. The trusted checkers are imported rather than vendored, from the companion qtsl repository — now public; a fresh clone’s default import address is the public repository, and the pinned revision resolves there. The spine is inspectable end to end today.

Asserted claims are design intent and judgment, kept as such and never dressed as the other two.

The audit trail is layered because the layers fail differently. The certified checker has the smallest trusted base and is the slow path by design. The fast path, geolog-alpha with the qtsl plugin, carries no mechanized soundness story and is nonetheless required to be sound in practice; beyond the Bernstein-Logic fragment it is the only checker there is today, so a gap that fools it counts as a soundness failure of the assurance story and is treated as one. Its instruments are engineering-grade rather than theorems, an exact always-on reference floor, differential batteries on every acceleration lane, adversarial fooling campaigns, and rebuild-invariance checks in continuous integration. The axis between the two is trusted-base size and assurance level, mechanized with respect to the instruction set against tried hard to fool it and could not, rather than a division of soundness responsibility. A third route loads the same bytes into Lean, whose once-kernel-checked reader accepts them (in the kernel itself for small certificates), which ties the system to a kernel scrutinized by a community that owes this project nothing. Verification receipts are signed and stored content-addressed, so a verdict is something you can re-check rather than something you were told. No single tool is trusted alone, and the sceptical reader can start at machine code, for the fragment the composed theorem covers.

Refusals belong in the audit too. The Experiments chapter records a published, manually constructed supermartingale bound refuted by exact recomputation, localized to a two-sided interval that the published value lies strictly outside.

Continue to: the certificate calculus · the logical framework · replication & authority.