Post #1546587

@regehr you state that someone takes formally verified code and finds real problems. However, the blog post states that the problems were found in the *non-verified* code: the parser and the Lean runtime. I quote from the blog post: "The positive result here is actually the remarkable one. Across 105 million executions, the application code (that is, excluding the runtime) had zero heap buffer overflows, zero use-after-free, zero stack buffer overflows, zero undefined behaviour (UBSan clean), and zero out-of-bounds array reads in the Lean-generated C code." Arguably, the denial-of-service was a problem in the verified code, but: "[t]he denial-of-service was a missing specification". Which, as I posted elsewhere, is a validation problem and not a verification problem.