Lucio Durán
lucioduran.com

Projects / Agent Policy State Machine

Agent Policy State Machine

An executable authorization state machine with finite TLA+ safety checks, compensation and replay of the actual TLC transition graph.

Author: · Python 3.14.7, Java 17.0.17 and TLC 2.19 · License: MIT

Page published: · Page updated:

Repository · TLC measurement metadata · Release v0.1.0

Problem and relevance to agents

An agent can plan an action without permission to execute it. Retries, late results and failed compensation also need an explicit policy before effects occur.

A serialized runtime enforces approval and effect accounting for one synthetic operation, while a separate formal model exposes invalid transition paths.

Architecture

  1. Constrain the operation. An opaque approval capability gates one in-memory unit effect. Accepted event IDs are deduplicated inside the same critical section.
  2. Explore the finite model. TLC checks types, authorization, accounting, rollback and terminal stability across nine event symbols and nine phases.
  3. Compare model and runtime. A graph parser replays a representative path to every node and each outgoing edge, then checks the runtime against the exported model state.

What this demonstrates

  • Real TLC exploration with a deliberately faulty authorization path and a retained counterexample.
  • Agreement on all 981 exported graph edges and an executable regression that blocks the unauthorized effect.
  • Twenty-two runtime and conformance tests, including concurrent dispatch, conflicts, invalid capabilities and compensation recovery.

Published results

The recorded local checks used an Intel Xeon W-3223, 48 GiB RAM and macOS 26.7.1 on November 9, 2026.

TLC ran with one worker, one active processor and a 512 MiB heap. The correct finite graph was exhausted without a depth cutoff. The faulty configuration enabled execution before approval and stopped on an authorization violation.

Finite model checking

README and reproduction ·
MeasurementObserved result
Generated / distinct states982 / 109
Search depth / remaining queue8 / 0
Faulty-model exit code12
Correct / faulty TLC wall time1.085 / 1.085 s

Runtime conformance

Runtime replay metadata ·
MeasurementObserved result
Conforming graph edges981 / 981
Unauthorized counterexampleBlocked
Replay wall time0.138 s

These observations establish safety within the finite abstraction and edge agreement from representative histories. They do not prove refinement for every runtime history, liveness or unbounded correctness.

Wall times include JVM or Python startup and are single observations. Peak RSS, energy, billing and performance variance were not measured.

The repository preserves the initial parser error and graph-parser failure separately from the successful checks. README and reproduction.

Reproduce

Use uv 0.8.23 and Python 3.14.7. The setup command creates a repository-local environment; uv must be able to locate the matching interpreter. Install that Python version first if it is unavailable in uv's download catalog. Initial setup and test dependencies may need Internet access. Replay uses only the standard library. Regression tests use the frozen uv lockfile. Java and the separately downloaded TLC JAR are needed only for fresh model checking.

After environment setup, the replay command works offline. The replay command verifies hashes and replays saved evidence without Java or model checking. The second block runs the small regression suite. Follow the README for fresh TLC measurements, using the shared benchmark_lock.py wrapper on the original host and exclusive scheduling elsewhere.

Verify saved evidence

git clone https://github.com/lucioduran/agent-policy-state-machine.git
cd agent-policy-state-machine
git checkout bb96a1ace19ac0c7a90fb0e1059a2a58f6b06c70
UV_CACHE_DIR="$PWD/.tools/uv-cache" UV_PYTHON_INSTALL_DIR="$PWD/.tools/python" uv venv --python 3.14.7 .venv
PYTHONPATH=src .venv/bin/python scripts/replay.py

Run regression tests

UV_CACHE_DIR="$PWD/.tools/uv-cache" UV_PYTHON_INSTALL_DIR="$PWD/.tools/python" uv sync --frozen --python 3.14.7
.venv/bin/pytest -q

Scope and limitations

  • The model covers one operation and one stable ID per event symbol. Fresh-ID conflicts and actual threading are tested outside the formal abstraction.
  • The effect and compensation are synthetic in-memory ledger changes. There is no crash recovery, external tool adapter, durable journal or distributed exactly-once guarantee.
  • Trusted application code must keep the approval capability private. The CLI supplies its own capability and is a demonstration, not an authentication service.
  • Compensation may remain unresolved. No fairness or liveness guarantee is claimed, and saved hash consistency is not independent measurement attestation.

Sources and revision

The model check used commit 9a8273d57ecf691f5dc36207f2ce4877875f1dd4, starting at the report timestamp below. Runtime replay used commit 30aa48bfe943dc84b8ae2cdf8fde74e138046f13 at 2026-11-09T20:20:14.821954+00:00. The final release adds tests and documentation; its manifest binds the measured model and runtime files to the published revision.