@meltedcheese@c.im @briankrebs@infosec.exchange With a sufficiently rigorous specification, we definitely can prove code is correct to the spec. It’s difficult, and there can still be security issues in the specification, but it’s well within the means of any serious company. The fact these companies spent umpteen billion dollars without building formally-verified security boundaries for the code they intended to weaponize speaks to their fundamental unseriousness. They’re private companies intending to engage in their very own Sea Spray.