I found this incredibly interesting. I need to play with CBMC [1] sometime. I've always been fascinated by the idea of perfect programs, because so much of my t

I found this incredibly interesting. I need to play with CBMC [1] sometime. I've always been fascinated by the idea of perfect programs, because so much of my time is spent tracking down bugs. And because so much of my PII and finances depend on software that is decidedly not perfect. I would like to know more about how this works: > The formal verification tool effectively runs this function with all possible seed values and checks if the assert() is violated in any of the cases. But it uses a more much efficient method to accomplish this than running the function 2^32 (approximately 4 billion) times. Or are the "prove_" functions some sort of DSL that don't actually get executed as ordinary C code? http://www.cprover.org/cbmc/ http://www.cprover.org/cbmc/