CCF consensus verification roadmap

[achamayou]

This issue aims to create a priority-ordered list of items that need to be tackled to complete the verification of CCF Raft, and summarise their dependencies so they can be picked up efficiently.

• ccfraft.tla startup is incorrect, and needs to be aligned with the implementation. This our top priority item, it's documented at length in Handling of initial configuration in TLA+ spec does not match implementation #5220, Retain all signatures during a soft rollback #5749, and there's an ongoing effort in Add driver commands to start networks and reconfigure more realistically #5769 to fix it. We should not be adding any more invariants, properties etc until this has been addressed.
• ccfraft.tla commit is incorrect, and needs to be aligned with the implementation. This is documented in Minimal repro triggering the issue in ccfraft.tla AdvanceCommitIndex #5798. This does not depend on the first item, and can be picked up independently.
• Check, and eliminate NotifiyCommit messages, documented in Check if NotifyCommit messages in TLA+ are safe #5280. Those do not exist in the implementation, will not trace validate.
• Split leadership_state from membership_state. Refactoring consensus leadership states in specification #5902 They are confused in the spec (RetiredLeader). Prerequisite to:
• Complete retirement modeling, see TLA+ spec does not model a retiring Follower #4818.

#2577, #5678 and #5290 are lower priority than all of the above, and some of them may reconsidered altogether once these are complete.

[achamayou]

This roadmap has run its course, we can look at the next steps in the larger-scoped #5057.