the champagne of beta embedded databases

• UpdatedNov 4, 2025
• Rust

The P programming language.

• UpdatedDec 12, 2025
• C#

My own notes (drafts mostly) about software quality

• UpdatedFeb 1, 2023

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

• UpdatedOct 26, 2025
• F*

Lean 3's obsolete mathematical components library: please use mathlib4

• UpdatedJun 28, 2024
• Lean

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

• UpdatedDec 17, 2025
• Rust

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

• UpdatedDec 17, 2025
• TypeScript

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

• UpdatedApr 1, 2024
• Coq

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

• UpdatedJun 13, 2025
• Rust

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

• UpdatedOct 12, 2025

Verified Software Toolchain

• UpdatedNov 20, 2025
• Rocq Prover

A verification toolchain for Rust programs

• UpdatedDec 17, 2025
• OCaml

ACL2 System and Books as Maintained by the Community

• UpdatedDec 18, 2025
• Common Lisp

TLA+ language support for Visual Studio Code

• UpdatedDec 11, 2025
• TypeScript

Verification framework and tool for higher-order Scala programs

• UpdatedDec 17, 2025
• Scala

Links to tools by subject

• UpdatedMar 19, 2024

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

• UpdatedDec 16, 2025
• Python

Research on theory of programming languages λ, compilers, interpreters, functional programming, formal methods, logic etc.

• UpdatedAug 30, 2024

Interface with the rustc compiler for the purpose of program verification

• UpdatedDec 17, 2025
• Rust

Learn TLA+ for free! No prior experience necessary!

• UpdatedDec 9, 2025
• TLA