Formal-Proof Compliance Gate

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.

Solution

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.

When to use

• Actions run in a regulated domain where a single non-compliant action is a reportable breach, not a recoverable mistake.
• The binding constraints can be stated as formal invariants over the action and the resulting state.
• A supervisor must be able to re-verify, independently and deterministically, that each executed action was compliant.