CakeML: A Verified Implementation of ML

Coq library for verified low-level programming

Analyze Rust crates without touching compiler internals

A Proof-oriented Programming Language

Icarus Verilog

Reads a state transition system and performs property checking

The VerCors verification toolset for verifying parallel and concurrent software

Sound static analysis for the masses.

A precise specification for "Rust lite / MIR plus"

Lean 4 port of Iris, a higher-order concurrent separation logic framework

An interpreter for Rust's mid-level intermediate representation

Documentation and proof of concept code for CVE-2022-24125 and CVE-2022-24126.

An SMT solver frontend for OCaml

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

C Bounded Model Checker

Kani Rust Verifier

Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.

Multi-engine SMT-based automatic model checker for safety properties of Lustre programs

The Gillian Platform main repository

Verified Rust for low-level systems code

Research prototype tool for modular formal verification of C, Rust and Java programs

The core implementation of the Acorn language.

Welcome to the ultimate list of resources for formal verification techniques and tools. This repository aims to provide an organized collection of high-quality resources to help professionals, rese…

Nagini is a static verifier for Python 3, based on the Viper verification infrastructure.

Public repo for H-Houdini / VeloCT code release for ASPLOS'25

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

Dafny is a verification-aware programming language