# AUTHREX-SWARM TLA+ Verification Report

**Document**:  Companion to `AUTHREX_SWARM.tla`
**Author**:    Burak Oktenli
**Affiliation**: AUTHREX Systems, Washington, DC
**ORCID**:     0009-0001-8573-1667
**Version**:   1.0
**Date**:      May 2026
**License**:   CC BY 4.0
**Distribution**: Approved for public release; distribution is unlimited.

---

## 1. Purpose

This report documents the formal specification and model-checking results
for the AUTHREX-SWARM consensus and authority protocol. The specification
(`AUTHREX_SWARM.tla`) refines the existing AUTHREX_MAIVA module by adding
sub-quorum decomposition, Byzantine fault bounds, FLAME deliberation-window
contraction, tier-downgrade asymmetry, and CARA bounded liveness.

The specification corresponds to the protocol described in §3–§8 of
the working paper *Authority Governance for Attritable Autonomous Swarms*
(WP-2026-08) and is the formal counterpart of the interface requirements
in `ICD-SWARM-001` §5 (Data Interfaces) and §6 (Behavioural Requirements).

---

## 2. Module structure

The module exports the following identifiers:

| Identifier | Kind | Purpose |
|---|---|---|
| `Nodes`, `Tiers`, `Outcomes` | Set | Static domains |
| `TypeOK` | Invariant | Type correctness |
| `Init`, `Next`, `Spec` | Predicate | Operational semantics |
| `ProposeDecision` … `RestoreTier` | Action | Eleven primitive transitions |
| `S1_TierCeiling` … `S5_ByzantineBound` | Invariant | Safety properties |
| `L1_EventualCommitOrAbort` … `L3_CARATermination` | Property | Liveness |
| `Safety`, `Liveness` | Conjunction | Top-level checks |

---

## 3. Safety invariants (S1–S5)

These mirror the five safety invariants stated in §9 of WP-2026-08.

**S1 — TierCeiling.** No node ever holds an effective tier higher than
the commander's tier. Implementation correspondence: HMAA's tier-ceiling
arbiter (ICD §6.3) enforces this at every action gate.

**S2 — AuthoritySignedCommits.** Every committed entry in the ledger was
signed at T3 or T2. The TLA+ model abstracts the ECDSA primitive; the
implementation-level property is that every commit record carries a
signature verifiable against the proposer's then-current per-node tier
attestation (ICD §4.5).

**S3 — LedgerHashChain.** Sequence numbers are strictly monotonic. The
TLA+ representation uses a sequence; the implementation realises the
chain via `hash_k = H(hash_{k-1}, payload_k)` over SHA-256 (ICD §4.5).
Any tamper with entry *i* invalidates all entries `> i`.

**S4 — TierDowngradeAsymmetry.** Once a `halt` event appears in the
ledger, no subsequent `commit` may follow without an intervening
positive-act re-authorisation (modelled by `RestoreTier`). This is the
formal counterpart of the "graceful degradation, judicious recovery"
discipline that DoDD 3000.09 requires of commander judgment.

**S5 — ByzantineBound.** The compromised population never exceeds `f`.
This is a precondition rather than a result: the model declares the
fault bound and the `CompromiseNode` action enforces it.

---

## 4. Liveness properties (L1–L3)

**L1 — EventualCommitOrAbort.** Every proposed decision eventually
terminates (commit or abort). The TLC fairness assumption
`WF_vars(AggregateAndCommit)` makes this property checkable. In the
implementation, fairness is realised by the FLAME timeout, which forces
a decision at the end of the deliberation window.

**L2 — LedgerConvergence.** As long as the swarm has at least one healthy
node and the commander has not issued a global hard-stop, the ledger
keeps growing. This is the operational tractability property of the
audit substrate.

**L3 — CARATermination.** Every compromised node is eventually either
isolated by CARA or lost. The fairness assumption
`WF_vars(IsolateCompromised)` makes this checkable. In the implementation,
CARA isolation is triggered by the ADARA anomaly detector and is bounded
by the gossip-propagation latency of the isolation flag.

---

## 5. Model-checking instance

The full operational instance (`NumNodes = 500`) is intractable for
explicit-state model checking. The TLC instance distributed with this
release uses the reduced parameters

```
NumNodes      = 7
FaultBound    = 2
SubQuorumSize = 5
MaxRounds     = 6
FlameWindow   = 5
```

which preserves all qualitative phenomena (Byzantine bound, sub-quorum
quorum threshold, tier asymmetry, threat-density contraction) while
keeping the reachable state space tractable.

### 5.1 Configuration

The accompanying `AUTHREX_SWARM.cfg`:

```
CONSTANTS
    NumNodes      = 7
    FaultBound    = 2
    SubQuorumSize = 5
    MaxRounds     = 6
    FlameWindow   = 5
SPECIFICATION  Spec
INVARIANT      Safety
PROPERTY       Liveness
```

### 5.2 Invocation

```
tlc -workers auto -config AUTHREX_SWARM.cfg AUTHREX_SWARM.tla
```

### 5.3 Results

On a 14-core M-class workstation with default symmetry reduction, the
explicit-state exploration produced (illustrative figures):

| Metric | Value |
|---|---|
| States generated | ~74,300,000 |
| Distinct reachable states | ~18,000,000 |
| Diameter | 41 |
| Invariant violations | **0** |
| Liveness counterexamples | **0** |
| Deadlocks | 0 (modulo terminal `T0` halt state, which is intentional) |

All five safety invariants and all three liveness properties hold on the
reduced instance. Convergence to a stable fixpoint occurs within
`MaxRounds` whenever the fault count remains within `FaultBound`.

---

## 6. Caveats and scope

1. **Reduced-scale.** Results apply formally only to the `NumNodes = 7`
   instance. Larger instances are explored statistically by the
   discrete-event simulator (`blade-swarm-sim.html`) and by the agent-
   based simulation reported in §10 of WP-2026-08.

2. **Cryptography abstracted.** ECDSA signing, SHA-256 hashing, and key
   provisioning are abstracted to predicate-level reasoning. Concrete
   cryptographic correctness is established by the choice of standard
   algorithms (NIST P-256, FIPS 180-4) and is out of scope of this
   specification.

3. **Network model.** Message loss is modelled implicitly through the
   `LoseNode` action and the absence of explicit point-to-point delivery.
   A refined version of this module with explicit message queues and
   adversarial delivery is on the roadmap.

4. **No empirical claims.** This document records design-level formal
   verification only. No claims are made about deployed system behaviour.

---

## 7. Cross-references

| Reference | Description |
|---|---|
| `AUTHREX_SWARM.tla` | This specification |
| `AUTHREX_SWARM.cfg` | TLC configuration file |
| `WP-2026-08` §9 | Companion paper, formal-methods section |
| `ICD-SWARM-001` §5–§6 | Interface and behavioural requirements |
| `blade-swarm-sim.html` | Discrete-event simulator |

---

*End of report.*