JOjohnbender·Oct 28, 2021
Raft has been manually verified which was the hurdle here that makes the result interesting:
https://github.com/uwplse/verdi-raft
In Paxos automatically determined safe and secureuwplse
verdi-raft
Coq2017–2021
uwplse / verdi-raft
verdi-raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
4Distinct people
4Mentions
0Explicit recommenders
204GitHub stars
What to know before exploring
What it is
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
GitHub
Where it is used
No documented product use has been verified yet.
What people are saying
No recommendation phrase was found in the indexed comments.
No classified warning is attached to this page. Read the discussions before treating silence as approval.
Also in these discussions
No other repository is repeatedly linked in the same discussions.
This week on Hacker News
Nov 7–Nov 14 UTC · Direct repository links and separately labeled related project stories. Indexed through 11/14/2026, 5:04:57 PM UTC.
No direct repository links were found in the indexed HN discussions over the past seven days. Older discussions are available below.
Mentions over time
HN mentions by year4 dated mentions
Observed mentions: 2017-07-09 15:40:44 UTC to 2021-10-28 01:46:27 UTC.
Counts come from the repository’s dated source evidence. Index cutoff: 2026-11-02 08:16:59 UTC.
View mention counts and date ranges
| Period | Start (UTC) | End (exclusive, UTC) | Mentions | Submissions | Comments |
|---|---|---|---|---|---|
| 2017 | 2017-01-01 00:00:00 UTC | 2018-01-01 00:00:00 UTC | 2 | 0 | 2 |
| 2018 | 2018-01-01 00:00:00 UTC | 2019-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2019 | 2019-01-01 00:00:00 UTC | 2020-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2020 | 2020-01-01 00:00:00 UTC | 2021-01-01 00:00:00 UTC | 1 | 0 | 1 |
| 2021 | 2021-01-01 00:00:00 UTC | 2022-01-01 00:00:00 UTC | 1 | 0 | 1 |
What Hacker News says
4 sourcesTLA+ has no direct path to code. But it is a great way to test-drive your _idea_, to force you to dwell on your problem before beginning to code, to look for states that you never thought about even in a simplified setting.
Having gone through the exercise, I find I have greater clarity while coding, and have a better idea of where to place assertions and where to look for invariants. Often I iterate between prototyping with code, then playing with TLA+, then back to prototyping before throwing it all out and starting from scratch.
----
Then there are tools like Coq that convert a proof to running code automatically. For example, see the Verdi framework for doing Raft consensus: https://github.com/uwplse/verdi-raft.
This is clearly not for the faint of heart. The wonderful thing about this exercise is that it forces you to be precise abou
Read the rest
t your specification, and holds your feet to the fire until your proof meets the spec. At the end of the day however, you have no guarantee that the specification (and the simplifications made to get coq going) are enough to capture enough interesting aspects of the real world. Still, for safety-critical and security-critical systems, it is always comforting that someone's gone through the pain of thinking it through to an extra level.
> We're not even close to a world where tools can offer amazing protection.
Actually, we're reasonably close--the tools aren't quite there yet for mass consumption (many are still feel quite researchy), but given that the trend of (research -> industry) usually takes 10-25 years, I'd expect that more and more critical systems will be formally verified in 10 years. Even now, companies like Amazon are using some formal methods (modelling with TLA+) to validate that specifications will behave as expected. (https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-...)
Formal methods & dependent types allow for some very cool tricks on top of that--basically, you can encode in the type system a proof that the program implementation matches a specification. CompCert is a mostly-formally verified C compiler--since it was released, iirc, no
Read the rest
bugs have been found in the verified portion of the compiler. (CompCert page: http://compcert.inria.fr/man/manual001.html)
You can also prove that the specification has particular properties (in a distributed system, things like liveness and partition tolerance). Consider the Verdi framework (allows formal verification of distributed protocols) and their formal verification of RAFT. (Code here: https://github.com/uwplse/verdi-raft)
However--it's just that it currently takes a lot more work in terms of person-hours to do the development. But formal methods are getting used in more and more places, and they do make a difference in practice. (Wired has a not particularly deep, but straightforward article that shows another use: https://www.wired.com/2016/09/computer-scientists-close-perf... )
Anecdotally, as far as effort--I'm an industry programmer who writes mostly C#. I had to learn Coq (a formally verified language) for a class--it took me a couple of simple assignments to get the idea of how it worked. Even after a few months, hacking together a formally verified interpreter for a very simple language (functions, while loops, etc.--simple, but not trivial) took about 3-4 times longer than it would have taken me to do normally.
Yes; because it's mentioned in the article:
> Both the Verdi framework and our verified Raft implementation are open-source. Please feel free to submit comments, issues, and pull requests on either repository.
[1] https://github.com/uwplse/verdi-raft
In Verdi – Formally Verifying Distributed Systems (2016)