Comment by whattheheckheck

Throw in some tla+, eventb, p and modp for formal guarantees