Prototyping memory safety in your automotive stack — in weeks, not years

Memory safety has moved from an engineering topic to a boardroom topic. Regulators, security agencies, and OEM customers are increasingly asking the same question: what is your plan for eliminating this class of defects: buffer overflows, use-after-free, out-of-bounds access? These design flaws would cause software written in languages like C or C++ to crash. For software-defined vehicles, where firmware defects become recalls and security advisories, "we test carefully" is no longer a satisfying answer; you can never test for the absence of errors.

Static Memory Safety

Where memory safety is concerned, there are two popular memory-safe languages that should be top of your list right now. Rust and Ada SPARK. Rust is a popular systems-level language that is making headlines, partly because it is included in parts of the Linux kernel and adopted by Google. Ada SPARK has evolved from its aerospace and defense roots and is gaining popularity in the automotive industry.

The languages approach memory safety differently. Rust has some static checks, including its famous borrow checker, but some of its memory safety checks are performed at runtime. SPARK uses formal methods to statically prove the absence of runtime errors, delivering proof of the absence of undefined behavior across all possible execution paths, statically at compile time.

More information about that difference is available in our blog article.

Let’s assume that you wanted to evaluate Ada SPARK for your next automotive project, all the way from high-level business logic to low-level embedded device access. Where do you get started?

The evaluation trap

Adopting a memory-safe language for high-integrity components requires some planning. Mostly: Where do you get started? You have your existing code-base, say in C++. How can you isolate a particular component from that code base? How do you get it translated into SPARK, and how do you put the pieces back together such that you can actually execute everything together on your test bench?

Optionally, you could build a new component in SPARK and then combine it with other components.

In both cases, you will need some amount of scaffolding, glue code that binds the two languages together. Which means you need experts who understand both sides of the coin and can help you craft this binding code. Which, of course, slows everything down, costs time and money, and as people evaluate the investment, the mood changes and the project is abandoned.

So the question "would memory safety work for our firmware?" goes unanswered, and the C++ stays.

Accelerating your prototype

Two recent developments, together, collapse that evaluation cost and seriously question what is possible:

Translation is no longer the bottleneck. Modern LLMs are effective at converting existing C++ into Ada as a starting point. On its own, that would be a risky claim; no one should trust machine-translated code in a vehicle. But that is precisely where SPARK differs from other memory-safe languages: its toolchain statically proves properties such as the absence of runtime errors. The proof tools don't care whether a human or an LLM wrote the code; they verify it either way. LLM translation provides speed; SPARK's verification provides the trust that raw LLM output lacks.

The binding code is no longer hand-built. GNATpolyglot, a new capability of GNAT Pro by AdaCore, automatically generates the binding layer between Ada SPARK components and the C++, Java, or Rust code that calls them. No hand-written glue, no dual-language runtime experts, and when the component's interface changes during experimentation, the bindings are simply regenerated. For a prototype, where the design changes weekly, this matters more than anywhere else.

What a prototype looks like

Pick one component where a memory-safety defect would hurt most. Great choices include a hardware access layer, a module that parses data from outside the vehicle, or encryption/decryption logic. Then:

Use an LLM-assisted workflow to translate the existing C++ into SPARK as a first draft.

Ask the LLM to lift the SPARK code to SPARK Silver using publicly available skills. This enhances the code to the point where you have proof that there are no runtime errors. More information on that process is in our practical playbook.

Run SPARK's proof tools against it. Failed proofs are not setbacks — they are the tool showing you exactly where the translated (or original) code had unproven assumptions.

Generate the C++ bindings with GNATpolyglot and drop the component back into your existing system behind an ordinary-looking API.

The rest of your stack doesn't change. Your teams keep working in the languages they know. And at the end, you have something no slide deck provides: a working component in your real system, with a static proof behind it, and a grounded answer to "what would broader adoption actually cost?"

Why now, and what to expect

The strategic point is timing. Memory-safety expectations from regulators and customers are tightening on a schedule you don't control. Organizations that have already run a concrete evaluation will set their own migration pace; those that haven't will be pushed onto someone else's. Empirical evidence says that code in SPARK has up to 70% less defects than C++ code. This is an investment that will result in a real competitive advantage.

GNATpolyglot is available as a public beta in GNAT Pro 26.2. Beta means exactly that: it is the right tool for evaluation and prototyping, not yet for the production program, which is also the honest sequencing. Prototype now, on real code, at low cost; then make the production decision with evidence instead of estimates.

A scoped prototype for a single component is a low-risk way to gather that evidence.

The compiler and prover toolchain is available in open source through a package manager. LLM's skills are publicly available, and there are blog posts that describe the translation process to SPARK code. You can contact AdaCore to arrange a demonstration of GNATpolyglot and beta access.