Protocol-State Guided Fuzzing of Distributed Systems
How annotations could help drive deep behavior and scenario coverage for distributed databases, consensus algorithms, and replicated storage systems.
blltprf.xyz
Technical notebook by Dr. Thomas Pani.
Notes, experiments, and talks on executable specifications, formal verification, model checking, fuzzing, model-based testing, software reliability, and AI-assisted verification.
For profile, advisory work, and contact information, see thpani.net.
Writing and talks
Cannot MBT with PBT
Property-based testing can look a lot like model-based testing, until the next valid input depends on values the system under test just returned.
What are executable specifications?
A practical explanation of executable specifications as runnable references for critical software behavior, with a DNS balancer control-plane example.
Formal Verification of the Aztec Governance Protocol
An in-depth report on formally verifying Aztec's governance protocol, including modeling decisions, invariants, verification conditions, and outcomes.
25-Minute Solidity Fuzzer
Recording and repository for a hands-on Protocol Berg workshop: build a functional EVM/Solidity smart-contract fuzzer in Python.
Why Formal Verification Isn't Just Fancy Exhaustive Testing
A technical comparison of formal methods and exhaustive testing, and why the difference matters in practice.
Fuzzlands: Map of the Wider Fuzzing Landscape
A practitioner's map of fuzzing tools, techniques, and how the field has evolved.
Model Checking Accountability in Ethereum
SSF-MC: verifying accountable safety for Ethereum's 3-slot finality consensus protocol with TLA+, Alloy, and SMT.
Small and Modular Runtime Monitors in TLA+ for Soroban Smart Contracts
Solarkraft #2: writing small modular TLA+ runtime monitors for Soroban smart contracts.
Why Smart Contract Bugs Matter and How Runtime Monitoring Saves the Day
Solarkraft #1: smart contract vulnerabilities, the traditional security model, and runtime monitoring for Soroban contracts.
