VIII · Safety & ControlExperimental·

Formal-Proof Compliance Gate

also known as Type-Checked Compliance, Theorem-Prover Action Gate, Machine-Checked Compliance Proof

Require every agent-proposed action to ship a machine-checked proof that it satisfies the binding regulatory invariants, and reject deterministically any action whose proof does not check.

This pattern helps complete certain larger patterns —

  • specialisesStochastic-Deterministic Boundary (SDB)★— Formalize the seam between an LLM proposal and a system action as a four-part contract — proposer, verifier, commit step, reject signal — so the contract itself, not the agent's good intent, gates side-effects.

Context

An agent proposes consequential actions in a regulated domain such as order routing, capital allocation, or fund transfers, where a single non-compliant action carries legal liability rather than mere inconvenience. The binding constraints are written law — position limits, capital-adequacy floors, best-execution duties, segregation-of-funds rules — and a supervisor must be able to show, after the fact, that no executed action ever violated them. A probabilistic check that is usually right is not enough when one slip is a reportable breach.

Problem

An agent reasons stochastically, so any guard that asks the model whether an action is compliant inherits that uncertainty, and a heuristic rule engine only covers the cases its author anticipated. Audit-after-execution finds breaches only once the damage is done, and statistical guardrails leave a residual probability of letting a forbidden action through. The supervisor needs a guarantee that holds by construction before the action runs, not a confidence score that holds most of the time.

Forces

  • A breach in a regulated domain is a legal event, so a residual error rate that is acceptable for a recommendation engine is unacceptable here.
  • Heuristic policy engines are fast to write but only enforce the cases their rules enumerate; an unanticipated action shape slips through.
  • A machine-checked proof is a hard guarantee, but encoding regulation as formal theorems and producing a proof per action costs specialist effort and latency.
  • Not every regulatory duty is cleanly formalisable, so the gate covers the invariants that can be stated as theorems and must defer the rest to other controls.

Example

A trading agent proposes to buy 5,000 shares for a client account. Alongside the order it emits a proof that, after the fill, the account stays inside its position limit and the firm's capital-adequacy floor still holds. A Lean checker runs the proof in milliseconds; it type-checks, so the order is released and the proof is stored. A later proposal that would breach the position limit cannot be proven, so the checker rejects it and the order never leaves the system.

Diagram

Solution

Therefore:

Encode the binding regulatory invariants once as formal theorems in a proof assistant or a sufficiently expressive type system, for example position and capital invariants expressed as Lean 4 theorems. Every action the agent proposes must be accompanied by a machine-checkable proof object that, given the current state and the action's parameters, the post-action state still satisfies those theorems. A deterministic checker runs the proof: if it type-checks, the action is admitted to execution; if it does not check, or no proof is supplied, the action is rejected outright and never reaches the side-effecting layer. The agent may search for an action and its proof, but only the checker grants execution, so compliance is established mathematically before anything runs rather than asserted by the model or sampled by a statistical filter. The checked proofs accumulate into an audit record that a supervisor can re-verify independently.

What this pattern forbids. An action may not execute unless it ships a machine-checked proof that the required regulatory invariants still hold after it; actions with a failing proof or no proof are rejected deterministically and never reach the side-effecting layer.

And the patterns that stand alongside it, or against it —

  • alternative-toPolicy-as-Code Gate★— Evaluate every proposed agent action against externally-managed machine-readable policies before dispatch, so compliance authorship lives outside the prompt and outside the agent code.
  • complementsSimulate Before Actuate★— Before issuing an irreversible action, run a deterministic simulation that computes pre-conditions, invariants, and expected deltas; require a verifier — automated or human — to green-light the simulated outcome before the real command is sent.
  • complementsCompliance-Certified Launch Gate★— Require an external regulator to certify the generative service against a published content-safety standard before it may serve the public, forcing the standard's controls into the build as a re-certifiable artifact.

Neighbourhood

Click any neighbour to follow the language. Scroll to zoom, drag to pan.

References

Provenance