Systems, formal methods, and finance engineering

I design practical verification methods for financial and systems software.

I combine model checking, program analysis, and evidence from real failures to turn concrete risks into checks engineers can actually use.

Selected work

All projects

TLA-Finance

Formal models and trace-based analysis for investigating suspicious outputs from an agentic finance system.

Price Manipulation

I check whether manipulated AMM or oracle prices can push a contract into unsafe behavior.

SPS-VeriSpec

A Python tool that reads source code, uses Soufflé rules to connect what it finds, and turns the strongest results into pytest tests.