They use the SPARK subset of Ada to develop the most critical parts of their DriveOS. This contributed to their success of getting DriveOS certified at the highest automotive safety standard, ASIL-D.
This is a great article that highlights various virtues of developing with Ada and SPARK that contributed to NVIDIA's recent achievement of certifying their DriveOS automotive operating system to the _highest_ automotive level of safety, ASIL-D. The first ever!
Here is a paragraph from the article:
“Adopting a new programming language involves deploying a new environment, training teams to a new formalism, adapting programming patterns and many other issues. However, from a process standpoint, programming languages are vastly interchangeable, but Ada and SPARK is a different story.”
https://www.eenewseurope.com/en/nvidia-drives-ada-and-spark-...