Why ECL-1 uses TLA+

The hard question is what happens between the steps

“Check the permission, then perform the action” sounds complete. It leaves several questions unanswered. Can the permission expire between those steps? Can a second process use the same permission? What if the decision service goes down after approval? If an action reaches a remote server but its reply is lost, is a retry another attempt or another effect?

These are questions about the design before they are questions about code. A careful implementation of an ambiguous rule can still do the wrong thing. The purpose of the ECL-1 models is to give part of that design an exact meaning, then ask whether its rules permit a behavior that contradicts its stated properties.

A test exercises particular executions of a program. TLC, the model checker used here, explores the reachable states of a finite model and checks the selected properties across that state space. That makes it useful for orders of events a test author might not think to write down. The trade-off is abstraction: the model omits much of a running system, and the configurations are deliberately small. Exhaustive exploration of those configurations is not exhaustive testing of production.

The practical question is therefore specific: if these are the rules, under these assumptions and bounds, can an unauthorized effect still occur? A counterexample answers with a sequence of model states. That sequence gives a reviewer something concrete to dispute or repair.

Why TLA+, rather than another application test?

TLA+ is a language for specifying how a system’s state may change over time. An action describes a permitted transition; a behavior is a sequence of states. This is a useful level for ECL-1 because its runtime rules span several participants: an actor, a decision service, enforcement points, control updates and an emergency halt plane. No single function owns the whole sequence.

Writing the design at that level forces choices that ordinary prose can leave implicit. Which component may create authority? Which facts can change after a decision? Is consuming a permit part of the same transition as using it? What must eventually happen to a request that remains on hold? The language makes those choices inspectable without prescribing a customer’s programming language, database or cloud.

TLA+ and TLC are different things. TLA+ expresses the specification; TLC checks configured instances of it. TLAPS is a separate deductive proof system. ECL-1’s published TLA+ results are TLC model-checking results, not a TLAPS proof of the entire standard or its implementations. Leslie Lamport’s high-level introduction explains this way of describing systems.

Why there is a second model

The runtime model treats an action’s digest as the action itself and assumes only the decision service can create authority. That is helpful for reasoning about control flow, but it does not analyze signed messages crossing a hostile network. The separate Tamarin model addresses that question: who could have issued an accepted message, and does it authorize exactly this request, action and enforcement point?

Using both makes the division visible. TLC examines runtime rules, timing and control state. Tamarin examines symbolic message authentication and binding. Neither substitutes for parser tests, cryptographic-library review, an implementation assessment or checking the actual routes to an effect. The Tamarin introduction describes its protocol-analysis approach.

What the runtime model represents

The actor is not assumed to be cooperative. It can submit requests, present existing authority at different enforcement points, and try replay, altered actions or use after expiry, revocation or halt. It chooses self-reported inputs and steers judgment inputs such as a risk score. In the correct design it cannot write decisions, create authority or edit the evidence history, and it has no separate path to an effect.

The decision service

Answers admit, deny, hold or challenge. An admission issues authority bound to a request identifier, its action, an enforcement-point audience, a validity window, a trust epoch and a single use. An authenticated approval can resolve a hold or challenge through a new decision.

The enforcement point

Checks the authority against the request presented there, its current control state and the halt state. It remembers consumed authority. In the model, consuming authority, making an effect and recording its evidence happen together.

The control plane

Revokes authority and changes the policy and trust epoch. Enforcement points refresh their view while the control plane is reachable; propagation and stale-state limits govern the permitted delay.

The emergency plane

Requests a halt that each enforcement point acknowledges. It is separate from the decision service, so the model does not make a functioning decision service a prerequisite for stopping.

Time and failure

Discrete ticks represent time. The decision service can fail and recover. Decision and hold deadlines lead to a declared safe state. Process crashes, storage failures, clock skew and uncertain remote responses are not represented.

The model’s advancing clock is also a substantive assumption. In the correct control configuration, time cannot advance past a required propagation or halt-acknowledgment deadline while that obligation remains unmet. The model examines a design that meets those deadlines; it does not prove that a host scheduler, network or operator can meet them.

Read ECLCore.tlaRead the concrete values in MC.tlaRead the modelling assumptions

Three examples of what the checks are for

The sequences below are teaching examples of the model’s rules, not transcripts from a production incident or quoted TLC traces. The linked configurations and recorded outcomes are the evidence.

1. A valid signature does not make a permit reusable

Suppose a request is admitted for a particular action at enforcement point A. The actor presents that authority twice. Both presentations can carry the same authentic signature, name the same target and arrive before expiry. Checking those facts alone does not distinguish a first use from a replay.

