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 (GUI + TLC model checker).

Running the Model Checker

All specs at once

cd formal-verification
./run_all.sh

Individual specs (command line)

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.

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.

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.