> One of those verified building blocks comes with a proof guaranteeing that someone with access inside one partition won’t be able to escalate their privileges

> One of those verified building blocks comes with a proof guaranteeing that someone with access inside one partition won’t be able to escalate their privileges and get inside other partitions. The article is presumably referring to the seL4 formally verified operating system. There's not a single mention of it by name, but it lines up, as they're discussing the unmanned Little Bird, which is one of seL4's success stories. https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597724/ https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597724/ https://www.newscientist.com/article/mg22730392-600-unhackable-kernel-could-keep-all-computers-safe-from-cyberattack-2/ https://www.newscientist.com/article/mg22730392-600-unhackab... https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...