baraba/Baradb
1
1
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
0c7847abbaa87a6d284c8705af15959cdebe11ad
Baradb/formal-verification/CHANGELOG.md
T
dimgigov 8f87491eca FV-14: TLA+ faithfulness tests for Nim state machines 
Add tests/tla_faithfulness.nim verifying Nim code against TLA+ invariants:
- Raft: ElectionSafety, LogMatching, CommittedIndexValid
- MVCC: NoDirtyReads, CommittedMustStart
- 2PC: Atomicity, RecoveryConsistency

Documented gap: Nim MVCC allows multiple committed versions per key,
while TLA+ spec enforces first-committer-wins (WriteWriteConflict).
This test ensures future changes to Nim code maintain alignment with specs.

Update PLAN.md (FV-14 done), CHANGELOG.md, test_all.nim includes new suite.
2026-05-07 21:59:06 +03:00

5.6 KiB
Raw Blame History

BaraDB Formal Verification Changelog

[1.2.0] — 2026-05-07

Added (Software verification bridge)

  • tests/tla_faithfulness.nim — Nim test suite verifying that Nim state machines obey TLA+ invariants:
    • Raft: ElectionSafety, LogMatching, CommittedIndexValid
    • MVCC: NoDirtyReads, CommittedMustStart
    • 2PC: Atomicity, RecoveryConsistency
  • Documented gap: Nim MVCC allows multiple committed versions per key (TLA+ enforces first-committer-wins)

Added

  • raft.tla: Heartbeat, HeartbeatTimeout, LeaderLeaseExpired actions — models leader step-down when quorum is lost
  • raft.tla: LeaderHasSelfHeartbeat invariant — every leader must have a valid heartbeat in its own term
  • raft.tla: heartbeatReceived variable tracks last term in which each node received a heartbeat

Improved

  • raft.tla: Heartbeat causes recipients to step down if they see a higher term (realistic AppendEntries behavior)

Model Checker Configs (v1.2.0)

Spec Model Bounds States Checked Properties
raft 3 nodes, MaxTerm=3, MaxLogLen=3 38,051,647 7 invariants + fair execution
twopc 3 participants, MaxTxnId=3 22,855,681 7 invariants + fair execution
mvcc 2 keys, 2 values, MaxTxnId=2 177,721 7 invariants + 1 liveness
replication 3 replicas, MaxLsn=3, MaxSyncCount=2 3,687,939 4 invariants + 1 temporal
gossip 3 nodes, MaxIncarnation=3 692,497 4 invariants + fair execution
deadlock 5 txns, MaxEdges=8 3,767,361 2 invariants
sharding 3 shards, 2 nodes, 5 vnodes 186,305 3 invariants

[1.1.0] — 2026-05-07

Added

  • mvcc.tla: NoWriteSkew invariant — detects cyclic read-write dependencies (write skew) via readPredicate tracking
  • twopc.tla: coordinatorLog (persistent WAL), coordinatorAlive, CrashCoordinator, RecoverCoordinator — models coordinator crash/recovery correctly
  • twopc.tla: ParticipantTimeout — participant aborts only when coordinator is crashed AND undecided (coordinatorLog = Nil)
  • mvcc.tla: CommitProgress liveness property — any transaction that writes eventually commits or aborts (verified with WF_vars(Next))
  • raft/twopc/mvcc/gossip: Spec definition with WF_vars(Next) — all models now enforce fair execution

Improved

  • raft.tla: HasCompatiblePrefix check implements real prevLogIndex/prevLogTerm validation from raft.nim:190-197
  • raft.tla: RejectAppendEntries action + conflict truncation in Replicate — LogMatching invariant restored
  • gossip.tla: LearnViaGossip now uses strength operator to prevent overwriting stronger state (Dead/Suspect) with weaker (Alive/Suspect)
  • raft.tla: AppendEntry guard ensures term continuity — prevents gaps in leader log terms

Infrastructure

  • CI: Replaced container: eclipse-temurin with actions/setup-java@v4 + actions/cache@v4 + continue-on-error: true

Model Checker Configs (v1.1.0)

Spec Model Bounds States Checked Properties
raft 3 nodes, MaxTerm=3, MaxLogLen=3 3,031,684 6 invariants + fair execution
twopc 3 participants, MaxTxnId=3 22,855,681 7 invariants + fair execution
mvcc 2 keys, 2 values, MaxTxnId=2 177,721 7 invariants + 1 liveness
replication 3 replicas, MaxLsn=3, MaxSyncCount=2 3,687,939 4 invariants + 1 temporal
gossip 3 nodes, MaxIncarnation=3 692,497 4 invariants + fair execution
deadlock 5 txns, MaxEdges=8 3,767,361 2 invariants
sharding 3 shards, 2 nodes, 5 vnodes 186,305 3 invariants

[1.0.0] — 2026-05-07

Added

  • raft.tla — Raft consensus: ElectionSafety, LeaderAppendOnly, StateMachineSafety, CommittedIndexValid
  • twopc.tla — Two-Phase Commit: Atomicity, NoOrphanBlocks, CoordinatorConsistency, NoDecideWithoutConsensus, ParticipantStateValid
  • mvcc.tla — MVCC / Snapshot Isolation: NoDirtyReads, ReadOwnWrites, WriteWriteConflict, CommittedMustStart, CommittedVersionsUnique
  • replication.tla — Async/Sync/Semi-sync Replication: MonotonicLsn, AcksRemovePending, PendingAreKnown, AppliedLteCurrent
  • gossip.tla — SWIM-like Gossip Protocol: AliveNotFalselyDead, IncarnationMonotonic, DeadConsistency
  • deadlock.tla — Deadlock Detection: GraphIntegrity, NoSelfLoops
  • sharding.tla — Consistent Hashing Sharding: VirtualNodeMapping, NodeAssignmentConsistency, VnodeOrdering

Improved

  • raft.tla: Increased from 6 invariants (TypeOk included) to 5 verified properties with cleaner semantics
  • twopc.tla: Added 3 new invariants (CoordinatorConsistency, NoDecideWithoutConsensus, ParticipantStateValid), increased model to MaxTxnId=3
  • mvcc.tla: Added CommittedMustStart, CommittedVersionsUnique; removed incorrect ReadStability
  • replication.tla: Added AppliedLteCurrent, SemiSyncQuorum; simplified SyncDurability for model checking

Infrastructure

  • Added VERSION file (v1.0.0)
  • Added CHANGELOG.md
  • Added run_all.sh script for batch TLC verification
  • Added CI job (verify) for automated TLA+ model checking in GitHub Actions

Model Checker Configs

Spec Model Bounds States Checked Properties
raft 3 nodes, MaxTerm=3, MaxLogLen=3 475,972 4
twopc 3 participants, MaxTxnId=3 2,125,825 5
mvcc 2 keys, 2 values, MaxTxnId=2 177,849 5
replication 3 replicas, MaxLsn=3, MaxSyncCount=2 3,687,939 4 + 1 temporal
gossip 3 nodes, MaxIncarnation=3 1,257,121 3
deadlock 5 txns, MaxEdges=8 3,767,361 2
sharding 3 shards, 2 nodes, 5 vnodes 186,305 3
Reference in New Issue View Git Blame Copy Permalink