Hundred percent. All about trade-offs.

Although proof techniques such as proof repair have come a long way, it’s still impractical for a lot of scenarios.

TLA+ is great for systems design and such. Quick check style tests are awesome and a very low bar to clear from unit tests.