2 Commits

Author	SHA1	Message	Date
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	32b38675a9	Add TLA+ formal verification specs for backup and recovery ... - backup.tla: models backup/restore/verify/cleanup with properties: BackupSnapshotsValid, RestoreIntegrity, VerifyIntegrity, RetentionInvariant, HistoryConsistency, BackupIdValid - recovery.tla: models WAL replay REDO/UNDO with properties: RedoCommitted, RecoveryCompleteness, WalIntegrity - Added models/backup.cfg and models/recovery.cfg with bounded constants - Updated run_all.sh to include both new specs - All 9 TLA+ specs pass TLC model checking	2026-05-13 00:06:45 +03:00