Exactly, it's fundamentally impossible. Formal proofs can help with parts of the process, but it can guarantee no bugs in the product. These are the steps of so

Exactly, it's fundamentally impossible. Formal proofs can help with parts of the process, but it can guarantee no bugs in the product. These are the steps of software, and their transitions. It's fundamentally a game of telephone with errors at each step along the way. What actually would solve the customer's problem -> What the customer thinks they want -> What they communicate that they want -> What the requirements collector hears -> What the requirements collector documents -> How the implementor interprets the requirements -> What the implementor designs/plans -> What the implementor implements. Formal proofs can help with the last 3 steps. But again that's assuming the implementor can formalize every requirement they interpreted. And that's impossible as well, there will always be implicit assumptions about the running environment, performance, scale, the behavior of dependent processes/APIs. It helps with a small set of possible problems. If those problems are mission-critical then absolutely tackle them, but there will never be a situation where it can help with the first 5 steps of the problem, or with the implicit items in the 6th step above.