It's amazing how many people still wrongly believe that formal verification guarantees that software is bug-free. The proven properties only hold under certain conditions. In a recent study, researchers from the University of Washington analyzed several verified distributed systems and found a total of 16 bugs in them, some of which could cause the systems to crash or corrupt data. The bottom line is that formally verified software does NOT mean bug-free software and you STILL need to test software. Here's a summary of their findings.
Slashdot Mirror
It's amazing how many people still wrongly believe that formal verification guarantees that software is bug-free. The proven properties only hold under certain conditions. In a recent study, researchers from the University of Washington analyzed several verified distributed systems and found a total of 16 bugs in them, some of which could cause the systems to crash or corrupt data. The bottom line is that formally verified software does NOT mean bug-free software and you STILL need to test software. Here's a summary of their findings.