Foundational Research: Trustworthy Scientific AI
The gate you can trust
The idea behind a safeguarded AI is a gatekeeper: an agent may act only if it can present a certificate that its action is safe, and a small trusted component checks that certificate before anything happens. The appeal is obvious. The hard part is building a runtime where the check is small enough to actually trust and fast enough to run on every action. This is a working reference gatekeeper for a multi-agent system, and because the system is bounded we do not sample its safety, we verify all of it.
Unsafe actions blocked
672 / 672
and 504/504 safe admitted
Verification
exhaustive
sound and complete, not sampled
Trusted core
31 lines
0.36 microseconds per check
The Challenge
High-stakes multi-agent systems cannot yet give demonstrable guarantees of safe behaviour, and the usual formal-methods answer is too slow and too specialised to sit in the execution loop. What deployment needs is not another offline verifier but a runtime where every action is gated by a check you can trust because it is small, and afford because it is fast. That is the gatekeeper pattern, and its credibility rests entirely on the size and speed of the trusted component doing the checking.
Proof-carrying actions
The scenario is a small warehouse: two robots on a 3x3 grid, a shared battery budget, and one irreversible hazard cell. The safety specification is three invariants that must hold in every state, the robots never share a cell, neither enters the hazard, and the battery never goes negative. A proposer, which may be untrusted or an ML policy, emits a joint action and a certificate: the state it claims results and its claim that the result is safe. The gatekeeper, the only trusted component, recomputes the successor and checks it matches the certificate (so the proposer cannot lie about the outcome), then checks that successor against the three invariants. It dispatches only if both pass. Generating a safe action may need search; checking one is a handful of comparisons. That asymmetry is the whole design: an arbitrarily capable, untrusted proposer behind a tiny, trustworthy gate.
| Property | Result |
|---|---|
| Verification | exhaustive over the full reachable state space |
| Reachable states / transitions | 96 / 1,176 |
| Unsafe actions blocked | 672 / 672 (100%) |
| Safe actions admitted | 504 / 504 (100%) |
| Soundness & completeness | both hold across the reachable space |
| Adversarial (lying) proposer | 672 / 672 unsafe proposals blocked |
| Ungated baseline | 57.1% of transitions unsafe |
| Checker latency / trusted core | 0.36 microseconds / 31 lines |
Because the model is bounded, the checker enumerates the entire reachable state space and, for every state and every action, confirms it admits the action if and only if the resulting state is safe. That is a complete soundness-and-completeness result over the reachable space, not a passing test suite. An adversarial proposer that simply asserts "this is safe" is blocked on every one of its unsafe proposals, and without the gate 57% of transitions would land in an unsafe state, so the gate is load-bearing, not decorative.
The same gate on two real benchmarks
The gate is not tied to the warehouse. We run it, unchanged, on two published multi-agent safety benchmarks, using their real maps and safety definitions.
Island Navigation (DeepMind AI Safety Gridworlds). We take the official map and safety definition verbatim from the repo: the agent must reach the goal without ever entering water, an irreversible drowning penalised at -50. The gate permits a move only if its certified destination is not water. Exhaustive over the 21 reachable cells and 84 moves, it blocks 10 of 10 water-entering moves and admits 74 of 74 safe ones, sound and complete; ungated, 11.9% of moves would drown the agent.
Commons Harvest (Melting Pot), a faithful reimplementation of the substrate's dynamics: apples regrow only while an apple remains nearby, so eating the last apple in a patch kills it forever, the tragedy of the commons. The safety spec is sustainability, never harvest so as to empty a patch. The gate is verified exhaustively on a bounded instance (447 of 447 patch-killing harvests blocked, 1,857 of 1,857 safe harvests admitted), and a dynamic episode with four greedy agents shows what it buys:
| Commons after 200 steps (mean of 20 runs) | Ungated | Gated |
|---|---|---|
| Dead cells (irrecoverable) | 36 / 36 | 0 / 36 |
| Apples remaining | 0 | ~10 |
Ungated greedy agents collapse the commons completely; the same agents behind the sustainability gate never kill a patch, and the resource persists. Same 31-line trusted core, three different systems.
Why this is the ownable gap
The field ships verifiers and papers; what deployment needs is a certificate-carrying runtime, a gate small and fast enough to sit on every action. Making the trusted core explicit, 31 lines, sub-microsecond, and verifying the whole system rather than testing it, is the move. It is the runtime companion to a closed-world check on what a model emits and to the certificate ladder we are building elsewhere, and it is the reference specification for a formally-verified agent runtime whose small C core would carry exactly this gate into production.
"You do not make an untrusted agent safe by making it smarter. You put it behind a gate small enough to trust and fast enough to run on every action, and you verify the gate, not the agent. Then the agent can be as capable, and as untrusted, as you like."
Fabio Rovai, Tesseract Academy
An independent, self-initiated study. Every guarantee is exhaustive over a bounded model; scaling to large systems needs symbolic model checking, where the same small checker stays small. This repo verifies the systems exhaustively but does not ship a machine-checked proof of the checker itself, that is the role of the Tardygrada formally-verified runtime, whose C core is the production vehicle for this gate. The Island Navigation map and safety definition are taken verbatim from the official AI Safety Gridworlds repository (its live engine also loads and steps here); Commons Harvest is a faithful reimplementation of the Melting Pot substrate, since that engine's dmlab2d backend does not build in this environment. Full method and reproducible code in the repository.
Reproduce it
Pure Python standard library. Run the exhaustive verification in Colab or from the repo.
