Formal Verification

Open-source projects categorized as Formal Verification
Edit details
Language: + Java + Rust + Ada + Coq + C + C# + F* + Standard ML + OCaml + TeX + Python + Verilog
Topics: Formal Methods Verification Rust tlaplus coq
The modern identity platform for B2B SaaS
The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
workos.com
Sponsored

Top 23 Formal Verification Open-Source Projects

  • P

    The P programming language.

    • Project mention: Property-based testing in practice [pdf] | news.ycombinator.com | 2024-04-02

  • hacl-star

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

  • InfluxDB

    Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

    InfluxDB logo

  • prusti-dev

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

    • Project mention: Using_Prolog_as_the_AST | news.ycombinator.com | 2023-10-21

    > The overall goal would be to figure out classical error conditions like nill pointers deference.

    > If I can figure out if a pointer will be nil in some execution branch, there is no reason why a computer cannot do the same.

    Note, this is called flow-sensitive typing (also called type narrowing) and I think that typescript does it.

    https://en.wikipedia.org/wiki/Flow-sensitive_typing

    > I personally would see this as an human race level upgrades. Imagine feeding your code to a CI that spit back something like: "you will have a panic at line 156 when your input is > 4"

    A model checker can do that!

    See this

    https://model-checking.github.io/kani/tutorial-kinds-of-fail...

    Other techniques are also possible

    https://github.com/viperproject/prusti-dev#quick-example

    (Here I could link a lot of things, I just selected two Rust projects to illustrate)

    This works better if you are able to provide contracts in your API that says which guarantees you provide. Alternatively, asserts are useful too.

  • Checker Framework

    Pluggable type-checking for Java

    • Project mention: @Nullable et @NonNull | dev.to | 2024-03-29

  • creusot

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

    • Project mention: Creusot, a deductive verifier for Rust code | news.ycombinator.com | 2024-02-29

  • cakeml

    CakeML: A Verified Implementation of ML

    • Project mention: The Deep Link Equating Math Proofs and Computer Programs | news.ycombinator.com | 2023-10-11

    If I understand what you are asking about correctly, then I do think you are mistaken.

    As a sibling comment observed, you would be proving something about a program, but proving things about programs is both possible and done.

    This ranges from things like CakeML (https://cakeml.org/) and CompCert (compilers with verified correctness proofs of their optimizations) to something simple like absence of runtime type errors in statically strongly soundly-typed languages.

    Of note is that you are proving properties of your program, not proving them perfect in every way. The properties of your program that you prove can vary wildly in both difficulty and usefulness. A sufficiently advanced formally verified compiler like CakeML can transfer a high-level proof about your source code to a corresponding proof about the behavior of the generated machine-executable code.

  • magmide

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

    • Project mention: 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? | /r/rust | 2023-07-04

    https://github.com/magmide/magmide when

  • WorkOS

    The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

    WorkOS logo

  • CreuSAT

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

  • practical-fm

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

  • proofs

    My personal repository of formally verified mathematics.

    • Project mention: A Taste of Coq and Correct Code by Construction | news.ycombinator.com | 2023-09-03

    If you're already familiar with a functional programming language like Haskell or OCaml, you have the prerequisite knowledge to work through my Coq tutorial here: https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

    My goal with this tutorial was to introduce the core aspects of the language (dependent types, tactics, etc.) in a "straight to the point" kind of way for readers who are already motivated to learn it. If you've heard about proof assistants like Coq or Lean and you're fascinated by what they can do, and you just want the TL;DR of how they work, then this tutorial is written for you.

    Any feedback is appreciated!

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

  • Daikon

    Dynamic detection of likely invariants

    • Project mention: Everything that uses configuration files should report where they're located | news.ycombinator.com | 2023-06-25

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

  • hax

    A Rust verification tool

    • Project mention: Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec | news.ycombinator.com | 2024-03-23

    I have no idea what the legal weight is for a toml field so this repo really would benefit from having a formal copy of the Apache-2 license file https://github.com/hacspec/hax/blob/2da100068e9ae5e69e5b35bb... similar to its MIT friend https://github.com/hacspec/hacspec/blob/4ecc847fc944fe996e19...

  • RecordFlux

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

  • CATG

    a concolic testing engine for Java

  • acsl-by-example

    Public snapshots of "ACSL by Example"

  • jCUTE

    Java Concolic Unit Testing Engine

  • fizzbee

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

    • Project mention: FizzBee: Open-source formal methods tool that's not hard | news.ycombinator.com | 2024-04-01

  • RISC-V

    Design implementation of the RV32I Core in Verilog HDL with Zicsr extension

    • Project mention: Prototype Demonstration of a 32-bit RISC-V Softcore with FreeRTOS | /r/FPGA | 2023-06-03

    The project repository and the details about the paper can be found here.

  • libcrux

    The formally verified crypto library for Rust

    • Project mention: Verified ML-KEM (Kyber) in Rust | news.ycombinator.com | 2024-02-01

  • libsparkcrypto

    A cryptographic library in SPARK 2014

  • 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 related posts

Index

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

Project Stars
1 P 2,911
2 hacl-star 1,583
3 prusti-dev 1,460
4 Checker Framework 976
5 creusot 968
6 cakeml 912
7 magmide 804
8 CreuSAT 581
9 practical-fm 460
10 proofs 285
11 awesome-rust-formalized-reasoning 263
12 Daikon 202
13 spark-by-example 150
14 OpenJML 131
15 hax 127
16 RecordFlux 100
17 CATG 97
18 acsl-by-example 94
19 jCUTE 85
20 fizzbee 63
21 RISC-V 42
22 libcrux 38
23 libsparkcrypto 27

Sponsored
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com