How NVIDIA Boosted Software Safety by Switching from C to SPARK
NVIDIA’s security team adopted the formally verified SPARK language, replacing C in safety‑critical components, and after a successful proof‑of‑concept demonstrated improved security, verification efficiency, and unchanged performance, leading to widespread internal adoption across many products.
AdaCore, the company behind the Ada and SPARK programming languages, published a case study about NVIDIA.
NVIDIA’s products run many formally verified SPARK code components, and its security team is exploring replacing C with SPARK for safety‑critical applications.
SPARK is a programming language and a set of verification tools designed for high‑assurance software development. It is a subset of Ada that removes non‑verifiable features and extends contracts and aspects to support modular formal verification. SPARK is typically used in systems requiring predictable and highly reliable operation, helping develop applications with high safety or business integrity requirements.
In 2018, NVIDIA conducted a proof‑of‑concept (POC) converting two low‑level, safety‑sensitive applications from C to SPARK within three months. After evaluating the return on investment, the team concluded that the new technology—training, experiments, and tools—improved both application security and verification efficiency, and the two applications achieved a significant improvement in safety robustness.
Following the successful POC, SPARK adoption spread rapidly inside NVIDIA. More than 50 professionally trained developers now use SPARK to implement many components, and numerous NVIDIA products now ship with SPARK components.
SPARK also offers a notable feature: the ability to specify program requirements directly in the code and use its toolset to ensure the implementation matches those requirements. NVIDIA leverages SPARK for its most critical components to guarantee the absence of runtime errors and compliance with trusted‑root application specifications.
The full case study also discusses interesting topics such as performance, noting that “no performance difference” was observed when comparing SPARK to C.
Related link: https://www.adacore.com/uploads/techPapers/222559-adacore-nvidia-case-study-v5.pdf
Open Source Linux
Focused on sharing Linux/Unix content, covering fundamentals, system development, network programming, automation/operations, cloud computing, and related professional knowledge.
How this landed with the community
Was this worth your time?
0 Comments
Thoughtful readers leave field notes, pushback, and hard-won operational detail here.