Live demo by request
TLA-Finance
Interactive finance verification demo and supporting models. The demo runs from a local environment, so email me to schedule a live walkthrough if the demo link is unavailable.
Selected work
Projects
A small index of formal methods, finance verification, smart-contract security, and automated testing work.
Smart contract security
Methodology for Verifying Smart Contract Against Price Manipulation Attacks
How I apply model checking and program analysis to detecting AMM-style attacks and price-oracle manipulation attacks.
Automated testing
Automated Testing Framework with Soufflé
An automated testing framework I developed in SPS-VeriSpec, using Soufflé-based analysis to connect specifications with generated checks.