Just because two researchers claim their latest OS is bulletproof is not proof their latest OS is bulletproof. I've seen many other such claims in the past fall before a few weeks in the wild. . .
>> I prefer to go with things that can be formally proven: cannot happen is much better than “hasn’t happened yet”.
>
> Just because two researchers claim their latest OS is bulletproof is not proof their latest OS is bulletproof.
Except that’s not the claim they’re making — they’re making the claim that they have a fully type-safe OS.
(This is an important step toward a formally-proven secure OS; as there are MANY security holes which can be covered by type-safety.)
> I’ve seen many other such claims in the past fall before a few weeks in the wild. . .
Again; read the paper.
They’re not just “making claims” they’re running proof engines to prove the claims.
OSes aren’t the only things that are being formally proven — a while ago there was a DNS that is provably free of runtime-exceptions, remote execution, and single-packed DoS attacks. (See http://ironsides.martincarlisle.com/ for papers, source-code, etc.)