AdaCore and NVIDIA Publish an ISO 26262 Reference Process for Ada and SPARK
AdaCore says NVIDIA used Ada and SPARK for some of the highest-integrity components in its DRIVE OS stack and is now publishing the reference process so other automotive teams can reuse it. The HN thread quickly reframed the announcement as a question of proof-oriented tooling versus the industry's entrenched C++ base.
What was actually announced
The June 2025 announcement is more interesting than a language-war headline suggests. AdaCore says NVIDIA selected Ada and SPARK for some of the most critical software in DRIVE OS, the software stack used to develop and deploy autonomous-vehicle applications on DRIVE AGX hardware. The notable part is not only the language choice. It is the claim that the development process built around those languages is now being published as an off-the-shelf reference process for ISO 26262 work.
That matters because safety tooling only becomes reusable industry infrastructure once the surrounding process is explicit: how evidence is produced, how verification fits the lifecycle, and how language-level guarantees are turned into something certification teams can actually review.
Why this is relevant beyond Ada
For SYLEN readers, the interesting signal is that a major automotive software stack is treating proof-oriented development as process infrastructure rather than as an academic sidecar. SPARK's value proposition has always been that language restrictions and formal verification can be aligned with high-integrity software needs. This announcement says that alignment is being operationalized in a real automotive setting instead of left as a one-off internal practice.
That is the part worth watching even if your stack is not Ada. It speaks to a broader question facing safety-critical software teams: how much assurance can be moved upstream into the language, tooling, and reference process before test and review become the only practical line of defense?
What Hacker News focused on
The HN discussion immediately split in two directions. One camp treated SPARK's formal verification story as the obvious reason the announcement matters. The other defaulted to the historical question of why Ada never displaced C++ despite decades of safety-critical use. The thread also surfaced a pragmatic concern: language features are not enough by themselves if the surrounding tooling and hiring market remain thinner than the incumbent ecosystem.
That is a healthy framing. The real significance here is not that Ada suddenly won the market. It is that certification-oriented process reuse is being packaged in a way that other teams can inspect and potentially adopt.
Read the original article at adacore.com.