> Article doesn't say what parts of Nvidia's stack use SPARK.
Their linked case study lists three examples and one category, https://www.adacore.com/uploads/techPapers/222559-adacore-nv...
- image authentication and integrity checks for the overall GPU firmware image
- BootROM and secure monitor firmware
- formally verified components of an isolation kernel for an embedded operating system
- In general, their targets tend to be smaller code bases that would benefit the most from SPARK’s strong typing, absence of runtime errors, and in some cases, rigorous formal verification of functional properties
> NVRISCV is NVIDIA’s implementation of the RISC-V ISA and Peregrine subsystem includes NVRISCV and multiple peripherals. They show how fine-grain access controls, formally verified for correctness, allow following the principle of least privilege for each partition. NVRISCV provides secure boot that starts with an immutable HW, the chain of trust extends to the Secure Monitor in SW, where partition policies are set up and isolation enforced using HW controls.. Boot and Secure Monitor software is implemented in SPARK.