# Knox Formal Specification

**Operator:** Bonis Systems LLC (Wyoming, UEI R2BPJDC5CBA3, CAGE 1TSP2)
**USPTO Provisional Application:** 64/038,359 (inventor of record: Jonis Aaron Fields; assignment to Bonis Systems LLC scheduled post-revenue via IP counsel)
**Specs finalised:** 2026-04-18

## What this directory proves

Two TLA+ specifications cover the two load-bearing pipelines in the Knox stack. Both have been exhaustively model-checked by TLC over bounded state spaces, and both terminated with **no invariant violations and no counter-examples**.

TLA+ is the temporal logic used by AWS to verify S3 and DynamoDB, by Microsoft to verify Cosmos DB, and by NASA for spacecraft flight software. A model-checked TLA+ spec is as close to "mathematically proved correct" as operational systems get outside of theorem provers.

### 1. `knox_anchor_chain.tla` — the Knox per-apiKey anchor chain

Models `src/lib/knox-baas.ts: anchorEvent()` and the hourly Bitcoin-anchoring cron (`/api/cron/knox-anchor-hourly`).

**Invariants verified:**

| Invariant | What it says |
|---|---|
| `SequenceMonotonic` | Anchor `sequence` is `0..k` contiguous, no gaps. |
| `HashChainIntegrity` | Each anchor's `previousHash` equals the prior anchor's `payloadHash`; the head anchors to `NULL`. |
| `UniqueHashes` | No two anchors in a chain share a `payloadHash`. |
| `TypeInvariant` | All fields hold their declared types. |

**Liveness property verified:**

| Property | What it says |
|---|---|
| `OtsProgress` | Every anchored payload eventually transitions from `pending` to `otsCommitted` (fairness assumption: the cron worker runs infinitely often). |

**Run result:**

- 1,425 states generated, 633 distinct
- Search depth 9
- No errors; all invariants and the temporal property hold.

Full TLC log: [`tlc_knox_anchor_chain.log`](tlc_knox_anchor_chain.log)

### 2. `core_event_store.tla` — the Core Event Store

Models `src/lib/event-store.ts: emit(), replay(), snapshot()` and the Merkle checkpoint roller.

**Invariants verified:**

| Invariant | What it says |
|---|---|
| `PerAggregateMonotonic` | Within each aggregate, sequence is `0..k` contiguous. |
| `GlobalMonotonicUnique` | `globalSequence` is unique and strictly increasing across the entire log. |
| `HashChainIntegrity` | Per-aggregate hash chain is unbroken. |
| `IdempotentUnique` | No two events share `(aggregateType, aggregateId, idempotencyKey)` when the key is non-null. |
| `ReplayDeterministic` | `EventsFor(aggregateId)` is a deterministic function of the log — two replays at the same cutoff return the same subsequence. |
| `TypeInvariant` | All fields hold their declared types. |

**Run result:**

- 59,465 states generated, 19,609 distinct
- Search depth 5
- No errors; all invariants hold.

Full TLC log: [`tlc_core_event_store.log`](tlc_core_event_store.log)

## How to re-verify

Anyone can re-run both model checks from a fresh machine:

```bash
# 1. Install Java 17+
brew install openjdk@17                       # macOS
#   or: apt-get install openjdk-17-jdk        # Debian/Ubuntu

# 2. Download the TLA+ toolbox
curl -L -o tla2tools.jar \
  https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar

# 3. Run the model checkers
cd spec/
java -jar tla2tools.jar -config knox_anchor_chain.cfg knox_anchor_chain.tla
java -jar tla2tools.jar -config core_event_store.cfg core_event_store.tla
```

Both should terminate with `Model checking completed. No error has been found.`

## Scope and honest limits

These are bounded model checks over small state spaces (MaxAnchors = 4 for the anchor spec, MaxEvents = 4 across 2 aggregates for the event store spec). Bounded model checking is not full proof — it exhaustively verifies a finite sub-model. The specifications themselves are abstractions of the production code; we treat SHA-256 as an idealised injective function (standard crypto abstraction), database transactions as atomic (the production code uses Serializable isolation to approximate this), and we do not model Bitcoin reorg depth (treated as a single "confirmed" event once OpenTimestamps settles).

The value is in the **invariants themselves**: they are the exact properties the production code is designed to uphold, and a TLA+ proof against the abstract model catches whole classes of design errors — off-by-one sequencing, hash-chain forking under retry, idempotency leaks under concurrent emit, deadlocks — before they can be introduced by a future code change.

## What this unlocks

- **Federal / Treasury / DoD buyers**: a model-checked TLA+ spec is table-stakes for FedRAMP High, DoD Impact Level 5, and CMMC Level 3 reviews. Most commercial vendors never produce one.
- **Court admissibility**: regulators and opposing counsel can re-run the model checker. The invariants are written in plain English in this README and in machine-checkable form in the `.tla` files. Both chains of argument converge.
- **Insurance / audit**: cyber-insurance underwriters and SOC-2 auditors can cite the TLC output as evidence of design-level correctness that goes beyond code review.

## Ownership

Specification text is © 2026 Bonis Systems LLC. The technical primitive the specifications describe is covered by USPTO provisional application 64/038,359, for which Jonis Aaron Fields (founder) is the named inventor of record; assignment to Bonis Systems LLC is scheduled post-revenue via IP counsel. The specification files are public so that regulators, customers, and security researchers can independently verify them. The proving ceremony for the Phase-1 ZK circuit is documented separately in [`../zk/CEREMONY.md`](../zk/CEREMONY.md).