Symbolic execution tool

• UpdatedFeb 13, 2026
• Python

A Proof-oriented Programming Language

• UpdatedFeb 18, 2026
• F*

Liquid Types For Haskell

• UpdatedFeb 9, 2026
• Haskell

Transpiler of Python to many other languages

• UpdatedFeb 19, 2026
• Python

Automatic verification of LLVM optimizations

• UpdatedFeb 12, 2026
• C++

Better parametric search for components available for JLC PCB assembly

• UpdatedFeb 2, 2026
• 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

• UpdatedFeb 11, 2026
• Scala

Rust bindings for the Z3 solver.

• UpdatedFeb 14, 2026
• Rust

SMACK Software Verifier and Verification Toolchain

• UpdatedApr 18, 2025
• C

Verification framework and tool for higher-order Scala programs

• UpdatedFeb 18, 2026
• 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.

• UpdatedFeb 3, 2026
• Python

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

• UpdatedFeb 18, 2026
• OCaml

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

• UpdatedFeb 19, 2026
• Haskell

Tactics for discharging Lean goals into SMT solvers.

• UpdatedFeb 19, 2026
• Lean

JavaSMT - Unified Java API for SMT solvers.

• UpdatedFeb 20, 2026
• Java

A fuzzing framework for SMT solvers

• UpdatedDec 1, 2025
• Python

A verifier for automated and interactive proofs about transition systems.

• UpdatedFeb 19, 2026
• Lean