It's almost always done to argue for testing, too. But the point of verification as an engineering tool was never to replace testing, but to focus it. (Just lik

It's almost always done to argue for testing, too. But the point of verification as an engineering tool was never to replace testing, but to focus it. (Just like the point of a mathematical proof is not to offer 100% proof of the truth of a statement, but to reduce its truth to the truth of some other statement---usually "ZF holds".) So you do some formal verification, good. But you still need to: - validate your model; and - validate your assumptions. This would always have to be done, but the fact that GP did not think about it means that, in the case of testing, it's not done. It's just "extensive testing", perhaps with some metric if we're lucky. Never "what are we testing for, and under what circumstances". (Except in places---aerospace, hardware---that welcome formal verification.) Now, why does the above rant matter? Because GP is advocating the use of testing for a security property. Writing that test means you suspect there's something iffy that can happen with speculation. And if you know something iffy can happen, you can figure out what's not iffy and make that your spec for formal verification. You then get a proof that only the good (secure) behaviour takes place under clear assumptions, instead of getting the guarantee that none of the bad behaviours are exercised by your test suite.