uwplse/verdi
View on GitHub ↗ ★ 627 Rocq Prover
A framework for formally verifying distributed systems implementations in Coq
9 mentions on Hacker News by 9 people: 1 story, 8 comments · first 2015-04-08 · latest 2017-05-19
20082026
-
https://github.com/uwplse/verdi is a good example of this (it uses coq and extractions along with minimal glue).
comment by tschottdorf · 2017-05-19 · in Writing correct lock-free and distributed stateful systems in Rust, with TLA+ -
…side the publication. For example FSCQ( https://github.com/mit-pdos/fscq-impl ) from MIT, Verdi ( https://github.com/uwplse/verdi ) from UW, Dune( http://dune.scs.stanford.edu/ ) from Stanford, and many more. These are just the areas I…
comment by jroesch · 2016-05-01 · in “Extremely angry with the state of academic CS research right now” -
…coq code in verdi raft, and all the follow on commits should be strictly syntactic transformations. https://github.com/uwplse/verdi is the associated coq development )
comment by carterschonwald · 2016-03-03 · in Byzantine Fault Tolerant Raft With Smart Contracts -
…for distributed system verification, which now includes a formally proven Raft implementation. https://github.com/uwplse/verdi This appears to be the main theorem, "raft_linearizable": https://github.com/uwplse/verdi/blob/master/raft-proofs…
comment by mbrock · 2015-11-08 · in The category design pattern -
First, a correction -- the only known-good implementation of Raft is actually in Coq ( https://github.com/uwplse/verdi ), which predates Idris (which intends to be an easier-to-use Coq). So the problem with distributed consensus algorithms…
comment by felixgallo · 2015-10-05 · in Lessons learned writing highly available code -
…need to trust is the top-level specification. In our case, this is linearizability (have a look at https://github.com/uwplse/verdi/blob/master/raft/Linearizabi... for the key definition; the key theorem statement is at…
comment by wilcoxjay · 2015-08-06 · in Prove Raft Correct -
…to find time to give it a try ! By the way, a bit of DuckDuckGo gives: - http://verdi.uwplse.org/ - https://github.com/uwplse/verdi/
comment by dwenzek · 2015-06-22 · in A Framework for Implementing and Formally Verifying Distributed Systems [pdf] -
…interested in proving distributed algorithms correct, they should check out the Verdi project ( https://github.com/uwplse/verdi ), which has proved Raft correct in Coq. I imagine handling Byzantine faults and the full complexity of SCP…
comment by ziedaniel1 · 2015-04-08 · in Stellar Consensus Protocol: Proof and Code