InfluxDB Platform is powered by columnar analytics, optimized for cost-efficient storage, and built with open data standards. Learn more →
Top 3 Coq Formal Verification Projects
-
magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
-
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
-
NOTE:
The open source projects on this list are ordered by number of github stars.
The number of mentions indicates repo mentiontions in the last 12 Months or
since we started tracking (Dec 2020).
Coq Formal Verification discussion
Coq Formal Verification related posts
-
Translation of the Rust's core and alloc crates to Coq for formal verification
-
Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec
-
A Taste of Coq and Correct Code by Construction
-
Languages on the rise like Rust and Go are being quite vocal against inheritance and many engineers seem to agree. Is this the end of inheritance? What do you think?
-
Announcing Magmide Month! (proof language for/using Rust)
-
Formally Verifying Rust's Opaque Types
-
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
-
A note from our sponsor - InfluxDB
www.influxdata.com | 7 Sep 2024
Index
What are some of the best open-source Formal Verification projects in Coq? This list will help you:
| Project | Stars | |
|---|---|---|
| 1 | magmide | 811 |
| 2 | coq-of-rust | 386 |
| 3 | proofs | 289 |
Sponsored
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.
www.influxdata.com