Specifying and simulating two-phase commit in Lean4 | Protocols Made Fun

[giscus[bot]]

Specifying and simulating two-phase commit in Lean4 | Protocols Made Fun

Author: Igor Konnov

https://protocols-made-fun.com/lean/2025/04/25/lean-two-phase.html

[konnov]

You can leave your opinion about the blog post here.

[bugarela]

Very cool! I'm really happy to see an intro to Lean from the TLA+/Quint perspective! I'd be also interested to see what kind of useful proofs we can write for transition systems in Lean - I haven't really followed what people are doing in TLAPS up to this point.

And these simulation times are very impressive! I did consider generating C code from Quint for simulation at some point. This motivates me to take a look at what they are doing under the hood. I didn't know Lean had a simulator/fuzzer!

Great post 😄

[konnov]

Lean by itself does not have a simulator, unless we count PBT in, but, as you see, it is not hard to write a custom one, when needed.

[bugarela]

Right! I didn't realize this spec doesn't have any nested non-determinism, so you are actually handling all the nondet choices in the simulator you wrote. That should be feasible for most real specs though, so it's not unrealistic.

It could be fun to try to generate this from Quint.