Looking back on 10 years of the verified seL4 microkernel: https://microkerneldude.wordpress.com/2019/08/06/10-years-sel4-still-the-best-still-getting-better/
Includes some interesting design notes and comments on avoiding a kernel heap entirely.
miniblog.
Related Posts
Would you rather run a formally verified application on top of a conventional kernel/compiler toolchain, or a conventional application on verified kernel/compiler toolchain? Why?
@cwebber@octodon.social Yep, ever since I read 'Intel x86 considered harmful' I've been amazed by how many CPUs exist inside a modern computer. Any could have bugs.
There have been some verification efforts for RISC-V, and the ISA seems to have a bright future, so I'm hopeful there.
I hope it's economically viable though. I loved the OpenMoko project but it wasn't commercially successful.
I understand that companies wanting strong guarantees do custom, verified, single-purpose hardware (e.g. with Galois).
Prediction markets are a fascinating potential application for cryptocurrencies. The details of who and how a claim is verified are challenging though.
https://info.binance.com/en/research/marketresearch/augur-design-flaws.html
(But it looks like the several political outcomes are already available on UK betting exchanges.)