Formal Verification

Open-source projects categorized as Formal Verification

Top 23 Formal Verification Open-Source Projects

Formal Verification
  1. P

    The P programming language.

    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

  2. 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.

    InfluxDB logo
  3. hacl-star

    HACL*, a formally verified cryptographic library written in F*

    Project mention: HACL: A High-Assurance Cryptographic Library | news.ycombinator.com | 2024-06-09
  4. prusti-dev

    A static verifier for Rust, based on the Viper verification infrastructure.

  5. creusot

    Creusot helps you prove your code is correct in an automated fashion.

    Project mention: Coq-of-rust: Formal verification tool for Rust | news.ycombinator.com | 2025-03-14
  6. Checker Framework

    Pluggable type-checking for Java

  7. cakeml

    CakeML: A Verified Implementation of ML

  8. 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-13

    Yep, 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.

  9. SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
  10. magmide

    A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

  11. CreuSAT

    CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

    Project mention: LIMO: Less Is More for Reasoning | news.ycombinator.com | 2025-02-09

    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...

  12. practical-fm

    A gently curated list of companies using verification formal methods in industry

  13. 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.

  14. proofs

    My personal repository of formally verified mathematics.

  15. alpha-beta-CROWN

    alpha-beta-CROWN: An Efficient, Scalable and GPU Accelerated Neural Network Verifier (winner of VNN-COMP 2021, 2022, 2023, and 2024)

  16. hax

    A Rust verification tool

  17. Daikon

    Dynamic detection of likely invariants

  18. fizzbee

    Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications

  19. learntla-v2

    Learn TLA+ for free! No prior experience necessary!

    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.

  20. 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

  21. 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:

  22. libcrux

    The formally verified crypto library for Rust

  23. 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
  24. acsl-by-example

    Public snapshots of "ACSL by Example"

  25. CATG

    a concolic testing engine for Java

  26. SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
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

Log in or Post with

Formal Verification related posts

  • Type-Constrained Code Generation with Language Models

    7 projects | news.ycombinator.com | 13 May 2025
  • Coq-of-rust: Formal verification tool for Rust

    4 projects | news.ycombinator.com | 14 Mar 2025
  • Design and Explore Noise Handshake Patterns

    1 project | news.ycombinator.com | 5 Mar 2025
  • How concurrecy works: A visual guide

    2 projects | news.ycombinator.com | 20 Dec 2024
  • Release Creusot 0.1 · creusot-rs/creusot

    1 project | news.ycombinator.com | 20 May 2024
  • Translation of the Rust's core and alloc crates to Coq for formal verification

    3 projects | news.ycombinator.com | 15 May 2024
  • CakeML: A formally verified implementation of ML

    1 project | news.ycombinator.com | 14 May 2024
  • A note from our sponsor - InfluxDB
    www.influxdata.com | 18 May 2025
    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 →

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