Can you speak more on why ‘making them actually consistent in production is a completely different story’?
Curious because I’ve been learning TLA+ recently and interested to more know about cases where an algorithm has been proven but actual an implementation of it fails.