No, Rice's theorem states that there is no
general procedure to take an
arbitrary program and decide nontrivial properties of its behaviour. As software engineers, though, we write
specific programs which have properties which can be decided, perhaps by reasoning
specific to the program. (That's, like, the whole point of software engineering: you can't claim to have solved a problem if you wrote a program such that it's undecidable whether it solved the problem.)
The "several times more effort to verify code" thing: I'm hoping the next few generations of LLMs will be able to do this properly! Imagine if you were writing in a dependently typed language, and you wrote your test as simply a theorem, and used a very competent LLM (perhaps with other program search techniques; who knows) to fill in the proof, which nobody will never read. Seems like a natural end state of the OP: more compute may relax the constraints on writing software whose behaviour is formally verifiable.