Files
Baradb/formal-verification/VERSION
T
dimgigov 4791434cea FV-2: Raft leader step-down on partition loss
- Add heartbeatReceived variable tracking last term with heartbeat
- Add Heartbeat action: leader sends keep-alive; recipient steps down on higher term
- Add HeartbeatTimeout: follower starts election if no heartbeat in current term
- Add LeaderLeaseExpired: leader steps down if it loses quorum connectivity
- Add LeaderHasSelfHeartbeat invariant: every leader must have valid heartbeat
- raft.tla now models realistic partition behavior (38M states verified)
- Update CHANGELOG -> v1.2.0, VERSION -> 1.2.0, PLAN.md, README.md
2026-05-07 21:48:03 +03:00

2 lines
6 B
Plaintext