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.
A security perspective on numerical precision and rounding errors in financial systems.
Formal verification of Ethereum system contracts written in assembly.
Introducing symbolic testing as a bridge from property tests to formal verification.
Executable security properties for tokenized vaults, a standard interface for yield-bearing financial applications.
Introduced Keq, a language-parametric equivalence checker, and used it to validate LLVM instruction selection from LLVM IR to x86-64 MachineIR.
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 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.
Built a deductive verifier for EVM bytecode, with case studies on high-profile smart contracts.
Defined executable EVM semantics that passes the official test suite and generates interpreters, debuggers, and verifiers from the same semantics.
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.
Built executable JavaScript semantics that passed all core conformance tests, exposed test-suite gaps, and found bugs in JavaScript engines.