Formal Verification

Open-source projects categorized as Formal Verification

Top 23 Formal Verification Open-Source Projects

  • hacl-star

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

    Project mention: One step forward, an easier interoperability between Rust and Haskell | IOG Engineering | | 2023-01-27

    Nice work. About cryptonite: have IOG considered using crypto primitives provided by HACL*/evercrypt?

  • prusti-dev

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

    Project mention: A plan for cybersecurity and grid safety | | 2023-02-10

    Efforts: seL4, Project Everest, the Prossimo project of the ISRG, Let's Encrypt, and Prusti for the Rust language

  • Sonar

    Write Clean Java Code. Always.. Sonar helps you commit clean code every time. With over 600 unique rules to find Java bugs, code smells & vulnerabilities, Sonar finds the issues while you focus on the work.

  • Checker Framework

    Pluggable type-checking for Java

    Project mention: Don’t call it a comeback: Why Java is still champ | | 2022-08-09

    Java should adopt something like the Checker Framework Nullness Checker in its first-party tooling.

  • cakeml

    CakeML: A Verified Implementation of ML

    Project mention: Tools for Verifying a Language and its Semantics | | 2023-01-02

    You may want to look at [CakeML]( done in HOL4, there is also a nice proof pearl about a more .. minimalistic verified bootstrapped compiler also in HOL4.

  • magmide

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

    Project mention: Announcing Magmide Month! (proof language for/using Rust) | | 2023-02-28
  • creusot

    deductive verification of Rust code. (semi) automatically prove your code satisfies your specifications!

    Project mention: Prop v0.42 released! Don't panic! The answer is... support for dependent types :) | | 2023-01-18

    Wow that sounds really cool! I'm not an expert but does that mean that one day you could implement dependend types or refinement types in Rust as a crate ? I currently only know of tools like: Flux Creusot Kani Prusti

  • CreuSAT

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

    Project mention: CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot | | 2022-06-18
  • InfluxDB

    Access the most powerful time series database as a service. Ingest, store, & analyze all types of time series data in a fully-managed, purpose-built database. Keep data forever with low-cost storage and superior data compression.

  • practical-fm

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

    Project mention: We Need Simpler Types (speculations on what can be improved in future type systems and on erasing the boundaries between types and values) | | 2022-09-14 Look for Coq, Agda, Idris, MS - F*.

  • proofs

    My personal repository of formally verified mathematics.

    Project mention: Thoughts on proof assistants? | | 2022-12-13

    Personally I treat Coq like an extension of my brain. Whenever I'm uncertain about something, I formalize it in Coq. I have a repository of proofs with GitHub Actions set up in such a way forbids me from pushing commits containing mathematical mistakes. I've formalized various aspects of category theory, type theory, domain theory, etc., and I've also verified a few programs, such as this sorting algorithm. Lately I've been experimenting with a few novel types of graphs, proving various properties about them with the aim of eventually developing a way to organize all of my data (files, notes, photos, passwords, etc.) in some kind of graph structure like that.

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

    Project mention: CreuSAT: Formally verified SAT solver written in Rust and verified with Creusot | | 2022-06-17

    Unsurprisingly, we can see a growing interest in the Rust ecosystem regarding formal verification. I try to keep up to date. I will add CreuSAT shortly.

  • hacspec

    A specification language for cryptography primitives.

  • Daikon

    Dynamic detection of likely invariants

  • 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

    Project mention: Spark by Example is an adaptation of ACSL by Example for SPARK 2014, a programm | | 2022-11-18
  • 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:

    Project mention: Anybody tried OpenJML's static checker? What's it's state? | | 2022-04-29

    Has anyone successfully used OpenJML's static checker on a real project to reduce defects?

  • RecordFlux

    Formal specification and generation of verifiable binary parsers, message generators and protocol state machines

    Project mention: Why isn't there a Swagger/OpenAPI for binary formats? | | 2022-03-25
  • CATG

    a concolic testing engine for Java

  • acsl-by-example

    Public snapshots of "ACSL by Example"

  • jCUTE

    Java Concolic Unit Testing Engine

  • libsparkcrypto

    A cryptographic library in SPARK 2014

  • hardware

    Verilog development and verification project for HOL4 (by CakeML)

  • TLAplus

    TLA+ questions, answers, and experiments (by Isaac-DeFrain)

  • basalt

    Collection of formally verified building blocks (by Componolit)

    Project mention: SPARK Guide | | 2022-06-10

    As a real world example you can take a look at the Image_Ranged and Image_Modular functions defined in and basalt-strings_generic.adb. The goal property for these functions is (apart from the absence of runtime errors) that they always return a string that starts at the index 1 and that has a specific maximum length, depending on the base given.

  • isabelle-lambda-calculus

    A formal definition and verification of System F. To be extended to System Fc

  • 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). The latest post mention was on 2023-02-28.

Formal Verification related posts


What are some of the best open-source Formal Verification projects? This list will help you:

Project Stars
1 hacl-star 1,463
2 prusti-dev 1,234
3 Checker Framework 897
4 cakeml 799
5 magmide 749
6 creusot 644
7 CreuSAT 506
8 practical-fm 412
9 proofs 240
10 awesome-rust-formalized-reasoning 196
11 hacspec 181
12 Daikon 163
13 spark-by-example 145
14 OpenJML 114
15 RecordFlux 92
16 CATG 90
17 acsl-by-example 87
18 jCUTE 81
19 libsparkcrypto 26
20 hardware 18
21 TLAplus 16
22 basalt 9
23 isabelle-lambda-calculus 8
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives