3 ms·

Yes. https://microkerneldude.wordpress.com/2016/06/16/verified-software-can-and-will-be-cheaper-than-buggy-stuff/ https://microkerneldude.wordpress.com/2016/06/

• 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.