 dimgigov
|
422df08ab9
|
feat: clean build + crossmodal.tla + TLA+ symmetry (v1.0.0-prep)
Build warnings cleanup (0 warnings):
- Suppress threadpool deprecation warning (baradadb.nim)
- Remove unused 'os' import (logging.nim)
- Fix ImplicitDefaultValue for newNode params (ast.nim)
- Add explicit cstring cast for posix.open (wal.nim)
- Fix HoleEnumConv for MsgKind parsing (server.nim)
TLA+ Formal Verification:
- Add symmetry reduction (Permutations) to all 9 existing specs
- Add SYMMETRY directive to all .cfg files
- New crossmodal.tla: cross-modal consistency spec
* MetadataVectorConsistency, HybridResultValid
* CommittedAtomicity, AbortedAtomicity, TxnStateValid
- New models/crossmodal.cfg
Tests:
- Add Cross-Modal TLA+ Faithfulness tests (4 tests)
Docs:
- Update PLAN.md and BUG_AUDIT.md with completed tasks
|
2026-05-13 09:24:04 +03:00 |
|
|
dimgigov
|
f9e5169c3d
|
FV-6: Liveness properties + fairness constraints
- mvcc.tla: Add CommitProgress liveness (verified with WF_vars)
- raft/twopc/mvcc/gossip: Add Spec definitions with WF_vars(Next)
- gossip.tla: Fix LearnViaGossip strength-based filtering
(prevents overwriting Dead/Suspect with weaker state)
- twopc.tla: Add DecideCommitAction/DecideAbortAction for SF fairness
- Update all .cfg files to use SPECIFICATION Spec
- Update CHANGELOG.md -> v1.1.0, VERSION -> 1.1.0, PLAN.md
|
2026-05-07 21:21:22 +03:00 |
|
|
dimgigov
|
39e07b542d
|
FV-3, FV-4: 2PC coordinator crash/recovery + participant timeout
- twopc.tla: Add coordinatorLog (persistent WAL for decisions)
- twopc.tla: Add CrashCoordinator action
- twopc.tla: Add RecoverCoordinator action (reads from coordinatorLog)
- twopc.tla: Add ParticipantTimeout (only if coordinatorLog = Nil)
- twopc.tla: Add RecoveryConsistency invariant
- models/twopc.cfg: Add RecoveryConsistency to checked invariants
- Update PLAN.md, ANALYSIS.md, README.md with new metrics
|
2026-05-07 19:40:09 +03:00 |
|
|
dimgigov
|
19d0ff7366
|
feat(verify): expand formal verification to 7 specs, add versioning, CI integration
Added 3 new TLA+ specs:
- gossip.tla — SWIM gossip membership & failure detection
- deadlock.tla — wait-for graph deadlock detection
- sharding.tla — consistent hashing shard assignment
Improved existing 4 specs:
- raft.tla: added CommittedIndexValid invariant
- twopc.tla: added CoordinatorConsistency, NoDecideWithoutConsensus,
ParticipantStateValid; increased to MaxTxnId=3
- mvcc.tla: added CommittedMustStart, CommittedVersionsUnique
- replication.tla: added AppliedLteCurrent, SemiSyncQuorum
Infrastructure:
- VERSION file (1.0.0)
- CHANGELOG.md
- ANALYSIS.md (weak spots & improvement plan)
- run_all.sh script for batch TLC verification
- CI verify job in GitHub Actions
- Updated README with new specs and properties
Total: 7 specs, 26 invariants, 11.6M states checked, 0 errors
|
2026-05-07 18:26:55 +03:00 |
|
|
dimgigov
|
e73bfb450c
|
feat: formal verification suite — TLA+ specs for Raft, 2PC, MVCC, Replication
Verified with TLC model checker:
- Raft: 475k states, ElectionSafety + StateMachineSafety
- 2PC: 22k states, Atomicity + NoOrphanBlocks
- MVCC: 177k states, NoDirtyReads + ReadOwnWrites + WriteWriteConflict
- Replication: 3.6M states, MonotonicLsn + AcksRemovePending
|
2026-05-07 15:57:33 +03:00 |
|