Re:Cloudflare outage should not have happened
by zbentley on Wednesday November 26, 2025 @11:57PM
(#46065824)
Formal verification is well and good, but that is not what unsoundness means.
If a proof trivially demonstrated that a given program’s behavior was indeed “proceed if a condition is satisfied, crash otherwise”, then what? Or do we not trust the verifier with branching code all of a sudden?
If a proof trivially demonstrated that a given program’s behavior was indeed “proceed if a condition is satisfied, crash otherwise”, then what? Or do we not trust the verifier with branching code all of a sudden?