For decades, automotive embedded systems have been built in C and C++. These languages are powerful and well understood, but they are also unsafe by design. Buffer overruns and underruns, uninitialized variables, and use-after-free errors all trace back to undefined behavior baked into the language that the compiler is unable to catch. For CTOs weighing whether to stay with proven toolchains or adopt something new, the calculation has shifted.

Part of what has changed is the threat. Large language models can now find defects in critical software, working from both source code and compiled binaries. This introduces new failure modes. Where security teams once worried about attacks probing a system from the outside in, AI can reason about a codebase from the inside out, and most of the openings it surfaces trace back to undefined behavior. Regulators have noticed, and secure-by-design expectations are increasingly being written into the rules governing the development of safety-critical software.

Because the root cause is consistent, the responses cluster into four approaches.

The first is to constrain C and C++ with a coding standard such as MISRA or CERT. This keeps existing teams, tools, and code largely intact while measurably reducing risk. The disadvantage is that a subset is a discipline, not a guarantee. The unsafe constructs remain in the language, and a standard that depends on human compliance is easy to violate under deadline pressure. An added disadvantage is that sticking to the language subset requires manual review and is not always popular with the development team.

The second is to use a language where memory safety is built into the language's design rather than layered on top. Ada and SPARK fall into this category. Safety is enforced by the language and compiler rather than by convention, which removes whole classes of defects before code runs. The cost is a learning curve and, in some organizations, a cultural shift away from C.

The third is Rust, which also enforces memory safety through its ownership model and is gaining traction in embedded and automotive contexts. It offers strong guarantees with modern tooling, though the certification story and the maturity of qualified toolchains are still developing relative to more established options.

The fourth is CHERI, which enforces memory safety at the hardware level rather than in software. This is a promising long-term direction because it can protect existing code, but it depends on hardware availability and is the least mature of the four for production automotive use today.

These approaches are not mutually exclusive. The right mix depends on a team's existing codebase, certification targets, and tolerance for change.

Above all of them sits formal methods, which prove software properties at compile time rather than testing them afterward. Proof can establish the absence of run-time errors, the undefined behavior that causes so much trouble, and, at higher levels, prove that software does what its specification says. Formal methods are available in existing languages through tools such as Frama-C, and are native to languages such as SPARK and Dafny. There is even an open-source ISO 26262 process built around formal methods, published by NVIDIA.

This matters because of where development is heading. Agentic AI is changing how software gets built. Humans still drive the requirements and remain accountable for the result, but agents can increasingly translate those requirements into code, including formal specifications and tests, maintain traceability, run test suites, and gather coverage, with CI/CD platforms recording the chain of accountability. Agents can prove the absence of run-time errors as they go, thanks to the formal approach. Still, keeping humans in the review loop remains genuinely hard, and that responsibility does not move.

AI generates a lot of code quickly, but speed is worthless in a safety-critical system without a way to verify correctness. Formal methods supply exactly that: a mathematical check that does not depend on how the code was written, or on who, or what, wrote it. For a CTO, this is the practical payoff. The same techniques that make a language memory safe also give you a basis for trusting AI-generated code, which is the efficiency gain that justifies the investment. A review is still required, but the fact that the code has been formally verified increases confidence and makes the reviewer’s work easier and faster.

The encouraging part is that none of this is locked behind proprietary walls. Ada, SPARK, and Rust are all available in open source, and so is much of the formal methods tooling.

Click here to learn how formal methods can prove the correctness of AI-generated code in practice.