Resources for the Ada programming language

Ada is a statically typed, high-level programming language designed for reliability, efficiency, and safety, particularly in systems where safety-critical applications are essential. Developed in the 1980s for the U.S. Department of Defense, Ada emphasizes strong typing, modularity, and concurrency, making it well-suited for embedded systems, real-time applications, and aerospace software.

Known for its rigorous compile-time checking and runtime support for tasks, real-time scheduling, and exception handling, Ada is a preferred choice for mission-critical systems where correctness and fault tolerance are paramount. Its features also support concurrent programming, making it ideal for multi-threaded and distributed systems.

While it may not be as widely used in mainstream development, Ada continues to be relied upon in defense, aerospace, and other industries where high levels of assurance and performance are required.

NVIDIA: Formal Verification for Safety-Critical Components

NVIDIA needed to certify GPU firmware components for automotive applications under ISO 26262 ASIL D, the highest automotive safety integrity level. Traditional C/C++ development couldn't provide the mathematical guarantees required by safety certification, and extensive testing requirements made certification expensive and time-consuming. They needed a way to formally prove that small, safety-critical software units were free from runtime errors and conformed to specifications.

After a three-month proof-of-concept in late 2018 with help from AdaCore, NVIDIA adopted SPARK (an Ada subset designed for formal verification) for these targeted safety kernels. SPARK allows mathematical proof of correctness, potentially replacing much of the testing burden required by ISO 26262. Importantly, NVIDIA standardized on the completely free, open-source toolchain (FSF GNAT compiler and GNATprove Community verification tools) rather than commercial vendor tools. They kept most of their firmware in C/C++, using SPARK only for isolated safety-critical components where certification value justified the investment.

By 2022, NVIDIA had trained 50+ engineers and shipped multiple certified components. More significantly, they open-sourced their entire ISO 26262-compliant SPARK development process, including methodology, coding standards, proof strategies, and training materials. This means other organizations can now replicate NVIDIA's certification approach using entirely free tools and NVIDIA's published playbook, without requiring vendor support contracts. AdaCore helped bootstrap the initial adoption, but NVIDIA's published work demonstrates that SPARK is viable as a vendor-independent solution for safety-critical development.