ElNiak / awesome-formal-verificationLinks
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.
☆43Updated 5 months ago
Alternatives and similar repositories for awesome-formal-verification
Users that are interested in awesome-formal-verification are comparing it to the libraries listed below
Sorting:
- Python tools for the K Framework☆13Updated last year
- Binary analysis in HOL☆41Updated 3 months ago
- Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.☆36Updated 10 months ago
- CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.☆32Updated last month
- A framework for formally verifying hardware security modules to be free of hardware, software, and timing side-channel vulnerabilities 🔏☆35Updated 5 months ago
- System for verifying the correctness of generated Copilot programs☆17Updated 2 months ago
- Connecting bv_decide to SMTLIB.☆13Updated 2 weeks ago
- Generate Soufflé Datalog types, relations, and facts that represent ASTs from a variety of programming languages.☆69Updated last week
- Program Analysis, Software Verification & Testing. Python3, CAS, Dafny, Z3, CVC4, UCLID, ZChaff, NuSMV, AFL, Scala, CBMC & LLVM Framework…☆37Updated 2 years ago
- Tutorials and courses for Z3☆84Updated last month
- Documentation☆44Updated 2 months ago
- Synthesizes efficient Z3 strategies tailored to your problem set! Repo for the IJCAI'24 paper: Layered and Staged Monte Carlo Tree Search…☆17Updated 2 weeks ago
- Quantum circuits compiler with staging and continuations☆17Updated 7 months ago
- Symbolic execution tool for Sail ISA specifications☆73Updated last week
- Symbolic-execution-based verifier for the Viper intermediate verification language.☆108Updated this week
- Lean models of Rust libraries☆18Updated 10 months ago
- VSCode extension that is designed to help automate writing of Coq proofs.☆109Updated last month
- Formal specification and verification of hardware, especially for security and privacy.☆126Updated 3 years ago
- Unicorn: Symbolic Execution, Bounded Model Checking, and Code Optimization of RISC-V Code using Classical Solvers and Quantum Computers☆35Updated last week
- Introduction to homotopy type theory (reading course), LP2 2023, offered via DAT235/DIT577: Research-oriented course in Computer Science …☆14Updated last year
- Computer Systems Lab☆11Updated 2 weeks ago
- ☆40Updated 2 weeks ago
- Multi-engine SMT-based automatic model checker for safety properties of Lustre programs☆104Updated last week
- The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).☆32Updated 5 months ago
- Definition of the Viper intermediate verification language.☆87Updated this week
- A precise and scalable pointer analysis for LLVM, written in Ascent☆65Updated 4 months ago
- work in progress, playing around with btor2 in rust☆11Updated 3 weeks ago
- Actor-based Runtime Verification Tool☆18Updated 2 years ago
- Compositional Verification of Composite Byzantine Protocols☆12Updated 10 months ago
- IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform f…☆93Updated last month