TLA+ · Temporal Logic of Actions

Not “trust me.” Mathematical proof.

Knox uses the same formal-verification toolchain AWS uses for S3 and DynamoDB, Microsoft uses for Cosmos DB, and NASA uses for spacecraft flight software. Both load-bearing pipelines are machine-checkable by any reader in under five minutes.

Download README

Most commercial vendors never produce a formal specification. We publish ours so that regulators, customers, and security researchers can independently re-verify.

Knox Anchor Chain

No error

knox_anchor_chain.tla

Invariants: 4 + 1 temporal
States generated: 1,425
Distinct states: 633
Search depth: 9

Core Event Store

No error

core_event_store.tla

Invariants: 6
States generated: 59,465
Distinct states: 19,609
Search depth: 5

Knox Anchor Chain — invariants proved

SequenceMonotonic

Anchor sequence is 0..k contiguous. No gaps.

HashChainIntegrity

previousHash equals the prior anchor's payloadHash.

UniqueHashes

No two anchors in a chain share a payloadHash.

TypeInvariant

All fields hold their declared types.

OtsProgress

Temporal: every anchored payload eventually transitions from pending to otsCommitted.

Core Event Store — invariants proved

PerAggregateMonotonic

Within each aggregate, sequence is 0..k contiguous.

GlobalMonotonicUnique

globalSequence is unique and strictly increasing.

HashChainIntegrity

Per-aggregate hash chain is unbroken.

IdempotentUnique

No duplicate events for the same (agg, id, idempotencyKey).

ReplayDeterministic

Replay is a pure function of the event log.

TypeInvariant

All fields hold their declared types.

Re-verify in your own terminal

brew install openjdk@17

curl -L -o tla2tools.jar \
  https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar

curl -o knox_anchor_chain.tla https://bonissystems.com/spec/knox_anchor_chain.tla
curl -o knox_anchor_chain.cfg https://bonissystems.com/spec/knox_anchor_chain.cfg

java -jar tla2tools.jar -config knox_anchor_chain.cfg knox_anchor_chain.tla
# Expected: "Model checking completed. No error has been found."

Artifacts

knox_anchor_chain.tlaspec, 160 lines
knox_anchor_chain.cfgTLC configuration
tlc_knox_anchor_chain.logcaptured proof run
core_event_store.tlaspec
core_event_store.cfgTLC configuration
tlc_core_event_store.logcaptured proof run
README.mdhuman-readable summary