[brians]

Yes! But none you want to use on a workstation. Honeywell and Burroughs both produced A1 verified operating systems—presumably there are successors there or at General Dynamics. There are some Russian attempts as well. Nobody else had the engineers, the mathematicians, and the money to build a verified system.

The standards there assume a TCB of about 10 kloc; 5kloc for the OS, 5kloc for each application. Separation is by static allocation—of disk space and memory usage, but also static time-domain multiplexing of CPU cores and IO lanes, with caches flushed on every context switch. They’re ferociously expensive to acquire in the first place, and then you take a huge operational penalty for running multiple applications.

There are very few problems for which this is a helpful solution—maybe not none, but very few when you could just buy several distinct computers, run them airgapped, and go about your business.