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.
Writing and talks
Technical notes from blltprf.xyz.
This archive mirrors the writing index on the homepage.
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.
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.
25-Minute Solidity Fuzzer
Recording and repository for a hands-on Protocol Berg workshop.
Why Formal Verification Isn’t Just Fancy Exhaustive Testing
A technical comparison of formal methods and exhaustive testing.
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.
