Fuzzing & Formal Verification for Protocols and Distributed Systems
Stop guessing. Regain 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. Regain 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 formal methods, fuzzing, and hands-on systems engineering.
Fuzzing & Simulation
I build integrations and deploy advanced techniques — using tools like AFL, libFuzzer, cargo fuzz, the Wake fuzzer, or Echidna/Medusa — engineered for maximum coverage, reproducibility, and depth to uncover critical system behaviors.
Formal Modeling & Verification
Leveraging powerful tools like Alloy, TLA+, Lean4 or Certora Prover, I apply formal verification to prove the correctness of your protocols and systems, ensuring reliability beyond traditional testing.
Training & Applied Research
I provide training and mentorship in formal methods, fuzzing, and security best practices. Applied research in protocol design and security, including implementation guidance, paper review, and public speaking.
Security Consulting & PL Advice
Offering expert guidance on security strategy, threat modeling, audit preparation, post-deployment monitoring, and leveraging programming language design for enhanced system correctness and security.
Selected Work
Here's a sample of the work I’ve done in fuzzing, formal verification, and protocol correctness.Fuzzing Project for ▓▓▓▓▓▓▓▓ [client redacted]
2025 (ongoing)Ongoing fuzzing project. Targets deep functional security properties through concrete execution and simulation.
Solarkraft: Runtime Monitor
2024Developed a low-latency runtime monitor for Soroban smart contracts on Stellar blockchain.
GitHubVerified Accountability in Ethereum 3SF
2024Formal modeling of Ethereum 3-slot finality (3SF) consensus, exhaustively verified accountable safety.
GitHubIndependent Security Audits
2022–Now
Independent security reviews on Cantina, Code4rena and Sherlock.
Competitive verification contests with Certora Prover.
Apalache
2022–2024Co-developed the symbolic model checker for TLA+ and Quint. Modeled & verified formal specs around the Cosmos blockchain ecosystem.
GitHubQuint
2022–2024Contributed to 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, Practical Execution
I'm not just a researcher; I'm an engineer ready to roll up my sleeves and build the solutions we uncover together.
🚀 Agile and On-Demand
Access expert help exactly when you need it, without the long-term contracts or overhead of traditional options.
💎 Value-Driven and Focused on You
Get the expertise you need without the big firm price tag. I'm committed to finding the right tools and solutions tailored to your specific challenges.
🤝 Solo, But Not Isolated
My strong network of fellow researchers and engineers is an extension of my capabilities, ready to be tapped when needed.
🏆 Direct Accountability, Exceptional Quality
You work directly with me, ensuring a personal commitment to delivering outstanding results.
🗣️ Strong Communicator, Team Integration
While I operate independently, I communicate effectively and integrate well into existing teams.
Ready to get started? Limited Availability
Reach out and let’s talk about securing your protocol or verifying your system.
