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

A Fast and Safe Python based on PyPy

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

formally verified category theory library

ACL2 System and Books as Maintained by the Community

A selection of formal proofs in Coq.

Release snapshots of the Frama-C platform for source code analysis

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

A curated set of links to formal methods involving provable code.

A Julia package for calculus with convex sets

High-assurance implementation of the Ouroboros protocol family

Correctness proofs of Ethereum token contracts

Public snapshots of "ACSL by Example"

A List of Free and Open Source Hardware Verification Tools and Frameworks

XCrypto: a cryptographic ISE for RISC-V

The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.

Reachability and Safety of Nondeterministic Dynamical Systems

Formal message specification and generation of verifiable binary parsers and message generators

Coq formalizations and proofs of (data) structures and algorithms.

Imandra FIX Engine

CoreIR Symbolic Analyzer

Node and GUI for the Zen Protocol.

Information about the Interchain Foundation Funding Program

Awesome ASIC design verification

Linux kernel library functions formally verified.

Formal specification and verification of hardware, especially for security and privacy.

The Verifiably Safe Reinforcement Learning Framework

A simple REPL for the TLA+ language, using the TLC model checker.