Formal model artifacts
Evidence class: MODEL CHECKED (bounded). A TLA+ specification of the governance model was checked exhaustively over a deliberately small configuration. This is a result about the specification. It is not a proof about the running Python implementation, and no refinement relation between the two has been established. It is not a formal proof over an unbounded domain, and it is not a statement that any application built on AxiomGate is secure.
The run
| Tool | TLC2 version 2026.08.21.155922 (rev 9787e65), tla2tools.jar |
|---|---|
| Java | OpenJDK 17.0.20.1 |
| Specification | GovernanceMCV6.tla, extending GovernanceV6, GovernanceInvariantsV6 and GovernanceTransitionsV6 |
| Configuration | GovernanceMCV6.cfg — Authority = {auth1}, Entity = {ent1}, Actions = {act1, act2}, Resources = {res1, res2} |
| Invariants checked | GovernanceSecurityBoundary (I1–I10) and TypeInvariant |
| Command | java -cp tla2tools.jar tlc2.TLC -config GovernanceMCV6.cfg -workers auto -deadlock -cleanup GovernanceMCV6 |
| Result | Model checking completed. No error has been found. |
| States generated | 373,933 |
| Distinct states | 345,322 |
| States left on queue | 0 — the bounded state space was exhausted |
| Search depth | 11 |
| Run timestamp (UTC) | 2026-09-18T14:24:05Z, finished in 5 seconds |
Bounds and assumptions
- The configuration is deliberately minimal: one authority, one entity, two actions, two resources. A result over this configuration does not generalise to arbitrary sizes.
- The next-state relation is additionally bounded — uid counter under 2, observation log under 3, enforcement log under 3 — so that the state space terminates.
-deadlockdisables deadlock reporting. Without it the search halts on an expected terminal state at depth 8. That behaviour is itself asserted by AxiomGate's own verification script, so it is a known property of the model rather than an unreported failure.- TLC reports a fingerprint-collision probability of roughly 3.9×10-9 for this run. Exhaustiveness is therefore near-certain, not certain.
Published files
| File | SHA-256 |
|---|---|
| GovernanceV6.tla | 6f27bebc7fa3830cf566ba21c0959840e2a33a9dbc1050f732c2db50aa417778 |
| GovernanceInvariantsV6.tla | a7371b51bbe89c6e745b4991526958571b1f87ef493e67a3bc92b8acccdb662c |
| GovernanceTransitionsV6.tla | 70504673a7fa44177346fbe73ec72debe8ad88fc2fb24e2ddd6b9f02ddbd359c |
| GovernanceMCV6.tla | 51aa043b4ece485fb2d540d1dd35d9ca46e901350c67042b1a7e6a26130d337c |
| GovernanceMCV6.cfg | e25a19d5185a1cc8c64e27a2b65c13bf2c5b42e171a1e826c12385c1ef4056ea |
| tlc-run-2026-09-18.log | 138e7f021be1edc69e1a6d3b12c473d48e57d90965e07c84b244754f486c2c90 |
What is not published here
One further specification exists in the AxiomGate repository that has never been model checked. It defines invariants but ships no configuration, and no TLC run has ever been performed against it. It is deliberately withheld rather than published, because an unchecked specification is not evidence and listing it would make this proof surface look larger than it is.
Reproduce
mkdir tlc && cd tlc
curl -O https://axiomgate.org/formal/GovernanceV6.tla
curl -O https://axiomgate.org/formal/GovernanceInvariantsV6.tla
curl -O https://axiomgate.org/formal/GovernanceTransitionsV6.tla
curl -O https://axiomgate.org/formal/GovernanceMCV6.tla
curl -O https://axiomgate.org/formal/GovernanceMCV6.cfg
java -cp tla2tools.jar tlc2.TLC -config GovernanceMCV6.cfg \
-workers auto -deadlock -cleanup GovernanceMCV6Compare your output against the published run log. State counts are a property of the specification and configuration, so they should match exactly.