Finance verification
TLA-Finance
Uses TLA+ model checking to investigate and explain suspicious outputs from agentic finance systems.
2 · Selected work
Projects
Smart contract security
Checking Smart Contracts for Price Manipulation Attacks
Uses TLA+ model checking and program analysis to detect when manipulated AMM or oracle prices can push smart contracts into unsafe states.
Automated testing
SPS-VeriSpec
Uses Python, Soufflé, and pytest to turn source-code relationships into reliable automated tests.