Fuzzing & Formal Verification for Protocols and Distributed Systems
Stop guessing. Ship with confidence.
I’m Dr. Thomas Pani. I help protocol teams ship with confidence using formal methods, fuzzing, and systems-level engineering — including smart contracts, distributed systems, and custom infrastructure.
Fuzzing & Formal Verification for Protocols and Distributed Systems
Stop guessing. Ship with confidence.
I’m Dr. Thomas Pani. I help protocol teams ship with confidence using formal methods, fuzzing, and post-deployment security — including smart contracts, distributed systems, and custom infrastructure.
What I Do
I go beyond audits to design and build robust-by-design systems — from smart contracts to distributed infrastructure — using a pipeline of code review, fuzzing, and formal verification.
Code Review & Security Audits
Humans see nuance.
Tools miss context.
Deep, human-in-the-loop reviews that focus on real risk: I trace critical paths, check invariants, and explore failure modes, then deliver prioritized, actionable findings with clear remediation. Every engagement includes audit prep, triage, and post-fix verification.
Formal Verification, Fuzzing & Simulation
Stress what can break.
Prove what must hold.
I combine targeted fuzzing and simulation with formal verification to uncover deep bugs and lock down correctness. Fuzzing drives high path coverage with reproducible failures; formal models prove invariants and deliver machine-checked guarantees.
Security Strategy, Guidance & Training
Design for safety.
Ship with confidence.
Threat modeling, audit readiness, and post-deploy monitoring anchored in deliberate architecture and design choices for correctness and safety. Cement it with training and mentorship that embed formal methods, fuzzing, and secure engineering in your team’s practice.
Not sure where to start? Most teams start with an audit.
Selected Work
Here's a sample of the work I’ve done in protocol correctness:Formal Verification for ▓▓▓▓▓▓▓▓ [client redacted]
2025Formal verification of Solidity components using Quint & Apalache.
Independent Security Audits
2022–NowIndependent security reviews on Cantina, Code4rena and Sherlock. Verification contests with Certora Prover.
Verified Accountability in Ethereum 3SF
2024Formal modeling of Ethereum 3-slot finality (3SF) consensus, exhaustively verified accountable safety.
GitHubSolarkraft: 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 formal specs of Ethereum 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.
Talks & Writing
I occasionally give talks and workshops on fuzzing, formal methods, and protocol safety — and write about what I learn along the way.
New! Workshop Recording
25-Minute Solidity Fuzzer: Fuzzing Smarter, Not Harder
Presented at Protocol Berg v2 - June 2025 » Learn more
Blog
📚 More ideas and research: read the blog.
How I Work
No big firm overhead. No locked-in retainers. Just focused, expert help when you need it.
Strategic Insight, Value‑Driven Execution
I'm not just a researcher; I'm an engineer ready to roll up my sleeves and build the solutions we uncover together. I'm committed to finding the right tools and approaches tailored to your specific challenges.
Flexible, Frictionless Collaboration
Work with me when you need to — no retainers, no red tape. I communicate clearly, share progress, and integrate smoothly with your tools and rhythms.
Personal Commitment, Scalable Support
You get my direct accountability and high standards on every project. And when scope grows, I tap a trusted network of researchers and engineers to extend capacity without adding overhead.
Ready to get started? Limited Availability
Reach out and let’s talk about securing your protocol.
