specification
simulation
fuzzing
protocol audits
TLA+/Quint
model checking
verification
proofs
Igor Konnov and friends writing about protocol specification, testing, and verification
-
Proving consistency of two-phase commit in Lean4
-
Specifying and simulating two-phase commit in Lean4
-
The value of model checking in distributed protocols design
-
Model checking safety of Ben-Or's Byzantine consensus with Apalache
-
Why I use TLA+ and not(TLA+): Episode 1
-
Specification and Model-checking of the ZKsync Governance Protocol
-
Specification and model checking of BFT consensus by Matter Labs
-
The Rise of Model Checker: Verifying Blockchain Monitors In and Near Realtime (Solarkraft #5)
-
The Force Awakens: Hybrid Blockchain Runtime Monitors (Solarkraft #4)
-
How to Run Solarkraft (Solarkraft #3)
-
Guardians of the Blockchain: Small and Modular Runtime Monitors in TLA+ for Soroban Smart Contracts (Solarkraft #2)
-
A New Hope – Why Smart Contract Bugs Matter and How Runtime Monitoring Saves the Day (Solarkraft #1)
-
Is it a high: What are your protocol properties?
-
TLA+ cheatsheet in Markdown
-
You should not care about memory in protocol specifications
-
Thinking about a random number generator: Part 3
-
Thinking about a random number generator: Part 2
-
Thinking about a random number generator: Part 1