| ABC |
System for Sequential Logic Synthesis and Formal Verification
|
| Aya Prover |
A proof assistant designed for formalizing math and type-directed programming.
|
| Cobra |
Cobra is a fast code analyzer that can be used to interactively probe and query up to millions of … |
| DNNF |
DNNF is a tool for applying falsification methods such as adversarial attacks to the checking of DNN … |
| DNNV |
A framework for verification and analysis of deep neural networks.
|
| easy-rte |
Toolchain to automatically generate and verify HW or SW runtime enforcers from text-based framework
|
| fbPDR |
Forward / backward PDR/IC3 implementation.
|
| Fiat |
Mostly Automated Synthesis of Correct-by-Construction Programs
|
| Geyser |
Simple implementation of PDR and CAR model checking algorithms
|
| hlola |
|
| Incremental Neural Network Verifiers |
Incremental Verifiers for Neural Networks
|
| knuckledragger |
Knuckledragger is an attempt at creating a down to earth, highly automated interactive proof … |
| Lakeroad |
FPGA synthesis tool powered by program synthesis
|
| minsynth |
[ Not Maintained Since 2019 ] program synthesis is possible
|
| neuralkanren |
[ Not Maintained Since 2018 ] Neural Guided Constraint Logic Programming for Program Synthesis
|
| Paranoid Scientist |
Runtime software verification and automated testing for scientific software in Python
|
| PROSE |
Microsoft Program Synthesis using Examples SDK is a framework of technologies for the automatic … |
| QEA |
[ Not Maintained Since 2019 ] Quantified Event Automata (QEA) is a specification formalism … |
| Qrhl-tool |
Qrhl-tool is an interactive theorem prover for qRHL (quantum relational Hoare logic), specifically … |
| R2U2 |
The Realizable Responsive Unobtrusive Unit is an online runtime monitor framework.
|
| Reach |
Reach is a symbolic finite state reachability checker. One could also say that Reach is a safety … |
| ROSMonitoring |
ROSMonitoring is a framework developed for verifying at runtime the messages exchanged in a ROS … |
| Tree Diffusion |
Diffusion on syntax trees for program synthesis
|
| VeRAPAk |
VeRAPAk is an algorithmic framework for optimizing formal verification techniques for deep neural … |
| VeriGauge |
A united toolbox for running major robustness verification approaches for DNNs.
|
| Agda 2 |
Agda is a dependently typed programming language / interactive theorem prover.
|
| Megalodon |
Megalodon is an open source interactive theorem prover and proof checker.
|
| Caesar |
Caesar is a deductive verifier for probabilistic programs.
|
| Dafny |
Dafny is a verification-aware programming language that has native support for recording … |
| IVy |
[ Not Maintained Since 2023 ] IVy is a research tool intended to allow interactive development of … |
| Kani |
The Kani Rust Verifier is a bit-precise model checker for Rust.
|
| Loom |
Loom is a testing tool for concurrent Rust code.
|
| Loom |
Shuttle is a library for testing concurrent Rust code.
|
| Miri |
Miri is an Undefined Behavior detection tool for Rust.
|
| Verus |
Verus is a tool for verifying the correctness of code written in Rust.
|
| BEAGLE |
Beagle is an automated theorem prover for first-order logic with equality over linear … |
| Bitwuzla |
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … |
| Boolector |
[ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … |
| CaDiCaL |
CaDiCaL is a simplified satisfiability solver.
|
| Colibri |
Colibri is an SMT solver.
|
| CryptoMiniSat |
CryptoMiniSat is a SAT solver.
APIs and Bindings This tool is available through the following … |
| ESBMC |
ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying … |
| Gappa |
Gappa is a tool intended to help verifying and formally proving properties on numerical programs … |
| Glucose |
Glucose is a SAT solver.
|
| ImSpin |
ImSpin is a frontend for the SPIN model checker, providing an environment for users engaged in model … |
| JANI |
The JANI specification defines the jani-model model interchange format and the jani-interaction tool … |
| Lingeling |
Lingeling is a SAT solver.
|
| Mercury |
[ Not Maintained Since 2020 ] Mercury is a Model Checker developed for multicore, multiprocessors … |
| Metis |
[ Not Maintained Since 2020 ] Metis is an automatic theorem prover for first order logic with … |
| MetiTarski |
MetiTarski is an automatic theorem prover based on a combination of resolution and a decision … |
| MiniSat |
[ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help … |
| Momba |
Momba is a Python framework for dealing with quantitative models centered around the JANI-model … |
| MUNTA |
[ Not Maintained Since 2020 ] MUNTA is a model checker for the popular realtime systems modeling … |
| Princess |
Princess is a theorem prover (aka SMT Solver) for Presburger arithmetic with uninterpreted … |
| Profound |
[ Not Maintained Since 2011 ] Profound is an experiment in subformula linking as an interaction … |
| Q3B |
[ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which … |
| SMT-RAT |
SMT-RAT is an SMT Real Algebra Toolbox.
APIs and Bindings This tool is available through the … |
| STAMINA |
A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces … |
| stateright |
stateright is a Rust library for model checking systems, with an emphasis on distributed systems.
|
| STP |
STP is a constraint solver for quantifier-free bitvectors.
APIs and Bindings This tool is available … |
| Why3 |
Why3 is a platform for deductive program verification.
|
| Z3 |
Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
APIs and Bindings This … |