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 — 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, verification of remediations.
Best when: you’ve scoped targets and want high-signal results without noise.
Fuzzing & Simulation
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 Methods
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 an L2 blockchain governance protocol with Apalache & Quint.
Verified Accountability in Ethereum 3SF
2024Formal modeling of Ethereum 3-slot finality (3SF) consensus, exhaustively verified accountable safety.
GitHubIndependent 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 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.
Ready to get started? Limited Availability
Reach out and let’s talk about securing your protocol.
