Demo available by request
TLA-Finance
Formal models and an interactive walkthrough for investigating suspicious outputs from an agentic finance system.
Selected work
Projects
Smart contract security
Checking Smart Contracts for Price Manipulation Attacks
I check whether manipulated AMM or oracle prices can push a contract into unsafe behavior.
Automated testing
SPS-VeriSpec
SPS-VeriSpec reads Python code, runs Soufflé rules over what it finds, and turns the strongest results into pytest tests. Uncertain results stay marked for review.