Without getting into details, AFAICT they do not use any typical high-assurance software stacks, such as Ada or Spark or such that might be typical in avionics, like Airbus software. The use off-the-shelf tools like C++ and LLVM.
You don't know what kind of tools they've developed internally and Ada/Spark is far from the end-all be-all of high assurance programming.
High assurance comes from the overall systems design and testing, not the software itself. Afterall, radiation can cause any piece of software, including those written in Ada, to completely skip instructions.
There's obviously a lot of legacy Ada out there, but would you say it's 'typical' for new code being written? I don't have that sense. There's probably more MISRA C/++ code floating around at this point. I have no idea how compliant SX is, but I've heard mentions of Power of 10 rules and JPL standards. For what it's worth, their track record doesn't seem concerning nowadays.
I think commercial avionics is the only place you still find ada. Cars have been c or c++ even for safety critical for many years. Even defense abandoned ada well over a decade ago, and they invented it right? And medical jumped right on the windows ce bandwagon as soon as it popped up... I feel like a good pipelene with lots of static analysis asan, and really good tests is probably the best you can expect out of safety critical stuff these days. The days of provably safe software, and certified compilers are probably gone. And if you told me tesla was using folders with dates in the names for version control, and they preferred to test in production, I wouldn't ne surprised. Horrified, but not surprised.
Not to rain on your parade, but neither do any of the other automotive companies. Ada and SPARK is amazing, but I don't think I've seen it used outside aerospace/defence.
