On 7/24/2026 3:20 AM, John Haxby wrote:
And I don't care if you say you have a kernel with a formal proof -- you'll
still have bugs in somewhere in the application stack.
Or in the hardware its run on - formal proofs didn't defend from Spectre
and Meltdown when we all learned that CPUs did things differently than
our models of them assumed they did, and the proof of an OS is unlikely
to cover all the code running in the firmware of the underlying devices.
--
-Alan Coopersmith- [email protected]
Oracle Solaris Engineering - https://blogs.oracle.com/solaris
