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. Bonis Systems publishes its specs 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

Knox receipts — legal posture

Knox receipts have not yet been tested in litigation. The cryptographic primitives — Merkle proofs, hash chains, and Ed25519 / P-256 signatures — are well-established and standardized (RFC 8785 for canonical JSON, RFC 8032 for Ed25519, RFC 6979 for deterministic ECDSA). External Bitcoin anchoring uses the OpenTimestamps protocol (opentimestamps.org). The legal admissibility of any specific receipt format depends on jurisdiction, judge, and case posture. Bonis Systems LLC makes no representation that a Knox receipt will be admitted in any particular proceeding.