In thinking about formal verification techniques, you also need to have test coverage. But as that article shows, you can easily say you have "100% test coverage", but every test doesn't have any assertions. That is the extreme. But I'm wondering if there is ever a situation where you can say that you have 100% test coverage somehow. Similar to how a model checker can check every possible path and state in your application, wondering if a testing tool can be said to cover the same level of thoroughness as a model checker. Basically wondering if there is a way to be thorough enough with your tests to know that you have 100% percent coverage, without explicitly writing every possible combination of things.
There are strategies that can produce deep code coverage metrics. Mutation testing is one example. Roughly speaking, mutation testing ensures that any logical change to the program results in a failed test by actually running the tests against every logical permutation of a program. If a logical change doesn't produce a failing test, it represents a meaningful test coverage gap.
My disclaimer: I've never actually performed mutation testing. I can't speak to how feasible or valuable it really is. But, in theory, it sounds pretty darn slick. In practice, however, most businesses can survive (and thrive) on hiring good developers who are engaged, interested, and insist on following good development practices.
100% test coverage is possible, and despite 100% coverage, your program may still have errors. See shortcomings of test coverage at "Does path coverage guarantee finding all bugs?"
Similar to how a model checker can check every possible path and state in your application, wondering if a testing tool can be said to cover the same level of thoroughness as a model checker.
The basic idea is that test coverage will only measure if you've been through a particular statement / path etc or not, at-least in one state (in contrast to model-checking which provides guarantees for all possible states)
So the answer is no, unless you have test cases for every possible input-output pair (exponentially large number of test cases in the general case)
Depends my complexity of what you're testing. When my application only prints Hello World I only have to run an assert to check if the printed result is "Hello World". When real time performance issues, hardware limitations are involved, or there are very complex interactions I imagine some test cases that no one could expect can occur.