The P programming language.
Creusot helps you prove your Rust code is correct.
HACL*, a formally verified cryptographic library written in F*
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
A static verifier for Rust, based on the Viper verification infrastructure.
CakeML: A Verified Implementation of ML
Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.
Plan, apply and roll back changes to a production ontology, with a blast radius report and a proof an auditor can re-check.
A verification toolchain for Rust programs
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
十分钟魔法练习
Observer Patch Holography: finite observer consensus, machine-checked mathematics and reproducible models for reconstructing physical structure.
An agent-native web security workspace. Find vulnerabilities through red-teaming. Formally verify properties of Rust codes in Lean 4.
CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.
A List of Free and Open Source Hardware Verification Tools and Frameworks
A gently curated list of companies using verification formal methods in industry
Authority control plane for autonomous work. EMILIA Gate enforces finite customer-owned mandates at protected executor boundaries; the open protocol keeps evidence verifiable.
Verified Software Toolchain
A framework for the elicitation, specification, formalization and analysis of requirements.
To associate your repository with the formal-verification topic, visit your repo's landing page and select "manage topics."