iiinova — where your digital self keeps evolving

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

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