v0.3.1 · policy enforcement middleware for AI agents

A firewall for AI agent actions. Formally checked, cryptographically logged, honest about its limits.

Corrigibility sits between an agent and the actions it wants to take. It checks each action's parameters against typed policies with the Z3 solver, quantifies its own uncertainty, writes every decision to a tamper-evident log, and never argues with a shutdown.

What it does not do Code artifact · DOI
decision recordrun 2026-09-12
scenario
Mass email, 50 recipients
action
COMMUNICATION
decision
BLOCKED
policy
communication_limits
reason
Critical constraint violation → bulk messaging blocked, max 20 recipients per action
uncertainty
0.500 · CI [0.000, 1.000]
z3
used, concrete mode
eval
2.79 ms
Output of demo.py, unedited. Merkle root of the run: 6af24162…8c37. Nothing on this page is live.
56
tests passing
82%
line coverage, measured
3,910
lines of Python
0
HTTP APIs, SDKs or dashboards

§ 01 · Scope

Honest scope

This is a policy enforcement middleware, similar to a firewall for AI actions. A network firewall cannot prevent every attack, but it reduces risk in a way you can inspect. This system cannot prevent all unsafe agent behaviour, but it creates a verifiable, auditable safety layer around the actions an agent is allowed to take.

⊢What it does

  • Intercepts every action an agent attempts.
  • Verifies the action's parameters against typed policies with Z3, in concrete mode: exact evaluation of the actual values, with counterexamples.
  • Proves whether a policy is satisfiable at all, symbolically, and names the contradiction when it is not.
  • Quantifies uncertainty with calibrated conformal prediction and routes doubtful actions to a human.
  • Logs every decision in a hash chain with a Merkle tree, an optional Ed25519 signature over the chain head, and certified deletion for legal erasure.
  • Enforces shutdown unconditionally, before any policy runs.

⊬What it does not do

  • It does not verify the internal reasoning of a model.
  • It does not detect alignment faking inside a neural network.
  • It does not guarantee safety against a superintelligent adversary.
  • It does not replace human oversight. It augments it.
  • It does not stop an agent that can reach the world without passing through it. Making the layer unavoidable is the next build, not this one.
  • It does not ship an HTTP API, SDKs, metrics exporters or compliance reports. It is a Python engine with a test suite.

The quality of the safety depends on the quality of the policies. The engine proves that an action satisfies the constraints you wrote. It cannot prove that you wrote the right constraints.

§ 02 · Mechanism

How a decision is made

Four steps, in this order, for every action. Each step is a module you can read: core/engine.py, core/verifier.py, core/uncertainty.py, audit/trail.py.

  1. Intercept

    The agent proposes an action with typed parameters and context. Nothing executes until the engine returns a decision.

  2. Verify

    Every applicable policy constraint is checked with Z3 against the concrete values. A violation returns the constraint, the actual value and the expected one. Critical and fatal violations block.

  3. Quantify

    A conformal predictor scores how confident the system is. Under uncertainty it restricts further: the action goes to needs_human_review instead of through.

  4. Log

    The decision is appended to a hash chain with per-record salts, folded into a Merkle tree, and the chain head can be signed with a key held outside the process.

step 0 · shutdown

A shutdown request is detected by broad keyword matching and approved unconditionally, before any policy and before Z3 is involved. No policy can override it.

This is a hard-coded fail-safe, tuned toward false positives. It is not a formal proof. Earlier versions of this project said otherwise; that claim was withdrawn in August 2026.

§ 03 · Status

What is verified today

Three states, no adjectives. Done means it runs and the test suite covers it. Partial means it works but is weaker than it sounds. Not yet means it does not exist, whatever earlier material said.

CapabilityStateWhat it actually is
Per-action constraint check with Z3DoneConcrete mode: the actual parameter values are asserted and the negation is checked. Exact evaluation with counterexamples, not symbolic verification over ranges.
Policy consistency proofDoneSymbolic. One unpinned real per parameter, every unconditional numeric constraint asserted, satisfiability checked. UNSAT means the policy is a silent deny-all; the unsat core names the conflicting constraints.
Fail-closed when the solver is missing or times outDoneWithout Z3, or on an unknown answer, the consistency check reports consistent=False, verified=False. Unverified is never reported as a pass. Added September 2026.
Calibrated uncertaintyDoneConformal prediction with coverage guarantees decides when a human must look. Without calibration data the score is 0.5 and everything not blocked goes to review, as the run below shows.
Tamper-evident audit trailDoneSHA-256 hash chain with per-record salts, Merkle tree, optional Ed25519 signature over the chain head with an external key, certified deletion via signed and chained certificates. Tamper-evident, not tamper-proof.
Unconditional shutdownPartialKeyword-detected, hard-coded approval that runs before any policy. Deliberate and defensible. Not Z3-verified.
Conditional constraints in the consistency proofNot yetConstraints with a when clause are excluded from the satisfiability check. Case-splitting over contexts is designated future work.
External anchoring of the logNot yetChain-head signing stops a filesystem-only adversary. An adversary holding the signing key still needs a transparency log to be caught. Future work.
Unavoidable enforcement pointNot yetToday the agent must call the engine. A gateway that makes bypass structurally impossible is the current build and is not published here until it runs.
HMAC, REST API, SDKs, Prometheus metrics, regulatory mappingsNot yetNone of these exist in the code. Earlier public material claimed some of them. Withdrawn.

