All things about protocol specification, testing, and verification. Creative Commons Attribution 4.0 International License.
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). The figures are generated with ChatGPT 5.5. If you read my previous blog post , you know that I was impressed by the ability of the frontier AI tools to write complete proofs of safety for the Ben-Or's consensus using Lean 4 and TLAPS. Not…
This text is artisanally typed using Das Keyboard, with occasional suggestions by Copilot (most of them ignored anyways). The figures are generated with ChatGPT 5.5. In November 2024, I wrote a blog post about checking safety of the Ben-Or consensus protocol using TLA + and Apalache . The last section of the blog post introduces an inductive invariant IndInv that is used to prove protocol safety…
Author: Igor Konnov Date: May 26, 2026 This text is artisanally typed using a keyboard, with occasional suggestions by Copilot. The figures are generated with ChatGPT 5.5. The plots are produced by AI-generated scripts from the experimental data. By AI tools, I refer to Codex GPT 5.4/5.5 and Claude Code Sonnet/Opus 4.6/4.7. Recently, I gave a talk on " Interactive symbolic testing with TLA + ,…
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. There, I used custom-built simulators in Rust to randomly walk through the state spaces of several TLA + benchmarks: two-phase commit,…
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. It is another example of using LLMs to make distributed systems easier to test and debug, instead of generating piles of slop. Context I am currently developing a test harness for an implementation of distributed consensus, cannot disclose the…
Author: Igor Konnov Date: March 09, 2026 Punchline: Testing distributed protocols with random simulation and stateful property-based testing (PBT) is not enough! Yes, running a simulator for days is better than doing manual testing or just running unit tests. But you will miss states, which may expose bugs . Even on very small systems. I have been saying exactly this to many software engineers.…
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. When both code and tests are autogenerated, traditional quality checks lose their signaling value, increasing the likelihood of costly failures, outages, and liability…
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. The example is inspired by the talk on property-based testing by Scott Wlaschin . If you are looking for a light example that stresses the importance of writing good properties…
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. Enjoy my typos and weird grammar! Abstract. As promised in the blog post on small-scope hypothesis , I am continuing with the main body of the talk that I presented at the internal Nvidia FM Week 2025. This blog post is rather long. If you do not want to…
Authors: Thomas Pani , Igor Konnov Date: December 9, 2025 1. Introduction In August 2025, Aztec Labs engaged Thomas Pani and Igor Konnov to formally specify and verify the new Aztec Governance Protocol – the core on-chain system that governs Aztec Network . Over the course of five weeks, we reviewed every line of code in scope and developed a precise formal specification, verified automatically…