SPARK Doesn't Comply With MISRA C. It Makes Most of It Moot.

If you build flight control software, autonomous driving stacks, or implantable devices, someone has probably asked whether SPARK is "MISRA C compliant." It is the wrong question, and answering it literally will waste your team's time.

MISRA C is a set of guidelines for writing C that avoids the language's many traps. SPARK is a different language, a verifiable subset of Ada. Asking whether one complies with the other is like asking whether your seatbelt passes the airbag test.

The useful question is narrower: for each MISRA rule, what happens to the underlying hazard when you write the code in SPARK instead of C? I went through all 18 directives and roughly 155 rules in MISRA C:2025. The answers fall into four groups.

Four outcomes, not one

• Moot. The C construct that the rule policies do not exist in Ada, so the hazard cannot occur. This is the largest group by a wide margin.
• Rejected by the language. Ada's rules or the SPARK subset make the construct illegal, so the compiler stops you.
• Proven absent. SPARK's flow analysis and gnatprove guarantee the defect cannot happen. This is the smaller, high-value group.
• Still your problem. Process, documentation, and some resource handling that no language removes.

The interesting finding is how much lands in the first bucket.

Whole chapters disappear

MISRA C devotes an entire chapter, Rules 10.1 through 10.8, to its "essential type model." That model exists for one reason: C performs implicit conversions that silently change values. Ada does not allow them.

type Pressure_Bar is range 0 .. 500;
type Altitude_M   is range 0 .. 20_000;

P : Pressure_Bar := 100;
A : Altitude_M;
begin
   A := P;  -- compile error: these are different types

You cannot assign one to the other without an explicit conversion, and that conversion is range checked. The class of bug chapter 10 tries to discipline is gone, so all eight rules are moot.

The same thing happens elsewhere:

• Chapter 11 (pointer conversions): Ada access types are strongly typed, and SPARK forbids pointer arithmetic, so most of these rules describe operations you cannot write.
• Chapter 20 (the preprocessor): Ada has no preprocessor, so all fifteen rules vanish.
• Chapter 23 (_Generic selections): a C11 feature with no Ada analog.
• Almost all of chapter 21: these rules ban specific C standard library functions you would never call from SPARK.

Add the scattered moot rules across other chapters, and well over half of MISRA C is simply not applicable.

What SPARK actually proves

The rules that matter are the ones SPARK turns into guarantees rather than advice. A C programmer follows these by discipline and hopes a reviewer catches the lapses. In SPARK, they are checked, and exactly which guarantee you get depends on how far up the SPARK assurance ladder you go. AdaCore defines five levels, each building on the last: Stone (valid SPARK), Bronze (initialization and data flow), Silver (absence of run-time errors), Gold (key integrity properties), and Platinum (full functional correctness).

Two of those levels do the heavy lifting against MISRA, and they cost very different amounts of effort.

Bronze, from flow analysis, is close to automatic. gnatprove runs flow analysis and gives you:

• No reads of uninitialized variables (Rule 9.1).
• No aliasing or evaluation order surprises (Rules 13.2, 19.1). SPARK forbids side effects in expressions and uses an ownership model for pointers, so two names cannot quietly refer to the same object.
• No data races (Directive 5.1), which flow analysis detects directly. Deadlock freedom (Directive 5.2) and the ban on dynamic tasks (Directive 5.3) are mandated by the Ravenscar and Jorvik profiles by construction.

Silver, from proof, is the line that earns the strong claims. Silver level statically proves the absence of runtime errors (AoRTE): no exceptions can be raised at runtime. This is what discharges:

• No out-of-bounds access (Rule 18.1).
• No integer, fixed-point, or floating-point overflow (the heart of Directive 4.1, plus Rules 12.2 and 12.4).
• No divide by zero and no range violations.

Silver is the default target for critical software, and a Silver-proven subprogram carries a strong consequence: because no run-time error can occur, the run-time checks can be safely disabled, which matters when you are arguing performance parity with C under DO-178C or EN 50128.

That core, initialization, and data flow at Bronze, run-time safety at Silver, is exactly what MISRA can only ask C developers to achieve by hand, or through automated tooling such as static analysis.

This review, whether manual or automated, takes time and effort and is often demotivating. Writing a new feature in C and then finding 30 MISRA warnings to resolve when you submit it is not encouraging for new software developers. SPARK tackles this partially by language design and partially in the compile and proof step, empowering software engineers to write better code.

The catch worth knowing

The levels are not equal in cost, and conflating them is what makes a SPARK pitch lose a skeptical engineer. Stone and Bronze are cheap: Bronze is largely automatic, with no proofs attempted, just data and flow analysis.

Silver is where the bill arrives. Proving the absence of runtime errors means gnatprove has to discharge every check, and in real code, that routinely means adding preconditions, postconditions, and loop invariants by hand. The effort is usually called modest, but modest is not zero, and it scales with how much your code pushes the limits of integer ranges and array bounds.

Frontier Large Language Models and Agentic AI systems are a great help here. They are getting better at assisting developers in adding these preconditions and invariants, making Silver proof more affordable and erasing the additional time investment.

So the honest claim is not "SPARK gives you MISRA for free." It is "SPARK removes most of MISRA's hazards by construction, gives you initialization and data flow safety at Bronze for almost nothing, proves the run-time safety core at Silver for some real effort, and leaves you a short list of genuinely human responsibilities."

A few rules survive only partially, so know them before you write a deviation record claiming full coverage. SPARK forbids backward goto but allows the forward form. Recursion is permitted but must be proven to terminate.

Hardware Access

There is one more benefit of Ada and SPARK that is worth calling out: the concept of representation clauses. Ada allows the engineer to define the registers of a hardware device in a type. It allows the engineer to define bit fields and enumerations, specify the number of bits used to store each enumeration, and specify how each enumeration is stored in bits. It then prevents engineers from writing wrong information into the hardware. You can no longer, by accident, write a word in a byte and overrun the next hardware register.

In other words, Ada SPARK ensures type safety and eliminates runtime errors all the way down to the hardware. This is a differentiator often overlooked when building embedded systems.

What is left for you

Strip out the moot and language-rejected rules, and what remains is small and mostly non-code: documenting implementation-defined behavior, requirements traceability, not shipping commented out code, validating external inputs, and some file resource handling. That is your real MISRA workload in a SPARK project.

Try this today: take your current MISRA C deviation log, cross out every rule in chapters 10, 11, 20, and 23, then strike everything in 21 that names a C library function. How much time would you have saved, how many times has problematic code been integrated into your software, and how much time would you have saved had SPARK protected you?

Ready to shrink your deviation log? Get in touch with one of our experts to discuss SPARK here