4 ms·

Does anyone have more information about where sel4 is used in production?

• cmrx64 6y ago
  https://driveghost.com/ https://driveghost.com/ current users aren't very loud about it. RTI is implementing DDS for sel4. productionization is still early days. DARPA is pushing for it. you might look at the speakers, sponsors, and attendees of the sel4 conferences and workshops :)
• 762236 6y ago
  Self driving cars via driveghost.com: "Ghost has assembled a team of leading experts in formal methods, an approach to software development that makes it possible to build complex software systems that can be proven to run without bugs or errors. Unlike existing systems built on error-prone platforms, Ghost will be the first to bring formal methods to the roadways with the world's only formally verified runtime built for your car, delivering you bug-free driving and unparalleled safety behind the wheel."
  • person_of_color 6y ago
    Seems like a dumb approach that only marketing would come up with. The challenge is SDC is AI, not correctness of the kernel that the AI stack runs on. Is an SDC based on a formally verified OS but using logistic regression safe?
    • aidenn0 6y ago
      It's at least safe from someone hacking into it and intentionally (or accidentally) causing harm.
    • moonchild 6y ago
      A verifiably correct kernel is a necessary, but not sufficient condition for a self-driving vehicle to be trustworthy.