Fuzzing & Formal Verification for Protocols and Distributed Systems
I’m Dr. Thomas Pani. I make protocols boring.
Know your implementation behaves correctly – backed by evidence.
Fuzzing & Formal Verification for Protocols and Distributed Systems
I’m Dr. Thomas Pani. I make protocols boring.
Know your implementation behaves correctly – backed by evidence.
What I Do
I help protocol teams ship robust-by-design systems – from smart contracts to distributed infrastructure – by applying advanced reliability techniques like fuzzing, simulation, and formal verification.
Precision Code Review
Deep, human-in-the-loop reviews focused on real risk – not pattern matches. Clear findings, prioritized fixes, and support through remediation.
Deliverables: prioritized risk report, concrete patch guidance, and verification of applied fixes.
Fuzzing & Simulation
Targeted harnesses and scenario exploration to stress high-risk paths with reproducible failures and meaningful coverage.
Deliverables: CI-ready harnesses, failure corpus with repros, and coverage/scenario reports.
Formal Methods
For components where failure is existential: specify critical properties and prove what must hold with TLA+/Quint, SMT, or Lean.
Deliverables: executable specs, formally stated invariants, counterexamples tied to code.
Capabilities & Tooling
I choose tools that maximize signal: reproducible bugs, meaningful coverage, and verification of critical invariants.
Some Languages & Targets
Fuzzing & Simulation
Formal Methods & Solvers
Selected Work
Here's a sample of the work I’ve done in protocol correctness:Aztec Governance Protocol: Formal Verification
2025Massively parallel symbolic verification of 125 invariants across a multi-contract governance system.
Verified Accountability in Ethereum 3SF
2024Formal modeling of Ethereum 3-slot finality (3SF) consensus, exhaustively verified accountable safety.
Independent Security Audits
2022–NowIndependent security reviews on Cantina, Code4rena and Sherlock. Verification contests with Certora Prover.
Solarkraft: Runtime Monitor
2024Developed a low-latency runtime monitor for Soroban smart contracts on Stellar blockchain.
GitHubApalache
2022–NowCore team of Apalache, the symbolic model-checker for TLA+ and Quint. Apalache has been used to verify Ethereum and Tendermint consensus, L2 governance protocols, and Cosmos SDK/IBC.
GitHubQuint
2022–2024Dev team member for Quint, language and tooling for writing formal TLA+ specifications in a modern way.
Ready to get started? Limited Availability
Reach out and let’s talk about securing your protocol.
