Proposal: verify Verdi Raft store interaction down to file system level

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

Proposal: verify Verdi Raft store interaction down to file system level #80

Open palmskog opened 4 years ago

palmskog commented 4 years ago

This is natural followup to uwplse/verdi#125: use the general Verdi interface to a verified file system to prove that Verdi Raft, when run using the file system, does not suffer from bugs due to corrupted logs.