Comment by nernst

This is interesting work. I'm curious how confident we can be that the TLA+ proof from Diego Ongaro was correctly represented in Verdi/Coq. This still seems like a manual, hard-to-verify process.