Proposal: verify Raft handlers down to machine code 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 Raft handlers down to machine code level #79

Open palmskog opened 4 years ago

palmskog commented 4 years ago

This is a more ambitious version of uwplse/verdi#123, where one uses VST to refine the Raft handlers to C code, which CompCert can compile to verified machine code. As a first step, the verified code could interact with the existing Verdi shim that Verdi Raft uses via OCaml's C interface. One could also implement a standalone shim in C by taking inspiration from the OCaml shim.