Verifying correctness of an implementation is P NP, not serious CS research.
The issue is how to design a language that restricts programmers in a way you can prove everything you care for on their programs, and still don't make life of programmers unbearably difficult, because the language allows them nothing.
Personally i have some doubts, a lot of research has gone into the idea without much to show for it, but its a very reasonable research area.
But yeah, writing specs is usually harder than reviewing the code 4 times :)
See WPA2 KRACK, you could've had a formally verified WPA2 implementation and it still would've been exploitable because the flaw was the specification itself.
Part of what the research shows is that correctness-by-proof has a cost in developer effort.
If there really is a vulnerability-apocalypse due to AI, and it's not just a different flavour of AI hype, the cost of having insecure software will rise to the point that the cost of dealing with insecure or incorrect code at time of creation becomes less than the cost of ignoring it until it blows up.
I doubt it'll rise so much that we'll want to face the cost of behaviour proofs for much code at all, but it's quite possible it'll rise enough that we want to do things like prove that indices are in bounds, at compile time, so vector accesses can skip checks without compromising safety.