Every time it comes up, I am impressed by seL4. From the incredibly small size of the code to the fact that it's been proven correct, it's just a testament to

Every time it comes up, I am impressed by seL4. From the incredibly small size of the code to the fact that it's been proven correct, it's just a testament to the fact that correct code, in the formal sense, can be written. I'm happy to hear that advances in this area continue to be made.