Formal Verification Creates Hacker-Proof Code (2016)

Re:Formal Verification Creates Hacker-Proof Code (2016) by hwayne on Sunday April 26, 2020 @11:55AM (#22988006)

This is correct: the TLA+ model checker (TLC) will check all possible behaviors for the finite model. As the GP said, they were only working with a finite number of workers, but within those constraints it guarantees the spec always satisfies the invariants.

(This is of course assuming that TLC doesn't have any bugs that would cause it to misreport. By contrast something like randomized testing doesn't guarantee the spec satisfies the invariants even if the tester is bug-free.)

[ Parent | on HN ]

Re:Formal Verification Creates Hacker-Proof Code (2016) by sterlind on Sunday April 26, 2020 @05:23PM (#22990380)

exactly. I've proven that in a scenario with a certain number of zones and workers, the invariants and temporal properties cannot be violated.

With more work, I could prove the invariants for any number of workers and zones using TLAPS rather than TLC, though I couldn't prove the temporal properties in this way (since TLAPS doesn't support temporal logic, it can only prove invariants.)

[ Parent | on HN ]