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 system-level code review, fuzzing, and formal methods — 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 help protocol teams ship robust-by-design systems — from smart contracts to distributed infrastructure — with a practical pipeline: pre-audit diagnostics → code review → (optionally) fuzzing/simulation and formal verification.
Protocol Readiness Review
A one-week pre-audit diagnostic to pinpoint what to audit, where risk lives, and whether deeper analysis is worth it.
Deliverables
- Risk map of key assumptions
- Audit-scope & priority plan
- 1-hour debrief call
Outcomes
🔁 Fewer re-audits
💸 Smarter audit spend
🕒 Faster delivery
😬 Fewer surprises
Timeline & Cost
Duration: 1 week
Fee: $9.8 k flat
A week of clarity now prevents months of uncertainty later.
Limited availability · 1–2 slots / month
Precision Code Review
Deep, human-in-the-loop reviews focused on real risk — not pattern matches. Clear findings, prioritized fixes, verification of remediations.
Best when: you’ve scoped targets and want high-signal results without noise.
High-Coverage Fuzzing
Targeted harnesses and scenario exploration to stress high-risk paths with reproducible failures and meaningful coverage.
Best when: complex state machines / multi-actor flows need behavioral coverage beyond tests.
Formal Verification
For components where failure is existential: model critical properties and prove what must hold with TLA+/Quint, SMT, or Lean.
Best when: correctness is non-negotiable (consensus, bridges, governance, asset safety).
Capabilities & Tooling
A pragmatic toolchain for protocol correctness — from languages to fuzzing harnesses and formal verifiers.
Some Languages & Targets
Focus: smart contracts, protocol logic, distributed systems.
Fuzzing & Simulation
Goal: high-risk path coverage with reproducible failures & scenario exploration.
Formal Methods & Solvers
Outcome: invariant proofs, counterexamples, and machine-checked guarantees.
Selected Work
Here's a sample of the work I’ve done in protocol correctness:Formal Verification for ▓▓▓▓▓▓▓▓ [client redacted]
2025Formal verification of L2 governance protocol with Apalache & Quint.
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.