> don't confuse formal verification with security It sure makes auditing that code conforms to an expected design a lot easier, which is most security bugs. Th

> don't confuse formal verification with security It sure makes auditing that code conforms to an expected design a lot easier, which is most security bugs. This is a fantastic design choice for a security focused kernel. I will grant that proving something was implemented as designed does not rule out design flaws so, fair enough.