Proof-gated architecture
Policy is proven and compiled once. Whoever, or whatever, proposes the action plans freely inside it. Every consequential action is checked against what was proven, every time.
Proof-gated architecture is a pattern for building systems in which the policy governing a consequential action is proven internally consistent and compiled before any action is taken. The proposer, whether an autonomous agent, a conventional application, or a person, keeps full latitude in how it reaches a proposal. Every consequential action is checked against the compiled policy at the moment it is attempted. The pattern does not care what is proposing. It constrains only what is allowed to take effect.
Wherever a consequential action must be checked against policy before it takes effect, that check is done one of three ways today: a rule engine tested into approximate correctness, a person signing off inconsistently on a decision they did not make, or nothing beyond application code that was correct on the day it shipped. All three share a weakness. None proves the rule set internally consistent; each only exercises it against the cases someone thought to check. Autonomous AI agents make this weakness urgent, because they act at a speed and volume that outpaces manual review. Most agent governance responds by adding another probabilistic layer, a model or a learned rule judging whether a proposed action looks safe. That is the same kind of guarantee applied twice; it does not remove the underlying error rate. We describe proof-gated architecture: a pattern in which policy is captured as a bundle, proven internally consistent, and compiled, before any action is taken, into a deterministic enforcement artefact. The proposer keeps full discretion in how it reaches a decision. The gate is the only constraint, and it sits at the single point where a decision becomes an action. We set out the pattern (prove, compile, gate), its four defining properties, its lineage in existing work, where it applies, what it does not guarantee, and how our own deterministic governance and Spec++ work sit inside it as specific instances rather than the whole idea.
Testing a rule set is not the same as proving it.
Every generation of agent tooling arrives with a matching generation of agent governance: more guardrails, more approval steps, more classifiers watching the classifier. Almost all of it sits inside the probabilistic layer, with one model, or a rule learned from data, deciding whether another model's proposed action looks safe. A system that is right almost all the time is still, by construction, wrong some of the time, and a second probabilistic judge inherits that same error rate.
The same weakness exists outside AI, and predates it. A traditional business rule engine encodes "if this, then that" logic across dozens or hundreds of interacting rules, and it is validated by running test cases. Test cases confirm the rules behave as expected in the scenarios someone wrote. They do not establish that two rules never contradict each other in a scenario nobody wrote a test for, and in a large enough rule set, someone always missed one. Manual sign-off has the same shape: a person applying a rule set under time pressure, without anyone having proven the rule set coherent to begin with.
The fix in every case is the same. Remove the judgement call from the point of consequence, and move it somewhere that does not guess: a rule set proven consistent once, compiled into something that enforces it the same way every time, whoever or whatever is asking.
Take three payment rules. R1: a payment may auto-release if it is below the auto-approval threshold and the counterparty is not sanctioned. R2: a payment to a counterparty onboarded fewer than 30 days ago requires dual approval. R3: an auto-released payment does not require dual approval. Each reads well alone. Now take a payment below the threshold, to an unsanctioned counterparty onboarded 10 days ago. R1 and R3 auto-release it with no dual approval; R2 requires dual approval. For a reachable state the policy demands both. A single-table conflict check misses this, and a test suite catches it only if someone writes that exact case. An SMT consistency check finds the contradiction before deployment and returns the offending fact assignment as a witness.
Prove, compile, gate.
A policy bundle is authored once, then proven internally consistent, which means checked for the kind of contradiction that only appears when two rules interact, not when either is read alone. Only then does compilation happen: the proven bundle becomes a policy state machine, the artefact the gate checks deterministically at runtime. Where the proposer is an autonomous agent, compilation can also produce an agent skill, an artefact that tells the agent what the process looks like, what is normal, and what tools exist. Nothing about the skill constrains the agent's plan. The policy state machine alone constrains what is allowed to take effect, whoever proposes it — agent, application, or person.
03 — PropertiesWhat makes an architecture proof-gated.
Bounded autonomy
Whatever proposes the action, an agent planning a multi-step process, a legacy system executing its normal logic, or a person requesting a change, has full latitude in how it reaches a proposal. Nothing above the gate constrains it.
Provable compilation
The policy the gate enforces is captured as a formal bundle and proven internally consistent before it is compiled into an enforceable artefact, rather than tested or reviewed into approximate correctness after the fact.
Deterministic gating
Every consequential action is checked against the compiled policy state machine and returns the same verdict for the same state and action, independent of how, or by what, it was proposed.
In-flight immutability
Once a process begins, the policy governing it cannot change until the process concludes. A process either completes under the policy it started with, or is explicitly terminated. It is never migrated mid-flight to a newer rule set.
It applies to any actor proposing a consequential action.
The same proven, compiled policy state machine can check:
- an autonomous agent proposing a step in a business process it is planning end to end,
- a conventional application executing a fixed code path that touches something consequential,
- a person, acting through an ordinary interface, requesting an approval, a payment release, or a record change.
The pattern generalises because the problem it solves generalises. It is a general answer to "how do we know this rule set holds", and AI agents are the case that makes the question urgent now.
Replacing rule-based frameworks. Some rule engines already include conflict detection. Drools, for instance, flags when two rows of a decision table can both fire with disagreeing outcomes. That is a genuine, useful check, but it is structural, scoped to the table's own rows, and does not extend to rules authored directly, to backward-chaining logic, or to contradictions that emerge from fact interactions elsewhere in the rule base. A proof-gated policy is checked differently in kind: proven internally consistent as a whole, using the same class of SAT/SMT techniques used in formal software verification, before it is compiled.
Guarding human actions. A person requesting a consequential action, releasing a payment, editing a regulated record, or granting an access right, can be gated by exactly the same compiled policy state machine an agent is gated by. This is a stronger control than conventional role-based access or a second person's manual sign-off, neither of which is proven internally consistent, and both of which depend on a human applying them correctly, every time, under pressure.
05 — DistinctionsWhat proof-gated architecture is not.
- ≠Agent governance platforms. Most enforce policy at runtime by scoring or classifying a proposed action, which is another probabilistic system watching the first. Proof-gated architecture proves the policy before any action is taken and gates against a compiled artefact, not a live judgement.
- ≠Traditional rule engines. Engines like Drools include conflict detection scoped to a decision table's rows. Proof-gated architecture proves the whole rule set consistent, with SAT/SMT-class techniques, before compilation.
- ≠Role-based access control and manual sign-off. These constrain who may act, applied by a person or a role check that was never proven consistent. Proof-gated architecture constrains what action may take effect, checked deterministically whoever or whatever is asking.
- ≠Human-in-the-loop. A person reviewing someone else's proposal, under time pressure, against data they cannot fully absorb, adds a formal step rather than a reliable control (see deterministic governance for the full argument). Proof-gated architecture reserves human attention for the exceptions a process surfaces.
- ≠Post-hoc auditing. Reconstructing what happened from logs tells you what happened. It does not establish that only permitted things could have happened.
Most of this pattern already has names.
Stating them makes the contribution clearer, not smaller.
- The gate is a reference monitor (Anderson, 1972): a mediator that is always invoked, resists tampering, and checks every action against a policy.
- The split between proposing and deciding is the policy decision point / policy enforcement point separation formalised in XACML.
- The runtime check is runtime enforcement, whose limits Schneider set out in 2000 with the theory of security automata.
- Deployed engines such as OPA/Rego, AWS Cedar, and Google Zanzibar already enforce policy as a compiled artefact at scale.
- SAT/SMT verification has proven properties of hardware and safety-critical software since the 1990s, and modern solvers such as Z3 have made the tooling widely available.
Against that background, the contribution is narrow and worth stating exactly: prove the policy itself internally consistent across the whole rule set before it becomes the enforcement artefact, and make that proof reachable for a normal engineering team rather than a formal-methods specialist. The mathematics is not new. The reach is.
07 — Related patternsSibling to the circuit breaker.
Proof-gated architecture is a pattern, not an architectural style, and its closest sibling is the circuit breaker. A circuit breaker sits at a call site and decides whether a call may proceed, based on the health of a dependency; its guarantee is about availability. A proof-gate sits at a consequential-action site and decides whether an action is permitted, based on a policy proven internally consistent; its guarantee is about authorisation. Both wrap an attempted operation at a single chokepoint, and both stay deterministic at the point of decision.
The pattern is also a specialisation of separation of concerns. It separates the party that proposes an action from the authority that permits it, and adds one requirement: the authorising side must be provably consistent before it runs.
08 — LimitsWhat the pattern does not guarantee.
Stating the limits plainly is part of the claim, because a careful reader raises them first.
- Consistency is not correctness. Proving a policy internally consistent shows the rules do not contradict each other. It does not show they are the right rules. A consistent policy can be consistently wrong, and choosing the right policy stays a human responsibility.
- Expressiveness trades off against decidability. Keeping the policy inside a fragment a solver can decide efficiently limits what you can express. Some rules will not fit cleanly, and deciding what to place outside the proven core is part of the work.
- Authoring is the hard part. The value depends entirely on the quality of the authored policy. The pattern moves the difficulty from "did enforcement behave?" to "is the policy right and complete?".
- The proof can be expensive. For some rule sets the consistency check is slow or intractable, and the tooling must handle that rather than skip the proof in silence.
Where deterministic governance and Spec++ sit inside it.
Proof-gated architecture is the general pattern. Two things we have already described in depth are specific instances of it, not separate ideas:
- Deterministic governance is proof-gated architecture applied to AI action governance: reasoning separated from authority, and a validator that decides the same way every time, for the case where the proposer is an autonomous agent.
- Spec++ is proof-gated architecture applied to curating and proving software development specifications: the same prove-then-compile discipline, applied to the artefact a system is built from rather than to the actions the system takes at runtime.
Neither is the whole pattern. The general claim is broader than either: wherever policy governs a consequential action, prove it once, compile it, and gate every proposal against it, whatever the source.
Worth separating the two proofs. Proof-gated architecture proves a rule internally sound before anything acts on it, which is a consistency proof. Proof-gated enforcement is the adjacent step that proves, cryptographically, that a given event was gated under that rule and not altered afterwards, using signing, hash-chained logs, and zero-knowledge proofs, which is an evidence proof. One governs what may take effect; the other produces the evidence that it did. They are different problems solved with different tools, and they compose: the architecture decides, the enforcement attests.
The term is new, and we intend to keep developing it in the open. If you are building something with the same shape, policy proven ahead of use, discretion preserved where it is genuinely safe, and a deterministic check at the point of consequence, we would like to know about it. The deeper technical treatment of the proving and compilation stages lives in our research.
10 — FAQCommon questions.
What is proof-gated architecture?
A pattern for systems in which policy is proven internally consistent and compiled before any consequential action is taken, the proposer keeps full discretion in how it reaches a decision, and every consequential action is checked against the compiled policy at the moment it is attempted.
Does this only apply to AI agents?
No. AI agents make the pattern urgent because they act at a speed and volume that outpaces manual review, but it applies to any consequential action proposed by anyone or anything: a legacy application, a business rule engine, or a person using an ordinary interface.
Can this replace a traditional business rules engine?
Yes, for the consistency guarantee it makes, and for any policy expressible in the proven fragment. Existing engines such as Drools include a verification step that warns when two decision-table rows conflict, but that check is scoped to a single table, not a proof over the rule set as a whole. A proof-gated policy is proven consistent in full, using SAT/SMT-class techniques, before it is compiled.
Is proving the policy the same as proving it correct?
No. Proving the policy internally consistent shows the rules do not contradict each other. Whether they are the right rules is a separate, human judgement. The pattern removes one class of failure, contradiction in the rule set, not all of them.
Can it gate actions taken by a human, not an AI?
Yes. The same compiled policy state machine can check a person's requested action, a payment release, a record edit, or an access grant, exactly as it checks an agent's. This is a stronger control than role-based access or manual sign-off, neither of which is proven internally consistent.
How does Spec++ relate to proof-gated architecture?
Spec++ is a specific application of the pattern, proving and compiling software development specifications rather than runtime actions. Deterministic governance is another specific application, for AI action governance. Proof-gated architecture is the general pattern both sit inside.
Can policy change while a process is running?
No. A defining property of the pattern is that policy is immutable for the life of any process it governs. A process either completes under the policy it started with, or is explicitly terminated.
Where does this apply?
Anywhere a consequential action needs to be checked against policy before it takes effect: AI agents executing business processes, legacy applications carrying hardcoded rules, and people operating regulated systems directly.
Bring proof-gated architecture to your highest-risk process.
Start with a fixed-scope pilot on one process, the one with the most human bottleneck, the most edge cases, and the most cost when it goes wrong, whether an agent team, an existing application, or your own people propose the action. Policy proven and compiled once, full discretion preserved upstream, every consequential action gated and logged.