Unhackable Is a Marketing Lie. Here's What Formal Verification Actually Proves

The strongest software assurance claim in the industry belongs to seL4, a microkernel with a machine-checked proof down to the binary. Its own documentation publishes the list of things the proof does not cover. That list is the whole story.