I'm not really sure what you're saying here -- the parent commenter is talking about closed-world source-level code verification.
My claim is that these techniques help in relatively few areas of software development. In the main, software is built with open-world interactions across a range of devices (network, disk, etc.) where those interactions dominate the net failure modes of the system.
In the latter case, source-level verification is not only of no help, but it's a huge resource misallocation. You end up writing tests that just create the illusion of success; and then the whole thing constantly falls over.
Spend all that time instead in designing tests that do fit into ram (eg., sample your datasets); and instrumentation that does reveal errors (eg., sampling of memory, requests, etc.).
One of my first software jobs was writing a reverse proxy -- one of my co-devs wrote unit tests that simply established the in/out of various functions was "as expected". Pretty useless -- the issue is whether the proxy actually worked.
Likewise most source-level correctness efforts are 'testing theatre'.
Devs are looking for cargo-cult solutions they can copy/paste. No, testing software is an actual area of development -- and you need to develop tests, not cargo-cult