The AI2 gate is a reference monitor and a safety instrumented function, applied to the actions of AI agents. This page states what the corpus inherits, what it adds, and what it still owes.
Computer security has known since 1972 how to mediate every access through a small, tamper-proof checker that the governed program cannot reach. Process safety has known for decades how to keep a trip independent of the control system it protects, how to make one demand win over any number of permits, and how to require a deliberate reset after a trip. The corpus applies both, in independent hardware, to the individual actions of an AI agent: the tool call, the transfer, the write, the command.
That is the AI2 gate. A model proposes an action. A separate, finite evaluator, sharing no write path, memory, clock or power with the model, decides whether that exact action may cross a declared boundary now. Denial dominates. Authority is never restored by the governed system. The object that reaches the consequence must be the object that was authorized.
In one line: a reference monitor in Anderson's sense, built with the independence discipline of a safety instrumented system, placed on the action path of an AI agent.
The Model Proposes. The Gate Disposes.™
The corpus uses its own vocabulary because it extends these ideas in specific ways, set out in §03. Each paper in the gate track now carries a lineage note at the top and a related-work section at the end, so that a reader trained in either discipline can place every result against the work it builds on.
Anderson's 1972 planning study for the U.S. Air Force defined a reference validation mechanism with three properties: it is always invoked, it is tamper-proof, and it is small enough to be analyzed and tested completely. Saltzer and Schroeder (1975) named the surrounding principles, including complete mediation, fail-safe defaults and separation of privilege. Axiom A1 and its six construction obligations (Genesis §7.1) are the tamper-proof property stated for physical hardware. WP-12's requirement that the evaluator be a finite automaton, checkable over every reachable state, is the third property. Rule R4, "every effect is mediated," is complete mediation.
IEC 61508 and IEC 61511 require a safety instrumented system to be independent of the basic process control system it protects, and they treat common-cause failure (shared power, clocks, firmware and so on) as the thing independence must defeat. WP-16 §04 states the same pattern: the optimizer proposes, the regulator executes, the independent trip disposes. The corpus's four-state chain is a trip with two hold states and a latched state. Its global meet is 1ooN voting, where any single demand trips (Genesis §4.3 compares it with 1oo2, 2oo3 and 2oo4D directly). The requirement that recovery from a trip take two rising edges from disjoint trust domains is a manual reset with separation of duty.
The Simplex architecture (Sha, 2001) pairs an unverified high-performance controller with a verified safety controller and a decision module that switches between them. ASTM F3269 standardizes the same pattern for aircraft. The gate keeps the decision module and removes the second controller: when authorization is lost, outputs fall to a fixed fail-safe state rather than to an alternative policy, and they stay there until an exogenous grant. Control barrier functions (Ames et al.) supply the certificate that WP-12's proposal side computes and the evaluator only checks.
Schneider (2000) characterized the policies an execution monitor can enforce: those whose violation can be detected on a finite prefix of execution, so that the monitor halts the program before the bad step. Ligatti, Bauer and Walker extended this to edit automata, and shield synthesis (Bloem et al.) applied it to reactive and learning systems. WP-17C's distinction between authorization and quarantine is Schneider's distinction between preventing a bad step and responding after one, stated for agents and their effects.
Use this table to read any paper in the gate track. The last column is the part each paper has to defend as its own.
| Corpus term | Standard term | Lineage | What the corpus adds |
|---|---|---|---|
| Λ, the adaptive execution plane | Untrusted component; Simplex high-performance controller | Anderson 1972; Sha 2001 | The AI model is untrusted by default, however capable it is |
| Π, the governance stack (F, the evaluator inside it) | Reference monitor; Simplex decision module; SIS logic solver | Anderson 1972; Sha 2001; IEC 61511 | Enforced in separate silicon, at the level of individual agent actions |
| Axiom A1 and obligations A1.1–A1.6 | Tamper-proofness; separation; SIS independence and common-cause defence | Anderson 1972; Rushby 1981; IEC 61508, IEC 61511 | Clock, reset and power domains named explicitly, as an audit obligation rather than a proof |
| Global meet; zero masking; deny dominates | 1ooN trip voting; fail-safe defaults; lattice meet | IEC 61508 voting architectures; Saltzer and Schroeder 1975; Denning 1976 | Trip voting applied to the permissions an agent holds, with the availability cost stated (Genesis §4.4) |
| Four-state chain BOT < IDLE < COND < TOP | Trip, hold points and run permissive | Process-safety practice (hold point versus scram) | Two non-latched hold states that carry diagnostic information |
| Ratchet; authority is never restored autonomously | Latching trip; manual reset | IEC 61511 | Latching applied to authority itself, with the fan-in of the set input audited at netlist level (WP-10 Obligation 6) |
| Two rising edges from disjoint trust domains | Two-person rule; separation of duty; separation of privilege | Saltzer and Schroeder 1975; Clark and Wilson 1987 | Required in hardware, as edges rather than levels (Genesis Theorem 6.3) |
| Input equals output, or fail closed (R3, Law 5) | Complete mediation at the point of use; time-of-check-to-time-of-use prevention; integrity binding | Saltzer and Schroeder 1975; Bishop and Dilger 1996 | Comparison at the point of consequence, on the evidence path as well as the object path |
| Binding at origin; state-witness isolation | Provenance; measured attestation; signed sensor data | TCG TPM 2.0 attestation | The evaluator verifies a binding it did not compute |
| PCR™, the Permission Control Runtime | Synchronous policy enforcement point and decision point | OASIS XACML 3.0; NIST SP 800-162; NIST SP 800-207 | The decision point runs on the independent hardware, under a pause → contextualize → resume cycle |
| Grant: exogenous, fresh, bound, single-use (WP-16 Rule 2A) | Capability; time-boxed, caveated, bounded-use token | Dennis and Van Horn 1966; Birgisson et al. 2014 | Checked against a pinned action schema, with a unique admissible interpretation (Rule 3A) |
| Authorization Gap™ | Missing mediation at the action boundary; confused deputy | Hardy 1988; Saltzer and Schroeder 1975 | Locates the gap where agents act, and gives a falsification condition for closing it |
| Level 3 versus Level 4 (WP-12, WP-17C) | SIS trip on measured state versus a start permissive | IEC 61511; Schneider 2000 | A ladder that classifies containment products against pre-effect authorization |
| Level 7, energy-bound control | De-energize to trip; Safe Torque Off; stop categories 0 and 1 | IEC 61800-5-2; IEC 60204-1 | The governed intelligence's own supply is the controlled path, with drop order and reservoir bounds |
| Path dossier, ten exhibits (WP-18) | Assurance case; safety case evidence | Kelly and Weaver 2004 (GSN); ISO/IEC/IEEE 15026-2 | One case per path, with a machine-readable schema that refuses a claim with a missing exhibit |
| Monitoring link with no control path | Data diode; unidirectional gateway | IEC 62443 zones and conduits | Remote supervision of the gate without a path into it |
| Prior work | What it does | How the gate differs |
|---|---|---|
| Simplex; ASTM F3269 runtime assurance | Switches control to a verified fallback controller when the advanced controller leaves a safety envelope | No fallback policy: loss of authorization de-energizes to a fixed fail-safe and latches. Re-entry needs an exogenous grant, not a return to the envelope. |
| Separation kernels; seL4 | Prove isolation of partitions sharing one processor, with a machine-checked proof (seL4) | Isolation is physical rather than proved about shared hardware. seL4 has a mechanized proof. The gate does not yet; WP-10 Obligation 5 lists it as open. |
| Safety instrumented systems (IEC 61511) | Trip on measured process state after an excursion begins | That is Level 3. Level 4 decides on a typed action or a predicted state, before the effect is issued. |
| Hardware security modules; TPMs | Guard keys and attest platform state. An HSM refuses to use a key without authorization. | The gate guards the effect, not the key. The HSM's refusal to sign is the nearest analog to Level 4, applied to one kind of effect. |
| Zero-trust policy enforcement points | Mediate access requests against a policy decision point | A software enforcement point shares fate with its host (Level 2). The gate places the decision in independent silicon on the action path. |
| Execution monitors; shields | Theory of what a monitor can enforce, and synthesis of shields for reactive systems | The theory carries over. The gate is a physical placement of such a monitor, with a latch the monitored system cannot reset. |
| Data diodes | Enforce one-way information flow in hardware | Used inside the gate's own design for supervision. The gate itself is two-way: proposals in, a decision out. |
The corpus keeps these separate, and so does this page.
| Item | Status | Where |
|---|---|---|
| Meet algebra, zero masking, latch invariance under arbitrary rules | Paper proof | WP-10 §4; Genesis §4 |
| No autonomous ascent; two-domain recovery | Paper proof | WP-12 Theorem 3; Genesis Theorem 6.3 |
| Evaluator RTL behaviour | Simulation | 33-check testbench on 64/157,181 (WP-10 §6.1) |
| Mechanized proof (Coq, Lean or TLA+) | Owed | WP-10 Obligation 5; WP-12 §8 |
| Netlist proof that only the reset line can raise the latch | Owed | WP-10 Obligation 6 |
| Published bench data: latency, fault injection | Owed | WP-16 §22; Genesis Appendix B |
| Worked end-to-end example on one plant | Owed | WP-12 §8 |
| Level 7 cut-set, drop order, reservoir bound | Validation target | WP-16 §18–19 |
The next exhibit. One real agent tool call, blocked end to end by the gate, with measured decision latency and a fault-injection log, would move the central claim from specified to demonstrated. That is the most valuable single addition to the corpus.
Across the gate track, Λ is the adaptive execution plane (the model and everything sharing its fate) and Π is the governance stack that is structurally disjoint from it. F is the evaluator inside Π. Two papers use these letters differently, and each now says so at the top:
The gate is close to existing practice and deployable now: this summary, then WP-17C, WP-16, WP-10, Genesis Rev 3.1, WP-12, WP-13, WP-18, WP-19 and the errata. The Synthetic Intelligence programme is a research track that adds no authority to the gate: One Skin, Two Faces, the Canonical statement, WP-11, WP-14, WP-15 and WP-20. Its claims about a new kind of machine are stated as hypotheses with the observations that would falsify them. The index lists both.