> humans refuse to spend effort on writing more formal specifications.

Code is formal specifications. It's just that programming language semantics has no domain related value of correctness. So you overflow an unsigned integer variable and got a lesser number which does violate addition rules. Or increase account A without decreasing account B, which violates accounting rules (and all kind of closed systems).

So it's up to the programmer to encode all of those rules. While we do have some tooling like type checking and memory safety, they are nowhere near enough. And encoding such thing in a language like Lean or TLA is brittle in terms of maintenance (which you do need to do as the real world evolves).