🔗 Explore a minimal execution engine in Rust for smart contracts, enabling clear state transitions and modular design for protocol experimentation.

🚀 Manage multiple dev services effortlessly with Devir, the terminal UI featuring colored logs, filtering, and MCP integration for streamlined workflows.

🌊 Access all your omg.lol services seamlessly with Triton, a modular native macOS client built in SwiftUI for a smooth desktop experience.

🛠️ Transform equations with symbolic regression in Rust, featuring WebAssembly support for browser-based demos and rapid experimentation.

Automatic verification of LLVM optimizations

Katamaran is a semi-automated separation logic verifier for the Sail specification language. It works on an embedded version of Sail called μSail and verifies separation logic-based contracts of functions by generating (succinct) first-order verification conditions.

An SMT solver frontend for OCaml

Python infrastructure to train paths selectors for symbolic execution engines.

Sandboxed data analysis with LLMs (powered by DuckDB)

Local node version of signal zero

Symbolic-execution-based verifier for the Viper intermediate verification language.

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

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

CLI tool, Ghidra plug-in, and Haskell library for analyzing binaries using under-constrained symbolic execution

Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE

ECE653-s2024 (Software Testing, Quality Assurance and Maintenance): Course project on implementing depth-first search and breadth-first search on a Python-based symbolic execution engine

SymWP, a concolic analysis framework designed specifically for WordPress plugin security. SymWP integrates an off-the-shelf symbolic execution engine and targets the PHP interpreter, allowing it to analyze plugin behavior at a semantic level with minimal human intervention.

symbolic execution plugin for binary ninja

ConcoLLMic: the first language- and theory-agonistic concolic execution engine via LLM agents