Fuzzing & Formal Verification for Protocols and Distributed Systems

Find deep bugs. Prove critical properties. Ship with confidence.

Dr. Thomas Pani

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.
Best when correctness is non-negotiable.

👉  Secure your protocol

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.

🌿 Evergreen

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.

🔥 High Coverage

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.

👑 High Assurance

Formal Methods

For components where failure is existential: model 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 to maximize signal: reproducible bugs, explainable counterexamples, and proofs for critical invariants.

Some Languages & Targets

🛠️ Solidity 🦀 Rust 🐹 Go 🐍 Python 🟦 TypeScript 📐 Lean

Focus: smart contracts, protocol logic, distributed systems.

Fuzzing & Simulation

AFL cargo-fuzz libFuzzer Echidna Medusa Wake

Goal: high-risk path coverage with reproducible failures & scenario exploration.

Formal Methods & Solvers

TLA+ / Quint Alloy Lean4 SMT: Z3 SMT: CVC5

Outcome: invariant proofs, counterexamples, and machine-checked guarantees.

Selected Work

Here's a sample of the work I’ve done in protocol correctness:

Aztec Governance Protocol: Formal Verification

2025

Massively parallel symbolic verification of 125 invariants across a multi-contract governance system.

GitHub | PDF report | → writeup (recommended)
🔹 Aztec 🦄 Solidity Quint Apalache Formal Verification

Verified Accountability in Ethereum 3SF

2024

Formal modeling of Ethereum 3-slot finality (3SF) consensus, exhaustively verified accountable safety.

Tech report (arXiv) | GitHub
🦄 Ethereum (core proto) Formal Verification TLA+ Alloy SMT Python

Independent Security Audits

2022–Now

Independent security reviews on Cantina, Code4rena and Sherlock. Verification contests with Certora Prover.

🌌 Cairo / StarkNet 🌟 Soroban / Stellar 🦄 Solidity / Ethereum 🧬 Various Ecosystems

Solarkraft: Runtime Monitor

2024

Developed a low-latency runtime monitor for Soroban smart contracts on Stellar blockchain.

GitHub
🌟 Stellar Soroban Rust TypeScript Go

Apalache

2022–Now

Core 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.

GitHub
🧬 Various 🪐 Cosmos TLA+ Formal Verification

Quint

2022–2024

Dev team member for Quint, language and tooling for writing formal TLA+ specifications in a modern way.
 

GitHub
🧬 Various Quint TLA+ Simulation Language Tooling

Ready to get started? Limited Availability

Reach out and let’s talk about securing your protocol.
Typical engagements: 2–4 weeks (review/fuzzing) or 4–8 weeks (formal methods), depending on scope.

Email Me Telegram Quick scope call (to see if I'm a fit)