Three Ways SPARK Catches Bugs Before Your Hardware Does

If you’ve been writing embedded software in C for any length of time, you know the drill. You write the code, it compiles cleanly, you flash it, and then something explodes or smoke curls up to the sky, sometimes figuratively, sometimes there is actual smoke. A buffer overrun here, a mistyped register value there, a type that silently wraps around at 255 when you needed 300.

SPARK is a formally verifiable subset of Ada designed for exactly this environment: constrained, safety-critical, low-level embedded systems where a runtime crash is not an option. Here are three concrete examples of where SPARK eliminates entire classes of bugs that C leaves open.

Example 1: Array Out-of-Bounds Write

The C problem

In C, an array is a pointer. The language lets you write past its end without complaint.

uint8_t buffer[8];
void fill(uint8_t *buf, int index, uint8_t value) {
   buf[index] = value;  // index = 10? No problem. Memory corrupted.
}

This compiles. It runs. It corrupts whatever lives after buffer in memory, which in an embedded system might be a stack frame, a peripheral register, or another task’s data. The fault may not surface until much later, in a completely unrelated part of the system.

How SPARK prevents it

In SPARK, arrays carry their bounds as part of their type. The compiler and proof tools know the valid range, and any access outside it is an error, mostly caught at compile time rather than at runtime on hardware.

type Buffer_Index is range 0 .. 7;
type Byte_Buffer  is array (Buffer_Index) of Interfaces.Unsigned_8;

procedure Fill (Buf   : in out Byte_Buffer;
                Index : in     Buffer_Index;
                Value : in     Interfaces.Unsigned_8) is
begin
   Buf (Index) := Value;  -- Index can only be 0..7. Proven.
end Fill;

It is hard to pass an out-of-range index. The type system guides the programmer. However, there are cases where the compiler may not be able to assist, for example, if Index is obtained programmatically, like read from disk or a socket. In that case, the Ada runtime system throws an exception at runtime if the index is out of range.

The compiler is only the first step where SPARK helps. The GNATprove tool that comes with SPARK adds a layer on top. It can provide compile-time guarantees that out-of-bounds writes cannot happen at runtime through deductive formal verification. Compile-time proof, through the use of formal methods that no runtime failures can occur.

Example 2: Writing the Wrong Value to a GPIO Register

The C problem

GPIO configuration in C typically means writing magic numbers to memory-mapped registers. The types offer no protection; a register that accepts only a 2-bit field will silently accept any 32-bit value you hand it. This is the power of C, but also part of its downfall.

#define GPIOA_MODER  (*(volatile uint32_t *)0x48000000)
#define MODE_OUTPUT  0x1

void configure_pin(void) {
    GPIOA_MODER = 0x00000005;  // Correct? Wrong pin? Wrong mode? Who knows.
}

The compiler cannot tell you if 0x00000005 is a valid configuration, whether you’ve hit the right bit positions, or whether you’ve accidentally configured a pin you didn’t intend to touch. This class of bug is especially painful on microcontrollers, where a wrong register write can silently misconfigure the hardware and produce symptoms that appear to be a firmware logic error.

How SPARK prevents it

SPARK’s representation clauses let you model the hardware register layout directly in the type system. The register structure becomes a first-class type with named fields, explicit bit positions, and constrained value ranges.

type GPIO_Mode is (Input, Output, Alternate, Analog)
   with Size => 2;

type MODER_Register is record
   Pin_0 : GPIO_Mode;
   Pin_1 : GPIO_Mode;
   --  ... remaining pins
end record
   with Volatile_Full_Access, Size => 32, Bit_Order => System.Low_Order_First;

for MODER_Register use record
   Pin_0 at 0 range 0 .. 1;
   Pin_1 at 0 range 2 .. 3;
end record;

GPIOA_MODER : MODER_Register
   with Address => System'To_Address (16#48000000#);

--  Configuration is now named, typed, and range-checked:

GPIOA_MODER.Pin_0 := Output;

You can no longer write an invalid mode value. You can no longer accidentally shift bits into the wrong field. The layout is verified against the hardware spec at the type level during compilation. What used to be a source of subtle, hard-to-reproduce hardware bugs becomes a compile-time constraint. On top of that, people can actually read and understand the code.

Example 3: Type Overrun

The C problem

C integer arithmetic silently wraps. A uint8_t that reaches 255 rolls over to 0 on the next increment. A computation that overflows an int16_t produces a garbage value with no warning, no exception, and no indication that anything went wrong.

uint8_t count = 250;
count += 10;  // count is now 4. Not 260. No error. No warning.

uint16_t sensor_reading = 60000;
uint16_t calibrated = sensor_reading + 10000;  // Wraps to 3392. Silent.

In safety-critical embedded code, sensor fusion, actuator control, protocol state machines, a silently wrapped integer can cause a system to make a dangerously wrong decision. The value looks valid. The type is satisfied. The behavior is wrong.

How SPARK prevents it

At SPARK Silver level, the GNATprove tool checks for overflow on every arithmetic operation. You define the range your type must satisfy, and GNATprove verifies that no execution path can produce a value outside it. Overflow becomes a proof obligation, not a runtime surprise.

type Sensor_Reading is range 0 .. 65_535
   with Size => 16;

type Calibrated_Reading is range 0 .. 70_000
   with Size => 32;

function Calibrate (Raw : Sensor_Reading) return Calibrated_Reading is
   Result : constant Calibrated_Reading := Calibrated_Reading (Raw) + 10_000;
begin
   return Result;
end Calibrate;

Run GNATprove on this and it refuses to discharge the range check on Result. The reasoning is simple: Raw can be as large as 65_535, so Calibrated_Reading (Raw) + 10_000 can reach 75_535, which exceeds Calibrated_Reading‘s upper bound of 70_000. GNATprove won’t sign off on code it can’t prove safe, and it tells you exactly where the obligation fails.

You fix it by tightening the contract, either narrow Raw‘s range with a precondition, widen Calibrated_Reading, or saturate the result explicitly. The point is that the failure surfaces at proof time, before you’ve written a single byte to a microcontroller. The guarantees are mathematical and up-front.

The Bottom Line

These aren’t theoretical advantages. Array bounds, register layout, and type overflow are three of the most common sources of defects in embedded C codebases, and they share a common cause: the C type system simply does not model the constraints that matter in your domain.

SPARK does. The type system is expressive enough to encode hardware layout, value ranges, and memory bounds directly. The proof tooling verifies them statically. The runtime cost is zero.

SPARK users report up to 70% fewer defects compared to projects developed in C. This is empirical data, not a marketing statistic.

That’s not a marginal improvement. That’s a different class of safe and secure software.