# maitria.org — the Mathematical Assurance and Interaction Toolkit for Reliable Intelligent Agents > maitria makes strong claims about dynamical systems and then arranges that > you need not trust the tools that made them. Claims are expressed in QTSL, > a quantitative temporal specification logic whose polynomial-certificate > core is Bernstein Logic, and discharged by certificates stored as ordinary > rows in geolog, a local-first database whose tables are logical > consequences. The organizing principle is powerful untrusted producers, > small trustworthy checkers. One set of certificate bytes is checkable three > independent ways: qtslab, the certified checker, whose soundness proof is > machine-checked in HOL4 and grounded through the CakeML verified compiler > in the Arm instruction set, and whose landed composed theorem covers the > Bernstein-Logic fragment (certified arms for the System/Spec rule family > are the remaining assembly); > geolog-alpha with the qtsl plugin, the fast path, which carries no > mechanized soundness story, is required to be sound in practice, and is > today the only checker for certificate species beyond that fragment; and a > Lean reflection route. maitria is the independent work of the maitria > coalition. It is not a product, deliverable, or output of ARIA or of the > Safeguarded AI programme, carries no ARIA endorsement, and takes that > programme's published TA1.1 and TA1.2 objectives as an external rubric. > Served today: a ~1,000-page book preview scaffold with its LaTeX source, > two technical reports, and the five public toolkit repositories. Agent readers are first-class here. Every page has a clean-Markdown source at a stable URL, listed below. Open decisions are stated as open; nothing is invented to fill one. Where a component is not yet public, the site says so plainly and does not link it. ## Pages - [Home](/md/index.md): the lede, results with links to the artefacts that state them, the programme relationship, the trichotomy of checking routes, the two trusted-side commitments, the toolkit repositories, and the five doors. - [Why believe a checker](/md/trust.md): the page for readers with no formal- methods background; why checking is easier than finding, what a certificate and a checker are, why novel mathematics does not break a proof kernel, and what still has to be trusted after an acceptance. - [Programme orientation](/md/programme.md): the relationship to the Safeguarded AI programme stated in full, the published objectives read as an external rubric, and the build mapped onto them. - [The certificate calculus](/md/certificates.md): Bernstein Logic, reading a certificate as rows in a signed geolog commit, running and auditing the checkers, refutation as a first-class outcome, and QTSL above the core. - [The logical framework](/md/framework.md): geolog on its own terms — theories, instances, the chase, the meta-schema, ground formats, tensors, and QTSL as a hosted theory rather than engine code. - [Replication & authority](/md/sync.md): merge-free replication over a signed commit DAG, equivocation detected from content addressing alone, and the capability layer built to converge with Keyhive. - [Toolkit inventory](/md/toolkit.md): the programme's published objectives quoted and mapped row by row to discharging components and witnesses. - [Campaign ledger](/md/campaign.md): 16–22 July 2026, day by day, preserved as an artefact of record; entries never retro-edit, corrections append. - [How this was built](/md/colophon.md): the build team plainly — a coalition of ephemeral frontier-model instances directed by David "davidad" Dalrymple, the spend, and the trust story. ## The book - [/book.pdf](/book.pdf): the book, a ~1,000-page preview scaffold, rebuilt from committed sources and republished continuously. Authored by "The maitria coalition", licensed CC BY 4.0. Its table of contents is the normative shape of the system: Executive Summary; Experiments; a Geolog part (Quick Start, Tutorial, Reference Manual, Diagrams as Data: S-Complexes); a QTSL part (Quick Start; Tutorial: Producing Proofs with MTK; The Semantic Universe; Hypernets: Primitive Functions; Hypernets: Markov Kernels; Systems: Mathematical Models; Systems: Composition Patterns; Specification Language; Rule Catalogue; Partial Completeness); an MTK part (Tutorial: A Re-entrant Semiconductor Fab; Implementation Pearls; Cookbook for Agents); and an appendix listing the Lean statements cited in the book, regenerated from the Lean trees at each build. The PDF is tagged and carries its complete LaTeX source as an embedded attachment: `pdfdetach -list book.pdf` shows it, `pdfdetach -save 1 book.pdf` extracts `book.tex`; `pdftotext` returns the rendered text but flattens superscripts (`13^26` comes out `1326`) — quote exact numerals from the TeX. - [/book.tex](/book.tex): the LaTeX source, deployed beside the PDF, always. If you are an agent, you probably want the TeX. ## Technical reports - [/TR_zeno_variadic.pdf](/TR_zeno_variadic.pdf): "Certifying SDCPNs without a non-Zeno axiom, and with finitely many verification conditions" (21 pages, 2 August 2026, draft for discussion; author line "davidad's AI ensemble"). Safety certificates for stochastically and dynamically coloured Petri nets that bind with zero non-Zeno hypotheses; the classical non-Zeno axiom (Everdij–Blom G4) becomes a certified, priced obligation; plate and variadic machinery gives one footprint verification condition per Petri transition, so nets with unbounded markings get finitely many verification conditions; a small re-entrant fab model is exhibited end to end, with a machine-checked real-time floor of $255N + 375$ ticks over all dispatch policies and a synthesized supervisor reaching all-arrivals at $626N$ counting steps. - [/TR_coln_delta.pdf](/TR_coln_delta.pdf): "Two databases for programs and proofs: a design-delta survey of geolog-alpha and Coln" (13 pages). Deltas in both directions at pinned revisions, each divergence steelmanned before it is judged; six replicate-candidates from Coln and seven held advantages of geolog-alpha. ## Repositories Six repositories live under `github.com/maitria-coalition`. The five toolkit repositories are public today; what is not yet public is not linked. - [kernels](https://github.com/maitria-coalition/kernels) (public): shared multi-architecture fast paths behind one conformance discipline; a lane may change cost, never verdicts; explicitly not a trusted computing base. - [mtk](https://github.com/maitria-coalition/mtk) (public): the modelling toolkit and producer side, untrusted by construction, with a float proposing tier and an exact certifying tier, kernels emitting witnesses rather than bare verdicts, and the proof-production cookbook. The agent-facing session surface has arrived. - [qtsl-experiments](https://github.com/maitria-coalition/qtsl-experiments) (public): the reproduction spine under the book's experiment tables — producers, byte-committed fixtures, receipts, mutant batteries, table generators, one `make` target per chapter section. Every number in the Experiments chapter re-derives mechanically from these committed artefacts. The trusted checkers are imported rather than vendored, and those imports point at the qtsl repository, now public; the spine is public and inspectable end to end. - [qtsl](https://github.com/maitria-coalition/qtsl) (public): the logic itself — theories as data, the literate rule catalogue, Lean rule lemmas and the HOL4 end-to-end development, the certified checkers beside their lemmas, the certificate fixtures, and the book's sources. - [geolog-alpha](https://github.com/maitria-coalition/geolog-alpha) (public): the local-first database whose tables are logical consequences; independently interesting as a principled replacement for an event-sourcing spine; engineering-grade assurance, explicitly not a trusted computing base. - maitria.org (this site): the narrative pages, the guided reading paths, the preserved ledger, and the book. - [geolog-zeta](https://github.com/davidad/geolog-zeta) (public): the ancestor prototype. ## Scope Applications of the toolkit to verifying specific external systems are out of scope for this site. Claims here link down into served artefacts and public repositories; the site never grades itself on a rubric it drew.