Symbolic execution tool

• UpdatedOct 14, 2025
• Python

A Proof-oriented Programming Language

• UpdatedNov 5, 2025
• F*

Liquid Types For Haskell

• UpdatedNov 5, 2025
• Haskell

Transpiler of Python to many other languages

• UpdatedOct 28, 2025
• Python

Automatic verification of LLVM optimizations

• UpdatedOct 16, 2025
• C++

Better parametric search for components available for JLC PCB assembly

• UpdatedNov 5, 2025
• JavaScript

pySMT: A library for SMT formulae manipulation and solving

• UpdatedSep 5, 2025
• Python

Simple Theorem Prover, an efficient SMT solver for bitvectors

• UpdatedOct 23, 2025
• C++

APALACHE: symbolic model checker for TLA+ and Quint

• UpdatedNov 5, 2025
• Scala

SMACK Software Verifier and Verification Toolchain

• UpdatedApr 18, 2025
• C

Rust bindings for the Z3 solver.

• UpdatedOct 21, 2025
• Rust

Verification framework and tool for higher-order Scala programs

• UpdatedSep 18, 2025
• Scala

An aggregate of MEV resources, libraries, research papers, and strategies.

• UpdatedJan 11, 2024

Monitor smart contracts deployed on blockchain and test against vulnerabilities with Mythril. It was presented at DEFCON 2019.

• UpdatedMay 23, 2025
• Python

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.

• UpdatedOct 31, 2025
• Haskell

Seamless bug-finding for Wasm, C, C++, Rust and Zig

• UpdatedNov 4, 2025
• OCaml

Tactics for discharging Lean goals into SMT solvers.

• UpdatedOct 28, 2025
• Lean

JavaSMT - Unified Java API for SMT solvers.

• UpdatedNov 4, 2025
• Java

A fuzzing framework for SMT solvers

• UpdatedJul 27, 2023
• Python

Datalog with support for SMT queries and first-order functional programming

• UpdatedNov 3, 2025
• Java