Projects

ARGUS is a concolic execution engine for EVM bytecode that combines concrete execution traces with symbolic reasoning to systematically explore contract state space and find reachability bugs.

ATLAS is a Rust-based toolchain for building, composing, and verifying zero-knowledge proof circuits. It provides a typed constraint system that catches under-constrained and over-constrained bugs at compile time.