3 ms·

seL4 comes to mind. https://sel4.systems/ https://sel4.systems/

• WhitneyLand 9y ago
  Is there evidence that it’s more reliable compared to equally complex systems? Or that it’s reliability would have been impractical or more expensive using traditional methods?
  • cmrx64 9y ago
    Yes. https://microkerneldude.wordpress.com/2016/06/16/verified-software-can-and-will-be-cheaper-than-buggy-stuff/ https://microkerneldude.wordpress.com/2016/06/16/verified-so...
    • WhitneyLand 9y ago
      I didn’t hold out much hope of a surgical response (because it’s not the most common thing being done in projects) but that looks like a great link exactly on point. It may sound cynical but as I mentioned anecdotally is does really feel like the AI winter, where simultaneously people felt there was incredible promise while hearing a steady stream of discouraging progress reports. I look forward to reading their paper, maybe there are a lot more bright spots than can be easily seen from the outside.
      • CalChris 9y ago
        I think that formal verification is going to be size limited. seL4 is a microkernel which means small, about 9000 LOC. I don't think xen at 150,000 is within the abilities of verification. So it's promising for small stuff.