Re:The Case Against Formal Verification, 50 Years Later
by demibabs on Sunday August 16, 2026 @06:40PM
(#49324494)
Iām a bit confused as to what makes formal verification different from extensive testing.
[ Parent
| on HN ]
Re:The Case Against Formal Verification, 50 Years Later
by gr_norm on Sunday August 16, 2026 @06:52PM
(#49324584)
To a first approximation, formal verification can guarantee some property holds for every possible run of the program, rather than just the tested ones. It's a lot more powerful than it sounds, because this unlocks the ability to talk about qualities of programs that cannot be tested (effectively or at all). Hyperproperties like confidentiality, integrity, and availability tend to be quite difficult to test, for instance.
Re:The Case Against Formal Verification, 50 Years Later
by japgolly on Monday August 17, 2026 @12:36AM
(#49326591)
1) With formal verification you can prove properties about your system. With extensive testing you can also do the same but you need to take care and make sure you cover all possible cases.
2) With formal verification you can easily test things that are normally hard to cover by traditional testing. For example, if you want to test if that a postgres randomly goes offline, you don't lose any data, it's pretty hard to cover with extensive testing, whereas with formal verification you just say "postgres exists, it has state and can be online/offline, it can go online/offline at anytime" and you're covered.