iiinova — where your digital self keeps evolving

Igor Konnov | konnov.phd

@k0nn0v.bsky.social

Melting formal methods into blockchain security

Igor Konnov | konnov.phd @k0nn0v.bsky.social · 16/12/2025

A new blog post on: connecting a TLA+ specification to real protocol code using Apalache + Z3, generating tests symbolically and executing them interactively against multiple TFTP implementations. Bootstrapping the test harness with Claude. protocols-made-fun.com/tlaplus/2025...

protocols-made-fun.com

Interactive Symbolic Testing of TFTP with TLA+ and Apalache

Author: Igor Konnov

000

Igor Konnov | konnov.phd @k0nn0v.bsky.social · 16/12/2025

What value is your formal spec if it's totally disconnected from the implementation? Follow the thread... #tlaplus #testing #smt #protocols

100

Igor Konnov | konnov.phd @k0nn0v.bsky.social · 27/04/2025

Sunday long read: Specifying and simulating two-phase commit in Lean4. protocols-made-fun.com/lean/2025/04...

protocols-made-fun.com

Specifying and simulating two-phase commit in Lean4

Author: Igor Konnov

000

Igor Konnov | konnov.phd @k0nn0v.bsky.social · 17/01/2025

</end-of-thread>

000

Igor Konnov | konnov.phd @k0nn0v.bsky.social · 17/01/2025

This work was done by @audithare, Jure Kukovec, @robsaltini, @thanh_hai_tran, and myself. We thank @luca_zanolini and @fradamt for fruitful discussions and @ethereumfndn and @ef_esp for the grant under the 2024 Academic Grants Round!

100

Igor Konnov | konnov.phd @k0nn0v.bsky.social · 17/01/2025

We have introduced several levels of abstractions, to avoid layers of graph problems, hidden inside. We ran Apalache+Z3, Alloy+Kissat, CVC5, for hours and days. It took many iterations, obviously, we found bugs in our specs as well. In the end, accountable safety held through.

100

Igor Konnov | konnov.phd @k0nn0v.bsky.social · 17/01/2025

Accountable safety was hard to think about, also to automatically reason about, as we found. We put our energy there. Our most direct translation from Python to TLA+ was good enough for finding examples, but showing safety for all combinations was too much for the tools.

100

Igor Konnov | konnov.phd @k0nn0v.bsky.social · 17/01/2025

We started with the Python specification of 3SF that was recently designed by @luca_zanolini @fradamt @robsaltini @thanh_hai_tran (see the tweet). x.com/luca_zanoli...

100

Igor Konnov | konnov.phd @k0nn0v.bsky.social · 17/01/2025

Thinking about distributed algorithms like consensus and their properties is hard. Too many combinations to consider, too easy to give up. Faults make it even worse 🤯 Check our recent report [arxiv.org/abs/2501.07958] for #Ethereum on how model checkers and solvers can help us 🧵

arxiv.org

Technical Report: Exploring Automatic Model-Checking of the...

We investigate automated model-checking of the Ethereum specification, focusing on the Accountable Safety property of the 3SF consensus protocol. We select 3SF due to its relevance and the unique...

120

Igor Konnov | konnov.phd @k0nn0v.bsky.social · 14/01/2025

Copilot definitely helps me to quickly write some experimental code in the languages I am not proficient in. It shortens the documentation and google lookups. Sometimes, the produced code is pure garbage, though :)

010