Yes, a formal proof shows that a system does not have a specified class of bugs, subject to specific assumptions. This is very valuable, but it is better to thi

Yes, a formal proof shows that a system does not have a specified class of bugs, subject to specific assumptions. This is very valuable, but it is better to think of it as another (very powerful) bug finding technology than a complete assurance that nothing can go wrong.