3 ms·
A lot of the seL4 work was actually funded by several nations' taxpayers, and developed by the late Trustworthy Systems group at Data61 (formerly NICTA). Sadly,
by endgame 3y ago
A lot of the seL4 work was actually funded by several nations' taxpayers, and developed by the late Trustworthy Systems group at Data61 (formerly NICTA). Sadly, they were disbanded a few years back and had to rush to set up a standalone seL4 Foundation: https://microkerneldude.org/2020/04/07/the-sel4-foundation-what-and-why/ https://microkerneldude.org/2020/04/07/the-sel4-foundation-w...
> seL4 is the result of big investments. Firstly by the Australian tax payers, who (through NICTA) funded its creation, and (through NICTA and then CSIRO’s Data61) continued supporting it. Over the past 6 years, US taxpayers (mostly through DARPA, but also other parts of the DoD as well as DHS) invested a lot in completing and extending the verification story, as well as deploying on real-world systems. And most recently, HENSOLDT Cyber funded verification of the RISC-V port of the kernel.
- astrange 3y agoAustralia seems to be quite good at software research, also producing Mercury which seems like a very underrated language, but somehow has zero products to show for it except Jira.