[bugarela]

Super cool! You might also like Quint if you give it a try: https://quint-lang.org/

This looks like a great example, I'll try to find some time to write a version of it in Quint. I have mentioned DB migration as an example of two phase commit usage before, but never as a standalone spec like this. It's definitely the kind of problem that made me anxious in the past, which means it's a good fit for formal verification :)