Wow, that's cool. TLA+ is the same formalism that Amazon uses to verify (some of) their cloud services.