Collect, organize, and act on massive volumes of high-resolution data to power real-time intelligent systems. Learn more →
Top 3 Coq Formal Method Projects
-
magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
-
InfluxDB
InfluxDB high-performance time series database. Collect, organize, and act on massive volumes of high-resolution data to power real-time intelligent systems.
-
-
aws-lc-verification
This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal verification is used to locate bugs and increase assurance of the correctness and security of the library.
Agree. The remaining comments boil down to:
1. "It's not visual, it's text". Yeah, but: how many "visual" representations have no text? And there _are_ visuals in there: the depictions of state space. They include text (hard to see how they'd be useful without) but aren't solely so.
2. "Meh, verification is for well paid academics, it's not for the real world". First off, I doubt those "academics" are earning more than median sw devs, never mind those in the SV bubble. More importantly: there are well-publicised examples of formal verification being used for real-world code, see e.g. [1].
It's certainly true that verification isn't widespread. It has various barriers, from use of formal maths theory and presentation to the compute load arising from combinatorial explosion of the state space. Even if you don't formally verify, understanding the state space size and non-deterministic path execution of concurrent code is fundamentally important. As Dijkstra said [2]:
> our intellectual powers are rather geared to master static relations and that our powers to visualise processes evolving in time are relatively poorly developed. For that reason we should do (as wise programmers aware of our limitations) our utmost to shorten the conceptual gap between the static process and the dynamic program, to make the correspondence between the program (spread out in space) and the process (spread out in time) as trivial as possible.
He was talking about sequential programming: specifically, motivating the use of structured programming. It's equally applicable to concurrent programming though.
[1]: https://github.com/awslabs/aws-lc-verification
[2]: https://homepages.cwi.nl/~storm/teaching/reader/Dijkstra68.p...
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 Methods discussion
Coq Formal Methods related posts
-
How concurrecy works: A visual guide
-
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?
-
Which proof assistant is the best to formalize real analysis/probability/statistics?
-
Announcing Magmide Month! (proof language for/using Rust)
-
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
-
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
-
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
-
A note from our sponsor - InfluxDB
influxdata.com | 21 Apr 2025
Index
What are some of the best open-source Formal Method projects in Coq? This list will help you:
| # | Project | Stars |
|---|---|---|
| 1 | magmide | 821 |
| 2 | koika | 148 |
| 3 | aws-lc-verification | 40 |
Sponsored
InfluxDB high-performance time series database
Collect, organize, and act on massive volumes of high-resolution data to power real-time intelligent systems.
influxdata.com