Top 4 Coq Proof Projects
-
Verdi — a framework for implementing and formally verifying distributed systems (based on Coq).
-
InfluxDB
Purpose built for real-time analytics at any scale. InfluxDB Platform is powered by columnar analytics, optimized for cost-efficient storage, and built with open data standards.
-
coq-of-rust
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
Project mention: Translation of the Rust's core and alloc crates to Coq for formal verification | news.ycombinator.com | 2024-05-15That's really impressive.
Automatic translation like this shifts the trust to the tool. coq-of-rust itself is written in Rust, not in Coq. The recursive nature is somewhat boggling, but I think a proof of its correctness could be done in much the same way as they do with the stdlib. To verify it, you'd use coq-of-rust to convert coq-of-rust to Coq. That translation is not trusted, because it was performed in Rust. You then undertake the process they describe in the article of proving equivalence between generated definitions and simpler hand-written definitions, which proofs are written in terms of. Once you prove that the generated Coq version of coq-of-coq translates Rust programs correctly, you use it to translate Rust coq-of-rust to Coq and compare the two. They should match. Since the current line count for coq-of-rust (specifically, lib/ [0]) is 6350 lines of Rust, this seems feasible.
It's a similar process to David A. Wheeler's “Countering Trusting Trust through Diverse Double-Compiling” (2009) [1], which circumvents Ken Thompson's Trusting Trusting attack by using a second compiler.
As an aside, it's nice to see industry funding for work like this. I'm often cynical of cryptocurrency, but its correctness constraints really push for improvements in areas I like (Rust, Coq, funding for masters students I know, etc.).
[0]: https://github.com/formal-land/coq-of-rust/tree/main/lib
-
verdi-raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
-
disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Diesel — a framework for implementation and compositional machine-assisted verification of distributed systems and their clients (based on Coq);
Coq Proof discussion
Index
What are some of the best open-source Proof projects in Coq? This list will help you:
| Project | Stars | |
|---|---|---|
| 1 | verdi | 580 |
| 2 | coq-of-rust | 394 |
| 3 | verdi-raft | 181 |
| 4 | disel | 94 |
Sponsored