specification
formal verification
protocol audits
TLA+/Lean/Quint
model checking
proofs
fuzzing
Igor Konnov and friends writing about protocol specification, testing, and verification
-
Extracting formal specifications from Apache ZooKeeper with AI tools and Apalache
-
TLC breadth-first search vs random simulation
-
Specification debugging as code generation
-
All you need is a simulator? Nope
-
AI-generated shovels or second-order slop?
-
Property-based testing, adversarial developers, and LLMs
-
Interactive Symbolic Testing of TFTP with TLA+ and Apalache
-
Formal Verification of the Aztec Governance Protocol
-
Small scope hypothesis revisited
-
Running TLC with non-standard modules
-
Proving completeness of an eventually perfect failure detector in Lean4
-
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)
-
A New Hope – Why Smart Contract Bugs Matter and How Runtime Monitoring Saves the Day (Solarkraft #1)
-
Guardians of the Blockchain: Small and Modular Runtime Monitors in TLA+ for Soroban Smart Contracts (Solarkraft #2)
-
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