§ 04 · Evidence

A real run, unedited

There is no live demo on this site. A browser simulation would show you random numbers and call them verification. Instead, this is the output of python demo.py from 12 September 2026, ten scenarios against nine policies, with the integrity check of the resulting audit trail. Full transcript.

Engine initialized with 9 policies

Scenario: Safe email (1 recipient, no PII)
  Decision: NEEDS_REVIEW   Uncertainty=0.500, CI=[0.000, 1.000]
  Eval time: 24.17ms   Z3 used: ✓

Scenario: Mass email (50 recipients)
  Decision: BLOCKED
    Critical constraint violation in communication_limits
    → Bulk messaging blocked — max 20 recipients per action
  Eval time: 2.79ms    Z3 used: ✓

Scenario: Email with PII
  Decision: FATAL
    Fatal policy violation in communication_limits
    → Cannot send PII in communications without explicit approval
  Eval time: 0.52ms    Z3 used: ✓

Scenario: Database dump attempt
  Decision: FATAL
    Fatal policy violation in data_protection
    → Broad data access patterns blocked
  Eval time: 0.65ms    Z3 used: ✓

Scenario: Delete request
  Decision: NEEDS_REVIEW
    data_delete actions always require human approval
  Eval time: 0.46ms    Z3 used: ✓

Scenario: Modify safety settings
  Decision: FATAL
    Fatal policy violation in system_protection
    → Cannot modify safety-related system settings
  Eval time: 0.26ms    Z3 used: ✓

Scenario: SHUTDOWN
  Decision: SHUTDOWN
    SHUTDOWN APPROVED — unconditional
    Shutdown IS safety. No policy can override this.

Audit Trail Integrity Check:
  Valid: ✓   entries: 11
  All entries verified with hash chain + Merkle tree
  Merkle root: 6af24162ab93a121db44b869d2dd8c37...
approved0
blocked6
needs review3
shutdown1
date
2026-09-12
version
v0.3.1 + Sep 2026 fix
solver
z3-solver 5.1.0
python
3.14, one process
eval time
0.26 to 2.79 ms after the first call; 24 ms cold

Why zero approvals. The demo ships without calibration data, so the conformal predictor reports 0.5 uncertainty for everything and the engine restricts further: nothing passes without a human. That is the intended failure mode, not a bug.

Timings are not a benchmark. They are one run on one laptop, printed as measured. No P99 is claimed.

§ 05 · Record

We number down when we find out we were wrong

Two versions of this project were labelled production-ready before they were. When an audit showed what they actually did, the version number went backwards, in public, instead of forwards. That record is the strongest evidence this page can offer that "honest" is a method here and not a tone.

  • v1.0retracted

    "Production-ready" AI safety framework

    String matching presented as verification. Not real.

  • v1.5retracted · Oct 2025

    Z3 integration

    Verified strings, not actions. Claimed HMAC signatures that did not exist and a Z3-verified shutdown that was keyword matching. The site you are reading replaced the one that still sold this version.

  • v0.3renumbered

    First honest, functional version

    The backward renumbering v1.5 → v0.3 was a public retraction. Concrete-mode Z3 over typed action parameters, conformal uncertainty, hash-chained audit trail.

  • v0.3.1Aug 2026

    Honesty and capability fixes

    The distributed v0.3 archive did not run: package imports shipped flat. Fixed, and the suite executed for the first time: 53 tests, 82% measured coverage, replacing an unauditable "85%+". Added certified deletion with crypto-shredding, Ed25519 chain-head signing, the symbolic policy consistency proof, and the honest description of Z3 as concrete-mode.

  • unreleasedSep 2026

    Fail-closed consistency check

    The consistency proof returned "consistent" when Z3 was missing or timed out: a missing solver disguised as a proof. Both paths now return not consistent and not verified. Suite at 56 tests.

§ 06 · Research

Four necessary properties

The engine is the code artifact of an RFC that proposes four properties any AI safety framework must satisfy as necessary, not sufficient, conditions for verifiable trust. Each property is formally defined, motivated by the failure mode its absence produces, and paired with an honest statement of implementation status.

Version 0.3, August 2026, corrects the document's claims about itself. An internal adversarial audit compared every implementation claim line by line against the shipped code. Twenty-three findings survived, and each one is listed with what was wrong, why, and the correction.

"This remains a request for comments, not a declaration of principles. We believe these properties are correct. We are requesting help finding where they are still wrong, incomplete, or impractical."

RFC v0.3, abstract

RFC
Four Necessary Properties for Verifiable AI Safety, v0.3, 14 August 2026. Licence CC BY 4.0. Draft available on request.
Code
Corrigibility v0.3.1, archived with a DOI: 10.5281/zenodo.17429067
Licence
Business Source License 1.1
Repository
Not yet public. The archived artifact is the citable source until it is.
Thesis
Corrigibility is a property of the environment, not of the agent. The agent does not choose to be corrigible; the environment leaves it no alternative.

§ 07 · Contact

One door

Comments on the RFC, requests for the draft or the code, and conversations about running this in front of a real agent all go to the same address. There is no sales team, no pilot programme and no calendar link.

antonio@aliaco.org
Author
Antonio Manjarrez, with AI collaboration. Every claim on this page maps to a line in the README or the RFC changelog.
Verify
Ask for the artifact, run python -m pytest, then run demo.py and compare it with § 04.