Formal Verification

Open-source projects categorized as Formal Verification

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*

  • Project mention: F* – A Proof-Oriented Programming Language | news.ycombinator.com | 2024-05-16

    F* existed before Project Everest, but Everest did power a lot of its development.

    We have built verified systems and components in the TLS ecosystem, including parts of TLS, QUIC and related protocols, and continue to do so: https://project-everest.github.io/

    Some of it is deployed in production systems:

    * Verified parsers in the Windows kernel and elsewhere: https://www.microsoft.com/en-us/research/blog/everparse-hard...

    * Verified crypto in Linux, Firefox, Python, ... https://github.com/hacl-star/hacl-star

  • 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: What if null was an Object in Java? | news.ycombinator.com | 2024-04-28

    I’m not familiar enough with kotlin to comment fully but from your description the checker framework [0] appears to do the same thing in Java.

    I confess I’m not fond of checker framework. I find the error messages can be obtuse but it is very effective.

    0 - https://checkerframework.org/

  • creusot

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

  • Project mention: Release Creusot 0.1 · creusot-rs/creusot | news.ycombinator.com | 2024-05-20
  • cakeml

    CakeML: A Verified Implementation of ML

  • Project mention: CakeML: A formally verified implementation of ML | news.ycombinator.com | 2024-05-14
  • 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

  • SaaSHub

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

    SaaSHub 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

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

  • 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

  • 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,929
2 hacl-star 1,594
3 prusti-dev 1,484
4 Checker Framework 989
5 creusot 1,027
6 cakeml 921
7 magmide 808
8 CreuSAT 591
9 practical-fm 465
10 proofs 286
11 awesome-rust-formalized-reasoning 279
12 Daikon 203
13 spark-by-example 150
14 hax 141
15 OpenJML 135
16 RecordFlux 101
17 CATG 98
18 acsl-by-example 94
19 jCUTE 85
20 fizzbee 80
21 RISC-V 46
22 libcrux 45
23 libsparkcrypto 27

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