This is a good reminder that every digital circuit is really a fancy analog circuit. Your program may be perfectly correct, but when it runs on faulty hardware, you are hosed no matter how many times you’ve formally proven it.