I’m interested. Do you have a link or can you elaborate?

Looks like they're using the SPARK subset of Ada:

"NVIDIA began implementing SPARK in its security strategy in 2019 on select pieces of firmware. They began training additional personnel in SPARK and eventually developed an in-house training program.

Several NVIDIA teams are now using SPARK for a wide range of applications that include image authentication and integrity checks for the overall GPU firmware image, BootROM and secure monitor firmware, and formally verified components of an isolation kernel for an embedded operating system, to name just a few."[0]

https://www.adacore.com/nvidia

[0] https://www.wevolver.com/article/nvidia-adoption-of-spark-us...

	▲	cpeterso 2 days ago \| parent [-]
		Here’s a related talk: “NVIDIA - Securing the Future of Safety and Security of Embedded Software” https://youtu.be/2YoPoNx3L5E > NVIDIA is working with AdaCore to implement Ada and SPARK programming languages into certain firmware elements to reduce this potential error. In this webinar you will learn how the combination of NVIDIA hardware with Ada and SPARK delivers robustness and security, improving efficiency and safety in the development pipeline.