Baradb/formal-verification/README.md

# BaraDB Formal Verification Suite

**Version:** 1.0.0 (see VERSION)

This directory contains TLA+ specifications for core BaraDB distributed-systems algorithms. These specifications serve as machine-checkable certificates of correctness for the most critical consensus, transaction, replication, membership, concurrency, and sharding protocols.

## Structure

| File | Algorithm | Key Properties |
|------|-----------|----------------|
| `raft.tla` | Raft Consensus | Election safety, leader append-only, state-machine safety, log matching, leader completeness |
| `twopc.tla` | Two-Phase Commit | Atomicity (all commit or all abort), no orphan blocks, coordinator consistency |
| `mvcc.tla` | MVCC / Snapshot Isolation | Read-own-writes, no dirty reads, write-write conflict, read stability, snapshot isolation |
| `replication.tla` | Async / Sync / Semi-sync Replication | Monotonic LSN, sync durability, semi-sync quorum, applied <= current |
| `gossip.tla` | SWIM Gossip Protocol | Alive-not-falsely-dead, incarnation monotonicity, dead consistency |
| `deadlock.tla` | Deadlock Detection | Cycle detection correctness, victim selection consistency, graph integrity |
| `sharding.tla` | Consistent Hash Sharding | Virtual node mapping, node assignment consistency, vnode ordering |

## Prerequisites

- Java Runtime Environment (JRE) 8+ — the bundled `tla2tools.jar` contains TLC and SANY.
- Or [TLA+ Toolbox](https://lamport.azurewebsites.net/tla/toolbox.html) (GUI + TLC model checker).

## Verified State Space (v1.1.4)

| Spec | States Generated | Distinct States | Depth |
|------|-----------------|-----------------|-------|
| raft.tla | 3,031,684 | 833,024 | 47 |
| twopc.tla | 22,855,681 | 2,097,152 | 31 |
| mvcc.tla | 177,849 | 59,860 | 13 |
| replication.tla | 3,687,939 | 490,560 | 22 |
| gossip.tla | 1,257,121 | 110,592 | 28 |
| deadlock.tla | 3,767,361 | 263,950 | 9 |
| sharding.tla | 186,305 | 23,296 | 11 |
| **Total** | **34,963,940** | **3,878,434** | — |

## Running the Model Checker

### All specs at once
```bash
cd formal-verification
./run_all.sh
```

### Individual specs (command line)
```bash
cd formal-verification

# Syntax check (parse)
java -cp tla2tools.jar tla2sany.SANY raft.tla

# Model check with small parameters
java -cp tla2tools.jar tlc2.TLC -config models/raft.cfg raft.tla
java -cp tla2tools.jar tlc2.TLC -config models/twopc.cfg twopc.tla
java -cp tla2tools.jar tlc2.TLC -config models/mvcc.cfg mvcc.tla
java -cp tla2tools.jar tlc2.TLC -config models/replication.cfg replication.tla
java -cp tla2tools.jar tlc2.TLC -config models/gossip.cfg gossip.tla
java -cp tla2tools.jar tlc2.TLC -config models/deadlock.cfg deadlock.tla
java -cp tla2tools.jar tlc2.TLC -config models/sharding.cfg sharding.tla
```

### GUI (TLA+ Toolbox)
1. Open the Toolbox.
2. `File → Open Spec → Add New Spec…` → select a `.tla` file.
3. Create a new model (`TLC Model Checker → New Model`).
4. Click the green play button to verify all invariants and temporal properties.

## Verified Properties

### raft.tla
- `ElectionSafety` — at most one leader per term.
- `LeaderAppendOnly` — a leader never produces invalid log entries.
- `StateMachineSafety` — if a node has committed a log entry at a given index, no other node has a different entry for the same index.
- `CommittedIndexValid` — commitIndex never exceeds the node's log length.
- `LogMatching` — if two logs contain an entry with the same index and term, all preceding entries are identical.

### twopc.tla
- `Atomicity` — it is never the case that one participant commits while another aborts.
- `NoOrphanBlocks` — once a transaction is committed, every participant is committed.
- `CoordinatorConsistency` — once the coordinator decides, it never changes the decision.
- `NoDecideWithoutConsensus` — coordinator only decides when all votes are collected.
- `ParticipantStateValid` — participant states are consistent with the coordinator decision.

### mvcc.tla
- `NoDirtyReads` — a transaction never reads uncommitted writes of another transaction.
- `ReadOwnWrites` — a transaction always reads its own writes.
- `WriteWriteConflict` — no two committed transactions write the same key (first-committer-wins).
- `CommittedMustStart` — committed transactions have a valid start timestamp.
- `CommittedVersionsUnique` — no two committed versions for a key share the same txnId.
- `NoWriteSkew` — no two committed transactions have a circular read-write dependency.

### replication.tla
- `MonotonicLsn` (temporal) — the applied LSN never decreases.
- `AcksRemovePending` — a replica that acked an LSN is no longer pending for it.
- `PendingAreKnown` — all pending acks reference valid replica IDs.
- `AppliedLteCurrent` — applied LSN never exceeds current LSN.

### gossip.tla
- `AliveNotFalselyDead` — an alive member is never reported as dead by any peer.
- `IncarnationMonotonic` — incarnation numbers only increase.
- `DeadConsistency` — once dead, a node knows it is dead (self-consistency).

### deadlock.tla
- `GraphIntegrity` — all edges reference known transaction IDs.
- `NoSelfLoops` — no transaction waits on itself.

### sharding.tla
- `VirtualNodeMapping` — each vnode maps to Nil or a valid shard.
- `NodeAssignmentConsistency` — node-to-shard assignments are well-formed.
- `VnodeOrdering` — virtual nodes are assigned in monotonic position order.

## Extending

To add a new algorithm:
1. Write the TLA+ spec (preferably with PlusCal for readability).
2. Define invariants that capture the safety properties you need.
3. Add a `<name>.tla` file and a matching `<name>.cfg` in `models/`.
4. Run TLC and confirm `No error has been found.`
5. Add the command to `run_all.sh`.
6. Update this README.