#区块链#Symbolic execution tool
A Proof-oriented Programming Language
Automatic verification of LLVM optimizations
pySMT: A library for SMT formulae manipulation and solving
Simple Theorem Prover, an efficient SMT solver for bitvectors
APALACHE: symbolic model checker for TLA+ and Quint
SMACK Software Verifier and Verification Toolchain
Verification framework and tool for higher-order Scala programs
#区块链#Monitor smart contracts deployed on blockchain and test against vulnerabilities with Mythril. It was presented at DEFCON 2019.
An aggregate of MEV resources, libraries, research papers, and strategies.
SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
Symbolic execution for Wasm, C, C++, Rust and Zig
Jupyter notebooks for tutorial on the Z3 SMT solver