1. The decision service issues authority for request R and action X, naming A as audience.
2. A accepts the first use and remembers that the authority is consumed.
3. A refuses another use, even if every signed field is still valid.

The SingleUse property checks that an authority object never produces two effects. The deliberately broken replay configuration removes the memory of consumption; TLC then finds the violation the check expects. Presenting the authority at B is a different failure, caught by audience binding. Changing the target or parameters is different again, caught by matching admission and scope.

This distinction matters in implementation. Two workers cannot safely perform separate “unused?” checks and then both proceed. Their consumption decision must be coordinated. Restarting a worker must not make a spent authorization usable again. Those are implementation obligations; an atomic model step does not establish a durable, concurrent use store.

2. A stop request is not the same event as a stopped system

A control plane revokes authority while an enforcement point still has its earlier view. Before the update reaches that point, an effect can occur inside the permitted propagation window. Likewise, a halt request and an enforcement point’s acknowledgment are separate events.

Scroll the table sideways to read every column.

The witnesses explicitly demonstrate an effect inside the revocation window and after a halt request but before acknowledgment. These are permitted behaviors within the declared bounds, not evidence that revocation and halt are instantaneous. A deployment must choose and enforce bounds appropriate to the action’s consequence.

An outage has a similar distinction. The model does not permit a service failure to manufacture fresh permission. It can permit an effect on an admission issued before the outage, while that authority and the other controls remain valid inside the staleness bound. The outage witness makes that case visible.

3. “We will log it afterward” creates a missing-evidence state

Imagine making an effect in one step and appending its evidence in the next. Between those steps, the effect exists without its record. The non-atomic evidence variant makes exactly that separation, and the EffectHasEvidence invariant fails.

Putting the two operations in a single model transition states the property the design needs. It does not solve a distributed transaction. A database journal usually cannot commit atomically with a payment network or another remote service. The implementation must preserve durable recovery information before release and distinguish an attempted release, a confirmed effect and an outcome it cannot establish. An unanswered call is not proof that nothing happened, and an unresolved attempt must not silently become permission to repeat it.

The implementation requirements are discussed in the model-to-implementation mapping, including the final validity check, spent-use handling and MCP gateway recovery. This is where a useful model leads to more engineering work, rather than replacing it.

What “correct” means in these checks

A checker cannot decide what safety ought to mean. The authors state properties, and the checker asks whether the configured rules satisfy them. A missing property, a mistaken assumption or the wrong model of a deployment can all leave a real risk unexamined.

Safety: something forbidden never happens

The safety checks cover matching admission; authority scope, audience and validity; single use; halt and revocation limits; evidence and append-only history; supported admissions; the one-way rule; outage behavior; safe-state closure; and the types of model variables. The complete property catalogue maps each named property to its normative requirement identifiers.

The one-way rule deserves particular attention for AI systems. In this model, a favorable self-report or low risk score cannot turn an action denied by policy over verifiable inputs into an admission. Such inputs can make an outcome stricter; they cannot supply missing authority. Two broken variants deliberately let judgment or self-report admit, and both violate OneWayRule. This does not prove a model’s judgment truthful or settle whether a policy is wise. It constrains what the control design may do with those inputs.

Liveness: something required eventually happens

A system that never executes anything can look safe while being useless. A held request that waits forever is also not a successful outcome. The liveness configuration therefore checks three obligations: a held or challenged request eventually resolves or reaches its safe state; a submitted request eventually resolves or reaches its safe state; and every enforcement point eventually acknowledges a requested halt.

These properties rely on weak fairness for specified control-layer steps: time, refresh, halt acknowledgment and timeouts. Roughly, a continuously enabled required step cannot be postponed forever. No fairness is promised for the actor, human operators or outages. The model does not assume that an unavailable person eventually approves a request, or that a failed service inevitably comes back.

That difference between safety and liveness helps a buyer ask a better question than “did the model pass?” Ask which property was checked, under which scheduling assumptions, and which component is responsible for making progress.

Why some successful checks must find failures

The suite does not consist of 32 flawless TLA+ models. It has three kinds of configuration, each answering a different question.

Three correct configurations

The intended design should satisfy its selected properties. These separately exercise binding, control changes and liveness.

Twenty-two broken variants

Each removes a particular rule and must produce a counterexample to the property it protects. They cover bypasses, self-issued authority or decisions, evidence erasure, binding, replay, timeouts, outages, staleness, revocation, halt and the one-way rule. A missing expected counterexample is a failed check.

