3 ms·

Good luck formally proving Linux.

• layer8 3y ago
  The goal is to prove that the source code matches the machine code, not to prove that the code implements some intended higher-level semantics. This has nothing to do with formally proving the correctness of the Linux kernel.