I know you're being tongue-in-cheek... but this is actually something we care about a lot! There's a technique in formal specification called "Refinement", wher

I know you're being tongue-in-cheek... but this is actually something we care about a lot! There's a technique in formal specification called "Refinement", where you show a detailed spec successfully implements a more abstract one. On the tooling side, Informal Systems has been doing some good work on static-typechecking TLA+ specifications: https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html https://apalache.informal.systems/docs/tutorials/snowcat-tut... (Disclosure, I've done consulting work for IS.)