Formal specification only works once the system are in a relatively final shape.

No body wants to pay that price when they are struggling with product market fit.

No, formal specification helps from the get-go. You can iterate more reliably, thus faster. The successful development of mathematical theories depends on having rigorous definitions and proofs all the way from the start so that people can communicate effectively, point out caveats unambiguously, and modify the theory robustly. Without formal specs/proofs, refactoring will become too hard. It's actually a lot easier to capture the behavior of a program formally than by tests. Programmers need to gain some experience in math to see this. Listen to Hoare and Dijkstra, and start "thinking".

formal > typed > untyped > unsound > vibed