Seven reachability witnesses

These run the correct design and ask TLC to refute an assertion that a situation never occurs. Finding an effect, an authenticated resolution, an identifier-collision denial or a permitted control window demonstrates that the model can actually reach that situation.

The witnesses guard against an empty success: “no unauthorized action” would be less informative if no action were possible at all. The broken variants test whether particular checks react when the protections they are meant to examine are removed. They strengthen the evidence for those checks; they do not show that every possible modelling mistake or implementation defect would be detected.

All configurations, removed rules and witnessesThe 32 configuration files

What the finite configurations leave out

The binding configuration has two enforcement points, two request identifiers and four possible actions, only one allowed, through tick 3, with at most three request submissions. The control configuration has two enforcement points, one identifier and one allowed action through tick 4, with one submission and an outage, revocation, trust change and halt. The liveness configuration has one enforcement point and two actions, only one allowed, through tick 3, with at most two submissions.

Across the configurations, there are at most two targets and two parameter values. The decision and hold deadlines are one tick. In the control configuration the propagation bound is one tick, the staleness bound two ticks and the halt bound one tick. These are model constants, not a measurement in milliseconds or a production service-level promise. Liveness is checked without symmetry reduction, which can conceal liveness violations.

Small configurations make exhaustive exploration practical. They can expose a bad rule with just two competing uses or two enforcement points. They do not establish a cutoff theorem saying every larger system behaves the same way. A violation requiring more participants, different bounds or an omitted mechanism may remain outside the checked state space.

Important omissions are part of the result

• Policy content. Allowed actions are a set over verifiable inputs. Complex policy evaluation, obligations, budgets and comparisons between differently scoped admissions are not modelled.
• Physical time. There is one global discrete clock, no skew and no elapsed time inside an atomic transition. Real release-boundary timing needs separate evidence.
• Durability and uncertain outcomes. Neither model crashes a process, loses storage or times out a remote call whose effect may have happened.
• Other parts of the standard. Delegation chains, distributed workflows, evidence bundles and their verdicts, historical trust-policy handling, trusted-time countersignatures and extension handling are outside this TLA+ model.
• The deployment boundary. The correct model has no route around enforcement. Whether an actual AI system has another credential, endpoint or privileged path is something an assessor must establish in the real environment.

The abstraction table explains the reasons and consequences. An omission is not a waiver of the corresponding normative requirement.

What Tamarin adds about signed messages

The protocol model puts a network adversary between the enforcement point and decision point. It can read, replay, reorder and redirect messages, present signed responses with other actions, and reveal keys. The security statements name the key-compromise exceptions they rely on; they are not promises that a system remains trustworthy after every possible key compromise.

The correct protocol checks seven lemmas. The first, executable, establishes that an honest completed exchange exists with no key revealed; it is not a promise that every exchange completes. The other six concern a request’s named signer; an accepted response’s named decision-point issuer; the original request identifier, digest and audience; execution within the authorized scope, audience and window; single use of an authorization; and at most one effect per request identifier.

The key-reveal exceptions are property-specific. Authentication and binding lemmas make exceptions for the specified earlier signing-key compromise. The single_use and one_effect_per_request lemmas exclude traces containing the relevant response-key reveal, without restricting that exception to a reveal before execution. They must not be read as a universal replay guarantee up to the moment of compromise. The exact lemma formulas define those qualifications.

Eight separate flawed variants remove response-signature checking, role-key separation, request/response binding, scope checking, audience checking, consumption memory, message-identity handling or request-signature checking. Each must falsify the lemma selected for it. That is nine Tamarin checks in total, separate from the 32 TLC configurations.

Tamarin uses ideal signatures and hashes. Its trust policy supplies one key per principal and role, and its enforcement clock is an assumption. The validity check therefore concerns the signed window under that clock, not proof of true wall-clock time. Its consumption memory does not prove a deployed store survives crashes. Encoding defects, weak keys, side channels and mistakes in cryptographic code need other forms of examination.

The Tamarin modelThe seven lemmas, eight flaws and assumptions

What the published results actually say

The published record contains all 32 TLC configurations and nine Tamarin checks, each with its expected outcome. All 41 recorded checks match that expectation. For a correct configuration that means no selected violation; for a broken variant or witness it means the required counterexample was found. It does not mean “41 proofs that the system is safe.”

Scroll the table sideways to read every column.

