|
|
|
|
|
|
by rzmmm
7 days ago
|
|
|
He mentions the seL4 microkernel. The specification is written in Isabelle, and it's relatively complex: PDF https://sel4.systems/Info/Docs/seL4-spec.pdf The bottleneck seems to be that clearly it's critical to be certain about the spec. Maybe not for kernels, but I can see use for cryptographic algorithms, etc? |
|
|