InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now. Learn more →
Top 23 Formal Verification Open-Source Projects
-
Project mention: Systems Correctness Practices at AWS: Leveraging Formal and Semi-Formal Methods | news.ycombinator.com | 2025-04-01
If you are wondering "why do formal methods at all?" or "how is AWS using P to gain confidence in correctness of their services?", the following re:Invent 2023 talk answers this question, provides an overview of P, and its impact inside AWS: (Re:Invent 2023 Talk) Gain confidence in system correctness & resilience with Formal Methods (Finding Critical Bugs Early!!) - https://www.youtube.com/watch?v=FdXZXnkMDxs
Github: https://github.com/p-org/P
-
InfluxDB
InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.
-
-
-
-
-
-
coq-of-rust
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦
Project mention: Type-Constrained Code Generation with Language Models | news.ycombinator.com | 2025-05-13Yep, Rust famously goes beyond this by modelling memory ownership at compile time.
In fact, the more behaviour we can model at compile time the better when it comes to LLMs - there's some cool ideas here like transpiling Rust into languages for formal verification. See https://github.com/formal-land/coq-of-rust as an example.
Formal verification was one of those things that was previously so annoying to do that it rarely made it past academic use cases or extremely important libraries, but I think LLMs take the tedium out of it. Perhaps formal verification will have a "test driven development" type of moment in the sun thanks to this.
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
-
magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
-
You tell it what you want it to prove. Or the tooling surrounding it does.
The tooling surrounding it might want to prove that "this main function never invokes undefined behavior", or something more local like "for all possible inputs to the public interface to this module, no undefined behavior is invoked".
Or you might want to specify constraints by hand. For examples, you might do that by writing normal tests except you can use magical variables that take on any value [1], or you might do that by annotating functions with contracts that they obey [2]. Or at a simpler level you might just annotate functions that should never panic.
Ultimately once you can prove things about your code, it's a tool in the toolbox for querying how your code works. You can use that to write correct code from the start, or to debug incorrect code, or various other things. The problem is that right now the state of the art (non-ai) can't reason about very complex code without a lot of human help - making it a fairly impractical tool. I think AI might mange to fix that.
[1] This is how kani works in rust, here's an example: https://github.com/model-checking/verify-rust-std/pull/112/f...
[2] Creusot takes this route, here's an example https://github.com/sarsko/CreuSAT/blob/master/CreuSAT/src/so...
-
-
awesome-rust-formalized-reasoning
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
-
-
alpha-beta-CROWN
alpha-beta-CROWN: An Efficient, Scalable and GPU Accelerated Neural Network Verifier (winner of VNN-COMP 2021, 2022, 2023, and 2024)
-
-
-
fizzbee
Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
-
Project mention: Formal Methods: Just Good Engineering Practice? | news.ycombinator.com | 2025-01-10
Not the OP, but Hillel Wayne’s course/tutorial (https://www.learntla.com/) is fantastic. It’s focused on building practical skills, and helped me build enough competence to write a few (simple, but useful!) specs for some of the systems I work on.
-
spark-by-example
SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada
-
OpenJML
This is the primary repository for the source code of the OpenJML project. The source code is licensed under GPLv2 because it derives from OpenJDK which is so licensed. The active issues list for OpenJML development is here and the wiki contains information relevant to development. Public documentation for users is at the project website:
-
-
RecordFlux
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Project mention: Nvidia Security Team: "What if we just stopped using C?" (2022) | news.ycombinator.com | 2025-02-13 -
-
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
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).
Formal Verification discussion
Formal Verification related posts
-
Type-Constrained Code Generation with Language Models
-
Coq-of-rust: Formal verification tool for Rust
-
Design and Explore Noise Handshake Patterns
-
How concurrecy works: A visual guide
-
Release Creusot 0.1 · creusot-rs/creusot
-
Translation of the Rust's core and alloc crates to Coq for formal verification
-
CakeML: A formally verified implementation of ML
-
A note from our sponsor - InfluxDB
www.influxdata.com | 18 May 2025
Index
What are some of the best open-source Formal Verification projects? This list will help you:
| # | Project | Stars |
|---|---|---|
| 1 | P | 3,283 |
| 2 | hacl-star | 1,751 |
| 3 | prusti-dev | 1,644 |
| 4 | creusot | 1,264 |
| 5 | Checker Framework | 1,070 |
| 6 | cakeml | 1,037 |
| 7 | coq-of-rust | 906 |
| 8 | magmide | 821 |
| 9 | CreuSAT | 630 |
| 10 | practical-fm | 535 |
| 11 | awesome-rust-formalized-reasoning | 336 |
| 12 | proofs | 299 |
| 13 | alpha-beta-CROWN | 282 |
| 14 | hax | 262 |
| 15 | Daikon | 224 |
| 16 | fizzbee | 221 |
| 17 | learntla-v2 | 210 |
| 18 | spark-by-example | 160 |
| 19 | OpenJML | 155 |
| 20 | libcrux | 124 |
| 21 | RecordFlux | 113 |
| 22 | acsl-by-example | 106 |
| 23 | CATG | 106 |
Sponsored
InfluxDB – Built for High-Performance Time Series Workloads
InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.
www.influxdata.com