awesome-formal-verification
github.com/elniak/awesome-formal-verification ↗Welcome to the ultimate list of resources for formal verification techniques and tools. This repository aims to provide an organized collection of high-quality resources to help professionals, researchers, and enthusiasts stay updated and advance their knowledge in the field.
Use this list with your AI agent
Add the Context Awesome MCP server to Claude, Cursor, or any MCP client, then ask:
"Show me tools resources from awesome-formal-verification"
Installation instructions →What's inside
Hardware Verification
- AAPG (Automated Assembly Program Generator)Tools
Generator for assembly programs.
- ABCTools
ABC: System for Sequential Logic Synthesis and Formal Verification. ABC notably provides combinational equivalence checking (CEC) and sequential equivalence checking (SEQ) engines.
- AgdaLanguages
Dependently typed functional programming language.
- Agda GitHubLanguages
- Agda User ManualLanguages
- APB Bus Functional Model tvip-apbTools
Functional model for APB bus.
Software Verification
- AlloyTools
Alloy is a high-level formal modeling language for specifying structural and behavioural aspects of systems using simple mathematics (first-order logic and relations). Comes with a bounded model checker which can find both satisfying and falsifying examples, as well as a unique visualization tool.
- A Practical Approach to Coverage in Model CheckingTools
Scientific paper.
- BLASTTools
BLAST is a software model checker for C programs. The goal of BLAST is to be able to check that software satisfies behavioral properties of the interfaces it uses. Blast uses counterexample-driven automatic abstraction refinement to construct an abstract model which is model checked for safety properties. The abstraction is constructed /on-the-fly/, and only to the /required precision/. The BLAST project is supported by the National Science Foundation .
- CamlLanguages
Caml is a general-purpose programming language, designed with program safety and reliability in mind. It is very expressive, yet easy to learn and use. Caml supports functional, imperative, and object-oriented programming styles. It has been developed and distributed by INRIA, a French research institute in computer science and applied mathematics, since 1985.
- Frama-CTools
Frama-C is an extensible and collaborative platform dedicated to source-code analysis of C software.
- HOLTools
Proof assistant for higher-order logic.
Courses
- Bedrock: A Software Development Ecosystem Inside a Proof Assistant
- Benjamin Pierce - Software Foundations Course
Software Foundations Course
- Coming Soon Machine-Checked Mathematical Proofs in Everyday Software and Hardware Development
- Coq Proof Assistant and Its Applications to Programming-Language Semantics
- DeepSpec Summer School
Videos about deep specification, Rocq (previously Coq) tutorials.
- Learning Automated Theorem Proving
Stackexchange post about learning.
Blogs
- Bits, Bytes and Gates
Blog covering formal verification and hardware design.
- Dan Gisselquist Formal Verification Blogs
Blog posts on formal verification.
- Verification Gentleman Blog
Blog on verification topics.
Books
- Certified Programming with Dependent Types
Textbook on practical engineering with Rocq (previously Coq).
- HoTT: Homotopy Type Theory: Univalent Foundations of Mathematics
- Latest draft
- MCB: Mathematical Components
- Software Foundations
Introduction to the mathematical underpinnings of reliable software.
More
- CertiKOS enables creation of secure system kernels
Secure concurrent kernel for x86 and ARM.
- Creating drones that can't be hacked
- Curry-Howard
Direct relationship between computer programs and mathematical proofs.
- DARPA Hack Proof Drones
- Designing A Theorem Prover (Paulson, Cambridge, 1990)
- From L3 to seL4: What Have We Learnt in 20 Years of L4 Microkernels?
Conferences
- CHIPS Alliance Workshop on Open Source Design Verification
Workshop on open source design verification.
- ORCONF
Open Source Digital Design Conference.
- OSDA
Open Source Digital Architecture workshop.
- Workshop on Open-Source EDA Technology (WOSET)
Workshop on open-source EDA technology.
Showing a sample of 123 resources. View the full list on GitHub →