It pushes the bugs to things that are easier to test. You write tests for things like "we properly error on a malformed input" and write TLA+ specs for things l

It pushes the bugs to things that are easier to test. You write tests for things like "we properly error on a malformed input" and write TLA+ specs for things like "there are no awful concurrency bugs spanning three servers in two regions."