You don't need to go all the way and specify/prove everything in order to achieve significant assurances of absence of (at least certain classes of) bugs.
See the section "Use SPARK at the right level for you" [0] for an example of how you can approach formal verification.
You can start proving certain things, like that your code is free from run-time errors, which already significantly eliminates a lot of bugs.
Then you can start proving certain properties, like it was done for WPA2, to make sure that at least those properties hold and are bug/error free.
Finally, you can achieve full functional correctness, which gives you a significantly higher assurance that your implementation really does satisfy your functional specification. You can start doing this in parts of the code, and progressively increase all the way to the entire code base if you so wish.
Every added formal verification step gives you higher assurance that your code works as intended.
Sure, you can never prove that your code is 100% bug free (this would require the functional specification itself to be bug free, and AFAIK there is no way to verify this), but I would argue that 99% verification is much better than 0% verification.
See the section "Use SPARK at the right level for you" [0] for an example of how you can approach formal verification.
You can start proving certain things, like that your code is free from run-time errors, which already significantly eliminates a lot of bugs.
Then you can start proving certain properties, like it was done for WPA2, to make sure that at least those properties hold and are bug/error free.
Finally, you can achieve full functional correctness, which gives you a significantly higher assurance that your implementation really does satisfy your functional specification. You can start doing this in parts of the code, and progressively increase all the way to the entire code base if you so wish.
Every added formal verification step gives you higher assurance that your code works as intended.
Sure, you can never prove that your code is 100% bug free (this would require the functional specification itself to be bug free, and AFAIK there is no way to verify this), but I would argue that 99% verification is much better than 0% verification.
[0] https://www.adacore.com/sparkpro