seL4 is the world's first (and only?) operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. In 34 days it is going open source:
Now if only we could get a provably-correct implementation of the Amoeba operating system kernel on top of this, it'd be the perfect base for a boxed AI software stack.
For more on seL4, see my interview with Gerwin Klein.
When did you start talking to formal verification researchers?
Because, you know, I totally have not wanted to do a PhD under any of these guys, or anything like that...