You don't need to prove everything against a complete spec, you can prove that things have particular properties you care about, from higher level behaviors like user data can only be accessed by the user down to there are no out of bounds array accesses.
You could prove some complex data-structure to be a correct implementation of some logical data-structure and then prove that your service won't deadlock.
There are a ton of interesting, impactful properties to prove that aren't "create a complete specification and prove the implementation refines it", and even that usage I think is more impactful for removing bugs and vulnerabilities than you're giving it credit for - even something as simple as sorting, Java had a bug in their Timsort implementation for a decade which was discovered when trying to verify it with formal methods: http://envisage-project.eu/wp-content/uploads/2015/02/sortin... ). Note too that if you compiled the simplest/easiest-to-understand spec for something like sorting you'd get something like bubble sort, not Timsort, though you are much more likely to want the latter.
You could prove some complex data-structure to be a correct implementation of some logical data-structure and then prove that your service won't deadlock.
There are a ton of interesting, impactful properties to prove that aren't "create a complete specification and prove the implementation refines it", and even that usage I think is more impactful for removing bugs and vulnerabilities than you're giving it credit for - even something as simple as sorting, Java had a bug in their Timsort implementation for a decade which was discovered when trying to verify it with formal methods: http://envisage-project.eu/wp-content/uploads/2015/02/sortin... ). Note too that if you compiled the simplest/easiest-to-understand spec for something like sorting you'd get something like bubble sort, not Timsort, though you are much more likely to want the latter.