NVIDIA: Adoption of SPARK Ushers in a New Era in Security-Critical Software Development

What's Inside

This case study will examine:

  • The challenges companies like NVIDIA face in confronting an increasingly hostile cybersecurity environment while expert software security resources remain scarce

  • Why NVIDIA made the “heretical” decision to abandon C/C++ and adopt SPARK as its coding language of choice for security-critical software and firmware components

  • The advantages of using the SPARK for security- and safety-critical coding applications

  • NVIDIA’s approach to ramping up their use of SPARK for critical component development

  • The benefits NVIDIA has gained through their adoption of SPARK

  • Why many of NVIDIA’s early SPARK skeptics have now become SPARK evangelists

  • NVIDIA’s recommendations for would-be SPARK adopters

  • And more…


NVIDIA Corporation is among the world's most trusted names in graphics processing units, embedded systems, high-performance computing, and artificial intelligence. Their GPUs and other systems are found in millions of products worldwide.


Confront an increasingly hostile threat environment for embedded systems by finding a more measurable solution for verifying system security and safety in their critical software and firmware components.


Replace critical firmware and software components written in C/C++ with new components written in SPARK, the software language designed for embedded systems where predictable and highly reliable operation is essential.

Results and Benefits

NVIDIA is now using SPARK to mathematically guarantee—and demonstrate to customers and regulators—a total absence of runtime errors in its most critical components and of unspecified behaviors in its root-of-trust applications. SPARK thus provides NVIDIA and its customers the highest possible assurance against cyberattacks and critical systems failures.