The P programming language.
Creusot helps you prove your Rust code is correct.
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
HACL*, a formally verified cryptographic library written in F*
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.
十分钟魔法练习
Unified Rust framework for building, verifying, and testing web apps. Kernel-based architecture for Lean 4 verification and GPU acceleration. Built-in red-teaming tools for automated vulnerability detection.
Observer Patch Holography: finite observer consensus, machine-checked mathematics and reproducible models for reconstructing physical structure.
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."