the champagne of beta embedded databases

The P programming language.

My own notes (drafts mostly) about software quality

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

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

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

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

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

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

Verified Software Toolchain

Links to tools by subject

ACL2 System and Books as Maintained by the Community

Verification framework and tool for higher-order Scala programs

TLA+ language support for Visual Studio Code

A verification toolchain for Rust programs

Learn TLA+ for free! No prior experience necessary!

MATLAB Independent, Small & Safe, High Integrity Tools - code formatter and more

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

Jupyter notebooks for tutorial on the Z3 SMT solver

SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada