Learn Lean 4 with PLFA proofs.

⚠️ Experimental | Prototype

A dynamic analysis framework for WebAssembly programs.

Arguzz is a zero knowledge virtual machine fuzzer

Recent papers about metamorphic testing

An Ethereum Dynamic Analyzer, a.k.a, open-sourced transaction explorer similar to Phalcon/EthTx/TxTracer

Fairness Verification of Smart Contracts

Automated verification of uniqueness property for ZKP circuits

Combinatorial Interaction Testing Repository

A tool for Model Based Testing

Rust language proof-carrying data framework

Program synthesis based deobfuscation framework for the USENIX 2017 paper "Syntia: Synthesizing the Semantics of Obfuscated Code"

Manipulation, canonicalization and identification of mixed boolean-arithmetic symbolic expressions

MBA-Blast is a tool for simplification of MBA expressions.

Mixed Boolean-Arithmetic

Computable Polynomials in Lean.

A Dolev-Yao-model-guided fuzzer for TLS

egraphs + datalog!

Pattern matching and exhaustiveness checking algorithms implemented in Rust

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