Welcome to the ultimate list of resources for formal verification/model checking 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.
Inspired by awesome-provable and awesome-open-hardware-verification!
-
Software
-
Hardware
-
Books - Textbooks commonly referred to
-
Courses - Online courses (YouTube, university courses)
-
Testbench Frameworks which make writing testbenches easier
-
Verification Guides and blog posts on how to actually go about verifying a hardware design
-
Conferences where new work on open source hardware verification is talked about
-
More Links - Video presentations about formal proof of code topics
- Panther - This tool presents a novel approach to bolstering network protocol verification by integrating the Shadow network simulator with the Ivy formal verification tool to check time properties. Furthermore, it extends Ivy’s capabilities with a dedicated time module, enabling the verification of complex quantitative-time properties.
- ivy - IVy is a research tool/language intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques.
- Uppaal - Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).
- BLAST - 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 .
- PRISM - PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. It has been used to analyse systems from many different application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, biological systems and many others.
- SPIN - Spin is a widely used open-source software verification tool. The tool can be used for the formal verification of multi-threaded software applications. The tool was developed at Bell Labs in the Unix group of the Computing Sciences Research Center, starting in 1980, and has been available freely since 1991. Spin continues to evolve to keep pace with new developments in the field. In April 2002 the tool was awarded the ACM System Software Award. [read more]
- TLA+ - TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones. It's based on the idea that the best way to describe things precisely is with simple mathematics.
- Coq - Formal proof management system.
- Isabelle - Generic proof assistant.
- HOL - Proof assistant for higher-order logic.
- LEAN - Theorem prover developed at Microsoft Research.
- K Framework - Rewrite-based executable semantic framework.
- Viper - Language and tools for permission-based reasoning.
- Panther - This tool presents a novel approach to bolstering network protocol verification by integrating the Shadow network simulator with the Ivy formal verification tool to check time properties. Furthermore, it extends Ivy’s capabilities with a dedicated time module, enabling the verification of complex quantitative-time properties.
/
/
- A Practical Approach to Coverage in Model Checking - Scientific paper
- ivy-syntax-highlight - Bare minimum syntax highlight definitions (most likely incomplete) for the Ivy language.
- ivy - IVy is a research tool/language intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques.
- Caml - 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.
- Symbiyosys - SymbiYosis a front-end driver program for Yosys-based formal hardware verification flows. SymbiYosys provides flows for the following formal tasks: Bounded verification of safety properties (assertions), Unbounded verification of safety properties, Generation of test benches from cover statements, Verification of liveness properties
- riscv-formal - A re-usable formal verification framework for RISC-V CPU designs.
- MCY - mcy is a new tool to help digital designers and project managers understand and improve testbench coverage. [...] Given a self checking testbench, mcy generates 1000s of mutations by modifying individual signals in a post synthesis netlist. These mutations are then filtered using Formal Verification techniques, keeping only those that can cause an important change in the design’s output. All mutated designs are run against the testbench to check that the testbench will detect and fail for a relevant mutation. The testbench can then be improved to get 100% complete coverage
- EBMC / CBMC - EBMC is a Model Checker for hardware designs. It includes both bounded and unbounded analysis, i.e., it can both discover bugs and is also able to prove the absence of bugs. It can read Netlists (ISCAS89 format), Verilog, System Verilog and SMV files. Properties can be given in LTL or a fragment of System Verilog Assertions
- seL4 - Operating-system kernel with an end-to-end proof of implementation correctness and security enforcement.
- Certikos - Certified Kit Operating System.
- Compcert - Formally verified compiler for C.
- Bedrock - Coq library for verification.
- HACMS - High-Assurance Cyber Military Systems.
- Genode - Novel OS architecture.
- Verilator - Verilator is "the fastest free Verilog HDL simulator". From a verification perspective it supports line coverage, signal toggle coverage and limited specification of functional coverage using SystemVerilog Assertions. It also allows one to write testbenches in C++ or SystemC.
- Icarus Verilog -The excellent Icarus Verilog simulator. Slower than Verilator, but it supports full 4-state simulation (i.e. X's and Z's).
- LibreCores CI - LibreCores CI is a service, which provides Continuous Integration of projects being hosted on LibreCores. The objective of the service is to improve the contributor experience and to increase trust to projects by providing automated testing and health metrics of the projects.
- FuseSoc - FuseSoC is an award-winning package manager and a set of build tools for HDL (Hardware Description Language) code. Its main purpose is to increase reuse of IP (Intellectual Property) cores and be an aid for creating, building and simulating SoC solutions
- AAPG (Automated Assembly Program Generator) - Generator for assembly programs.
- riscv-dv - Instruction sequence generator for RISC-V.
- rggen - Code generation tool for configuration and status registers.
- FORCE-RISCV - Instruction sequence generator for RISC-V.
- covered - Coverage analysis tool.
- svlint - Linter for SystemVerilog.
- sv-parser - SystemVerilog parser.
- Surelog - SystemVerilog pre-processor and parser.
- cocotb - Python based testbench environment for many simulators.
- python-uvm - A port of UVM 1.2 to Python and cocotb.
- cocotb-coverage - Functional coverage and constrained randomization extensions for Cocotb.
- Verification IPs - Various cocotb packages for common interfaces: AXI/Ethernet/PCIE.
- fvutils/pyvsc - Python packages providing a library for verification stimulus and coverage.
- chiselverify - UVM-like verification for the Chisel HDL.
- UVVM - Universal VHDL Verification Methodology.
- OSVVM - Open Source VHDL Verification Methodology.
- VUnit - Unit testing framework for VHDL/SystemVerilog.
- V3 - Verification framework.
- ROHD Verification Framework - Hardware verification framework upon ROHD for building and executing testbenches.
- uvm_axi - AXI bus verification IP.
- AXI Bus Formal VIP - Formal verification IP for AXI bus.
- AXI Bus Functional Model tvip-axi - Functional model for AXI bus.
- AXI SystemVerilog Modules and Verification Infrastructure - SystemVerilog modules and verification infrastructure for AXI bus.
- APB Bus Functional Model tvip-apb - Functional model for APB bus.
- USB 1.1 Test Suite - Test suite for USB 1.1.
- Cocotb Verification IPs - Various cocotb packages for common interfaces: AXI/Ethernet/PCIE.
- RISC-V-TLM - A SystemC transaction level model of RISC-V.
- Idris - General purpose pure functional programming language with dependent types.
- Agda - Dependently typed functional programming language.
- UR/Web - Ur plus a special standard library for dynamic web applications.
- Haskell - An advanced, purely functional programming language.
- Liquid Haskell - Refines Haskell's types with logical predicates for compile-time property enforcement.
- Elm - Type-safe functional programming language for declaratively creating web browser-based graphical user interfaces.
- Dan Gisselquist Formal Verification Blogs - Blog posts on formal verification.
- Verification Gentleman Blog - Blog on verification topics.
- Bits, Bytes and Gates - Blog covering formal verification and hardware design.
- ORCONF - Open Source Digital Design Conference.
- OSDA - Open Source Digital Architecture workshop.
- CHIPS Alliance Workshop on Open Source Design Verification - Workshop on open source design verification.
- Workshop on Open-Source EDA Technology (WOSET) - Workshop on open-source EDA technology.
- The Little Prover - Introduction to inductive proofs for computer programs.
- Certified Programming with Dependent Types - Textbook on practical engineering with Coq.
- Software Foundations - Introduction to the mathematical underpinnings of reliable software.
- HoTT: Homotopy Type Theory: Univalent Foundations of Mathematics
- MCB: Mathematical Components
- DeepSpec Summer School - Videos about deep specification, Coq tutorials.
- Adam Chlipala Videos:
- Coming Soon Machine-Checked Mathematical Proofs in Everyday Software and Hardware Development
- Lecture 1, OPLSS 2015
- Bedrock: A Software Development Ecosystem Inside a Proof Assistant
- Ur/Web: A Simple Model for Programming the Web
- Proof Engineering
- Coq Proof Assistant and Its Applications to Programming-Language Semantics
- Type-Drive Development in Idris - Edwin Brady
- Benjamin Pierce - Software Foundations Course
- Learning Automated Theorem Proving - Stackexchange post about learning.
- Curry-Howard - Direct relationship between computer programs and mathematical proofs.
- Hoare logic - Formal system for reasoning rigorously about the correctness of computer programs.
- Designing A Theorem Prover (Paulson, Cambridge, 1990)
- Rolf Rolles Program Synthesis in Reverse Engineering - Assume you generate all possible programs.
- The Open-Source seL4 Kernel. Military-Grade Security Through Mathematics - SFO17-417
- DARPA Hack Proof Drones
- Pentagon Wants Unhackable Helicopters
- Hacker-Proof Code Confirmed - Computer scientists can prove certain programs to be error-free with the same certainty that mathematicians prove theorems.
- CertiKOS enables creation of secure system kernels - Secure concurrent kernel for x86 and ARM.
- seL4 Is Free – What Does This Mean For You?
- From L3 to seL4: What Have We Learnt in 20 Years of L4 Microkernels?
- seL4 introduction: Capability--based Access Model - Chinese, translation?
- seL4 playlist
- Creating drones that can't be hacked
- HACMS: Protecting Military Systems from Hackers
Your contributions are always welcome! Feel free to submit a pull request with your suggestions.