We present the current HELM OSS TLA+ model for a six-gate guardian pipeline and the TLC model-checking result for four safety invariants: fail-closed behavior, default deny, unanimity before allow, and freeze override. The model is intentionally bounded and does not claim full proof of the production implementation. It is a repo-backed working paper about what is modeled, what was checked, and what remains outside the proof boundary.

Research question

An execution boundary for AI agents must not fail open. If policy is missing, a gate errors, a connector drifts, or an organisation-wide freeze is active, the boundary should not dispatch the action as if the system were healthy.

This paper documents the current bounded TLA+ model in helm-oss/proofs/GuardianPipeline.tla. The question is narrow: within the modeled state space, do the guardian pipeline invariants prevent an ALLOW verdict when a gate has not unanimously passed?

Source status

The model is real and present in the open-source repository. It models a six-gate guardian pipeline with the following gate set:

Freeze
Context
Identity
Egress
Threat
Delegation

The repository also contains guardian.cfg, which sets MaxActions = 3 and declares the invariants checked by TLC. On 2026-04-29, the model was checked locally with TLC2 version 2.19 using the public tla2tools.jar release from the TLA+ project.

The result:

Model checking completed. No error has been found.
171825 states generated, 32775 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 14.

This is bounded model checking of the specification as written. It is not a mathematical proof of every possible production execution.

Model

The TLA+ specification represents each gate with one of four states:

PASS
DENY
ERROR
PENDING

The pipeline verdict is one of:

PENDING
ALLOW
DENY

The model includes a Boolean frozen state and an actionCount bounded by MaxActions. The next-state relation allows gates to pass, deny, or error; permits the pipeline to allow only after all gates pass; permits freeze activation; and resets the pipeline for the next modeled action.

Invariants

The checked safety properties are:

FailClosed. If any gate is in ERROR, the pipeline verdict is not ALLOW.
DefaultDeny. If any gate is still PENDING, the pipeline verdict is not ALLOW.
AllowRequiresUnanimity. If the pipeline verdict is ALLOW, every gate is PASS.
FreezeOverride. If the system is frozen, the pipeline verdict is not ALLOW.

Together, these invariants test the core property expected from an AI execution boundary: an allow decision is reachable only after a complete, non-frozen, non-error, all-pass evaluation.

Interpretation

The model establishes that the abstract guardian state machine does not reach an allow verdict in the failure cases it explicitly models. That matters because fail-open behavior is often introduced by edge conditions: partial evaluation, stale state, error handling, or emergency override logic.

The model also gives implementers a compact contract. Production code should preserve the shape of the invariant:

missing or pending gate output is not allow;
gate error is not allow;
freeze state dominates local gate success;
allow requires unanimity across the configured gate set.

This is directly relevant to agent execution because the model treats the action boundary as a policy enforcement point. The model does not ask whether a model’s reasoning was correct. It asks whether the boundary can accidentally turn incomplete or failed evaluation into permission.

What the model does not prove

The proof boundary is deliberately small. It does not prove:

correctness of the production Go implementation;
correctness of connector schemas;
cryptographic soundness of receipts or signatures;
semantic quality of threat detection;
absence of policy authoring mistakes;
unbounded liveness;
all possible combinations of tenants, identities, policies, and delegated actors.

It also abstracts away timing, concurrency, storage failure, and distributed cache behavior. Those are separate modeling tasks.

Relationship to Apalache and Lean

The local check described here uses TLC, the explicit-state TLA+ model checker. Apalache is a symbolic model checker for TLA+ and is an appropriate next step for richer bounded analysis, but this paper does not claim an Apalache CI result for the current file.

The repository also contains a Lean proof workflow for separate proof material under proofs/Lean. That workflow should not be conflated with the TLC result for GuardianPipeline.tla. The current paper is scoped only to the TLA+ guardian model and the TLC run above.

Operational use

A bounded model is useful if it changes engineering behavior. The model should be used as:

a regression oracle for edits to the guardian pipeline;
a source of invariant names used in tests and documentation;
a design review checklist for new gate types;
a reference when evaluating fail-closed claims in competing systems.

It should not be used as a blanket safety claim. A public research page should distinguish modeled behavior from production guarantees.

Reproducibility

From a checkout of the HELM OSS repository:

mkdir -p .cache/tlc
curl -L -o .cache/tlc/tla2tools.jar https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
cd proofs
java -cp ../.cache/tlc/tla2tools.jar tlc2.TLC -config guardian.cfg GuardianPipeline.tla

Expected result: TLC reports no invariant violation for the bounded model.

Conclusion

The current TLA+ model gives a concrete, checkable statement of fail-closed behavior for a six-gate AI execution boundary. Its value is precision. It says exactly when an allow verdict is reachable in the modeled system and exactly what remains outside the proof boundary. That is the standard public AI infrastructure claims should meet.

A bounded TLA+ model of fail-closed AI execution