Reduce Cost While Improving Safety and Security with Formal Methods Through Ada SPARK

There are three conflicting needs for teams that are building software systems that have to adhere to functional safety and security standards such as ISO 26262, IEC 61508, ISO 62443, R155 and others. Firstly, they have to adhere to very strict security standards, secondly, they have to deliver on-time and on-budget and lastly, they have to frequently deliver updates to deliver more functionality as well as fix any reported security issues.

In this presentation, we will walk through a small sample application in Ada SPARK and demonstrate how it delivers improved safety and security at lower cost in three steps:

• Firstly, memory safety and type safety removes a significant amount of runtime problems.
• In the second step, we will tighten the program to be able to prove the absence of runtime errors completely.
• In the third step, we will prove the correctness of the program.

The presentation will also touch on how companies like NVIDIA and Rolls Royce depend on Ada SPARK, enabling them to deliver safe and secure software at scale.

What this presentation is about and why it matters

How do you bring formal methods into an embedded project without turning it into a research exercise, or a schedule risk? Mark Hermeling frames that tension through Ada SPARK, then walks through a concrete, hands-on path: what SPARK is, how contracts fit into normal code, what the proof levels mean, and how a small binary search example can be lifted with tool support. He also grounds the discussion in industrial use cases and reported cost, safety, and security benefits. This is a good fit if you want a practical entry point to deductive verification and a sense of where it fits in real embedded workflows.

Who will benefit the most from this presentation

• Embedded software engineers evaluating formal methods for safety-critical or security-sensitive code
• Team leads who need a pragmatic path from existing code to higher assurance
• Developers working in Ada, or considering Ada SPARK for a new project
• Engineers using LLMs for code generation and looking for stronger verification guardrails

What you need to know

Helpful background, but not required:

• Basic familiarity with embedded software development and common runtime failure modes
• Comfort reading code and simple precondition/postcondition style specifications
• Some awareness of Ada is useful, though the talk introduces the core ideas

Glossary (terms used in this talk)

• LLM (large language model): A statistical machine learning model trained on large corpora of text to generate or analyze natural language outputs.
• loop invariant: A condition that remains true before and after each iteration of a loop. Loop invariants help prove that a loop preserves important properties while it runs.
• postcondition: A requirement that must hold after a function or procedure completes. Postconditions describe the guaranteed outcome of a routine when its preconditions are satisfied.
• precondition: A requirement that must hold before a function or procedure is called. Preconditions make contracts explicit and allow callers and verification tools to reason about valid inputs.
• SPARK: A subset of Ada designed to support formal verification by restricting language features that complicate reasoning. It is commonly used to prove properties such as absence of runtime errors or functional correctness.
• Verification conditions: Logical formulas generated from code and specifications that must hold for a proof to succeed. They are typically discharged by automated theorem provers.
• Contract: A specification attached to a subprogram that describes what must be true before it runs and what it guarantees after it completes. Contracts make assumptions and guarantees explicit for both humans and tools.
• Zero-footprint runtime: A runtime environment designed to add minimal overhead while supporting application code and verification constraints. It is often chosen when predictability and small footprint matter.

Toolbox (mentioned in this talk)

• GitHub Copilot: An AI coding assistant that can generate or complete code from prompts and surrounding context. It is often used to scaffold repetitive code and boilerplate faster than writing it manually.
• Zephyr: Zephyr is an open-source real-time operating system for resource-constrained devices, supported by many embedded toolchains and debuggers.
• AdaCore ALIRE: A package manager and project manager for Ada and SPARK ecosystems. It helps fetch dependencies and set up tools needed for development and verification.
• GNAT Pro: An Ada compiler toolchain used to build efficient Ada and SPARK applications. It targets a wide range of desktop, embedded, and real-time platforms.
• NXP MCXW71 Freedom Board: A development board for building and testing embedded applications on NXP MCXW71 hardware. It can be used as a concrete target for running and validating firmware examples.

Final thoughts

Practical and tutorial-style, this session gives you a grounded look at what formal verification feels like in an embedded codebase, not just what it is in theory. The value is less about a checklist and more about a working mental model for contracts, proof levels, and how tools, code, and target constraints fit together. It will especially help engineers and leads who want stronger assurance without losing sight of delivery. The tone stays close to the work, which makes the topic feel reachable.

This overview is AI-generated from the session transcript. Spot an issue? Let us know.