The Muen Seperation Kernel (muen.sk) is a secure hypervisor written in SPARK Ada.
Ada was designed for low-level programming. It makes sense it does operating systems fairly easily. Parts of them will break its safety features. They can be validated with external tools, though.
Another trick, used in House with H layer, is to wrap the lowest-level parts which you might do in assembly. Build the GC or whatever, too. Then, everything else is in the higher-level language. These data, the lowest-level portions can be specified, verified, and implemented.
I was slightly more getting at it being not a natural fit for a Unix-like OS but I accept your point.
AFAIK, sadly, Intel BiiN is lost to history now. A Register reader wrote in to me to tell me that he was one of the developers.
What I really wanted from a developer was the i960. Specifically, the version with the object protections. That might be worth buying today for secure, embedded work. If I found the right person, I'd ask them to open-source, or at least dual-license, the i960. For embedded systems, leave it as a RISC-V alternative or port it to RISC-V.