IPA(Interaction-Preserving Abstraction) is a framework that leverages characteristics of TLA+ and enables practical and efficient compositional model checking for TLA+ specifications of distributed consensus protocols.
This repository shows our experiments of applying IPA to the famous consensus protocol Raft.
Readers can find detailed explanation for abstraction of each module in Docs and formal specifications in Specifications.