seL4 is the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement.
This project is a mathematically-verified bug-free microkernel system that supports x86 and ARM, and aims to be general-purpose.
Website:
sel4.systems
Whitepaper:
sel4.systems
Genode OS, an OS framework that supports seL4 and other kernels:
genode.org
seL4 is already being used and researched by the military for avionics and helmet displays.
Other urls found in this thread:
qualcomm.com
cavium.com
wiki.sel4.systems
genode.org
rumpkernel.org
hack.org
genode.org
genode.org
genode.org
fixup.fi
pcworld.com
gnu.org
twitter.com
Daily reminder that formal verification only proves the relationship of a model to an implementation and that it is not proof that the model has anything to do with reality / accurately deals with threats.
it doesn't have any proofs for x86 you fucking shill fuck off. you've been posting this all day on g too.
yeah.. ok
x86 is so fucking complicated if they could not possibly model it correctly. The "proof" would be meaningless.
There was actually already a bug in one of the unverified parts that had to be fixed. It's still a good choice if you need it but if you post here you don't.
...
Is it webscale?
wat