“A Polynomial Testing Principle” https://personal.cis.strath.ac.uk/conor.mcbride/PolyTest.pdf … gives a machine-checked proof that, under suitably controlled circumstances, in a small but familiar domain, testing can reveal the absence of bugs.
You don't need solve the termination problem, since your observations can consist in output options after N steps, which is enough to eventually rule out any and all programs leading to a discrepancy in observation.
Read my blog!