Applied formal verification researcher, focused on practical rigor.
An exploratory guide to AI-assisted Lean proofs for financial protocols.
Benchmarking AI agents on generating price-manipulation exploits.
Introducing symbolic testing as a bridge from property tests to formal verification.
Formal verification of Ethereum system contracts written in assembly.
Verified Ethereum's deposit contract down to compiled bytecode, proving the incremental Merkle tree algorithm and finding critical bugs at both the source-code and compiler-output levels.
Built a deductive verifier for EVM bytecode, with case studies on high-profile smart contracts.
A security perspective on numerical precision and rounding errors in financial systems.
Executable security properties for tokenized vaults, a standard interface for yield-bearing financial applications.
Built and extensively tested a formal semantics of the user-level x86-64 instruction set, revealing bugs in manuals and existing semantics and enabling binary-level analysis.
Defined executable EVM semantics that passes the official test suite and generates interpreters, debuggers, and verifiers from the same semantics.
Built executable JavaScript semantics that passed all core conformance tests, exposed test-suite gaps, and found bugs in JavaScript engines.
Introduced Keq, a language-parametric equivalence checker, and used it to validate LLVM instruction selection from LLVM IR to x86-64 MachineIR.
Used failed proof attempts to guide CEGIS-style invariant synthesis for quantified and heap-manipulating programs.
Generated correct-by-construction verifiers from operational semantics of C, Java, and JavaScript, checking functional correctness of data-structure programs.