An interesting quote from the short write-up on their webpage:
With all the purity and strength of mathematical proof it is easy to get carried away. There is a fundamental theoretical limit of formal verification: there will always be some bottom level of assumptions about the physical world left and these assumptions have to be validated by other means. Mathematical proof is proof as long as it talks about formal concepts. It is when assumptions connect to reality where things may still fail.
Albert Einstein is quoted as saying "As far as the laws of mathematics refer to reality, they are not certain; and as far as they are certain, they do not refer to reality."
An important reminder for project managers enamoured of the assurance provided by the numerical test section's relatively easy to come-by answers.
Slashdot discussion of this result (standard posts misunderstanding Goedel's work included of course).