These are three separate explored graphs, not numbers to add into a count of unique production states. The record also contains the expected counterexamples for 22 broken variants and seven witnesses. The correct Tamarin protocol verifies its seven lemmas; its eight flawed variants produce the expected falsifications.

The detailed guide identifies its table as the run of 5 October 2026. The historical JSON records Java 17.0.20.1; the reproduction guide recommends Java 21. The latter does not turn the older results into a Java 21 run. Runtime and some liveness-search counts are machine-dependent. No new model run is being claimed by this website update.

Each recorded check includes hashes of its model and configuration inputs. Those bind a result to particular source bytes and make stale records detectable. A matching digest does not authenticate a publisher, establish that the recorded execution happened or show that a deployment implements the model. Independent reproduction is a separate step.

Machine-readable results and input hashesComplete TLC and Tamarin result tables

What a real implementation still has to establish

A model can show the consequences of an ordering rule without showing that a particular program follows it. A deployment introduces threads, separate machines, storage commits, retries and operations the model treats as one step. The evidence must follow those differences.

At the release or effect boundary

Show how authority, scope, freshness, the validity window and current control state are checked. The normative timing arrangements include a release-boundary check, an explicitly permitted and enforced bound on the check-to-release delay, or checking authority at the point of effect. An earlier successful check is not automatically enough.

Across concurrent attempts and restarts

Show how uses are counted atomically across every instance that can act, how consumption survives recovery, and when a failed final check still leaves a use spent.

Across a remote call

Distinguish releasing the request, the remote effect and receiving the answer. Preserve recovery evidence durably before release where required. Keep outcomes unresolved when they cannot be established, without repeating an already-consumed use.

Across control failures

Measure and enforce the declared propagation, stale-state and halt bounds. Demonstrate the emergency path’s independence and behavior when the decision service is unavailable.

Across the real trust boundary

Establish key roles, credential custody, clock behavior, reachable effect paths, administrative separation and the scope of the conformance claim. The correct model’s assumptions cannot serve as evidence that those facts hold.

Conformance vectors exercise specified cases in code. Operational drills exercise a declared environment. An assessment examines the claim and its evidence. None of those should be relabelled as another one, and publishing a model is not certification. The conformance page explains what an implementation claim must actually state.

How to inspect or reproduce the work

Start with the property you care about. Read its definition, the transitions that can affect it, the configuration’s constants and the broken variant intended to challenge it. Then compare the expected result with the recorded one. This is more informative than treating the headline count as an assurance score.

The published runner requires Python 3.10 or later. The pinned tools are TLC 1.7.4, Tamarin 1.12.0 and Maude 3.5.1. The reproduction instructions give downloads, exact SHA-256 digests and setup requirements, including the Java 21 recommendation. They are optional maintainer tools, not installed as verifier-package dependencies.

From a local copy of Version 1.0 with the pinned tools available, a reviewer can select one configuration without implying a complete-suite run:

python3 formal/run_checks.py --only correct-control \
  --tla2tools /path/to/tla2tools.jar

To check all TLC configurations, omitting the separate protocol analysis:

python3 formal/run_checks.py --skip-tamarin \
  --tla2tools /path/to/tla2tools.jar

With the pinned Tamarin and Maude tools also available, the complete suite can retain its results outside the source tree:

python3 formal/run_checks.py \
  --tla2tools /path/to/tla2tools.jar \
  --tamarin /path/to/tamarin-prover \
  --maude-dir /path/to/maude-directory \
  --record /path/to/evidence/formal-results.json

A --record update can retain results for checks not selected in that invocation; inspect which checks actually ran before calling the output fresh. --readme regenerates result tables; it does not execute the models. The runner source defines the selection and recording behavior.

The source behind this explanation

Version 1.0 links below use the public release tag v1.0, rather than a moving branch. The current contribution and issue routes use the public repository. This explanation was checked against public source commit afd868b9a18fce1400cbc2826edd9a96449ae5b1.

• ECLCore.tla: state, transitions, properties and selectable flaws.
• MC.tla and all configurations: concrete values, bounds and reachability checks.
• DCMP2_Binding.spthy: signed-message protocol and its lemmas.
• run_checks.py and results.json: tool pins, expectations and recorded evidence.
• The technical guide: complete property/requirement mappings, configurations, results, assumptions and reproduction details.
• The specification and conformance requirements: the governing text and the implementation evidence it calls for.

If you find an incorrect property, an omitted behavior or a mismatch between model and text, open an issue with the relevant configuration and requirement identifier. For a vulnerability, use the repository’s current private reporting instructions rather than posting sensitive details publicly.