Verifying behaviour of an arbitrary program is uncomputable. However that doesnt mean you can't have proofs of behaviour of specific programs you create.
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.
There's lots of things to show for the research!
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.
I fear it'll just move the problem one layer up. Sure, you've now proven that the code matches the specification - but how do you ensure the specification is watertight?
The specification doesn't have to be.
But yeah, writing specs is usually harder than reviewing the code 4 times :)
It kinda does.
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.
Moving the problem one layer up is the desired outcome because it makes exploitation much more difficult. Your attack surface becomes much smaller.