A curated list of awesome smart contract datasets

Interactive formal verification tool for Yul programs

library learning w egraphs

Rewrite Rule Inference Using Equality Saturation

Formally verified smart contracts gives mathematical certainty across all inputs and execution paths. We bet that agents will make full formal verification practical.

Verification of BPF JIT compilers

Python implementation of Brahma (Synthesis of Loop-free Programs, PLDI'11)

A superoptimizer for LLVM IR

Solidity fuzzing tooling lives here.

Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations. Its name …

Some experiments with SMT solvers and GIMPLE IR

Executable formal model of the EVM and Yul in Lean 4.

EVMLiSA: an abstract interpretation-based static analyzer for EVM bytecode

Sui Move Fuzzer: 884 move-specific MetaMut-style mutations, harness, dicts, utilities

CodeAlchemist: Semantics-Aware Code Generation to Find Vulnerabilities in JavaScript Engines (NDSS '19)

language-agnostic program reducer.

A sample verifier for a toy language built on top of Boogie

A stack-driven generator of arbitrary WebAssembly programs

MetaMut is a mutation operator generator to facilitate compiler fuzzing.

LSVerifier - Large Systems Verifier

Automated DNN generation for fuzz testing and more

Repository for "Targeted Fuzzing for Unsafe Rust Code: Leveraging Selective Instrumentation"

FormatFuzzer is a framework for high-efficiency, high-quality generation and parsing of binary inputs.

LAVA: Large-scale Automated Vulnerability Addition

Collect crash (or UndefinedBehaviorSanitizer error) reports, triage, and estimate severity.

The efficient SMT-based context-bounded model checker (ESBMC)

A unit test-like interface for fuzzing and symbolic execution