Protocols Made Fun

Update (2026-07-28): Add Lean 4 proofs This text is artisanally typed using Das Keyboard, with occasional suggestions by Copilot (most of them ignored anyways).

This text is artisanally typed using Das Keyboard, with occasional suggestions by Copilot (most of them ignored anyways).

Author: Igor Konnov Date: May 26, 2026 This text is artisanally typed using a keyboard, with occasional suggestions by Copilot.

Author: Igor Konnov Date: April 30, 2026 Recently, I wrote a blog post on random walks that compared the state coverage of random walks for increasingly larger sets of experiments: 100 thousands, 1 million, 10 million, and even 100 million episodes.

Author: Igor Konnov Date: March 23, 2026 This is an anecdote about another useful application of Codex and Claude Code in the middle of a testing project.

Author: Igor Konnov Date: March 09, 2026 Punchline: Testing distributed protocols with random simulation and stateful property-based testing (PBT) is not enough!

Author: Igor Konnov Date: February 12, 2026 tl;dr: AI coding tools now reduce development costs, but they also accelerate the creation of software that appears high-quality while hiding serious correctness and reliability risks.

Author: Igor Konnov Date: December 22, 2025 I present a simple example that illustrates how property-based testing (PBT) and model checking can help us catch unexpected behaviors of LLMs when they are used to generate code.

Author: Igor Konnov Date: December 15, 2025 Note: I mostly stopped using LLMs for proof-reading my texts, so you know it is not all generated.

Authors: Thomas Pani, Igor Konnov Date: December 9, 2025 1.