> 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 behaviou

> 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. An important point, and something people often get wrong when they mistakenly believe that they understand the basics of formal methods. Here's an old quote about Sel4: > The C code of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more. The and nothing more part is vital. Not only are there no unexpected additional features, there are also no unexpected additional vulnerabilities. More precisely, if there are any vulnerabilities, they must either be in the spec, or be side-channel issues. Formal methods aren't very helpful against side-channel issues.