3 ms·

Of course, there might be bugs in the specification (the proof the made was that the kernel matches the specification)

• seanwilson 11y ago
  > Of course, there might be bugs in the specification (the proof the made was that the kernel matches the specification) Nothing is perfect, but this approach catches more bugs than any other technique. Also, some specifications are simple to specify e.g. it's not hard to specify that an array index must be within the bounds of the array and if you did get this wrong you'd notice quickly as you'd be unable to prove obvious facts are correct.
  • ktRolster 11y ago
    but this approach catches more bugs than any other technique Have you seen the specification for sel4? It's fairly complex.