uwplse / verdi-raft

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
BSD 2-Clause "Simplified" License
182 stars 19 forks source link

Verified serialization of network messages #60

Closed palmskog closed 7 years ago

palmskog commented 7 years ago

Use Cheerios and Verdi Cheerios to construct VarD Raft system with verified network message serialization. Use VST to prove linearization for serialized system.