Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Verified seL4 on secure RISC-V processors.
https://news.ycombinator.com/item?id=23464187
Also, my previous comment linking to how SeL4 performed the verification:
https://news.ycombinator.com/item?id=23475748
> seL4 hey used Haskell to create an model which was then their specification to help with the formal verification process [1][2].
> [1] https://dl.acm.org/doi/pdf/10.1145/1159842.1159850
> [2] https://www.sigops.org/s/conferences/sosp/2009/papers/klein-....
There are no comments on this comment yet.
https://news.ycombinator.com/item?id=23464187
Also, my previous comment linking to how SeL4 performed the verification:
https://news.ycombinator.com/item?id=23475748
> seL4 hey used Haskell to create an model which was then their specification to help with the formal verification process [1][2].
> [1] https://dl.acm.org/doi/pdf/10.1145/1159842.1159850
> [2] https://www.sigops.org/s/conferences/sosp/2009/papers/klein-....