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.
Great question Nikos,
That function is you application that runs on top of Zephyr. It can be a single function, or a larger app. many teams have a mixture of C (from a legacy project) and SPARK code. They may move some of the C to SPARK to benefit from the formal methods and they often develop new content in SPARK.
As an example, for most of my home automation projects I call the Ada Main from the Zephyr main() and I implement all the functionality in Ada, reaching into Zephyr to use device drivers, MQTT, WiFi and the like.
Regards,
Mark
Thanks for the reply! It makes more sense now. In case you are aware of any github repo that demonstrates this concept, please send it our way!
Thanks anyways!
Regards,
Nikos
Mark, thank you for your well-done presentation! I wonder though, how do I get started with Ada/Spark on the NXP board. Is there an onboarding document somewhere for using Spark on this embedded system? How does Spark compare to Eiffel (or even Modula-3)?
Thank you!
/TS
Thanks Thomas,
If you have access to an LLM (Claude, Codex, ...), then grab the alire skill from https://github.com/AdaCore/skills and follow the prompt in the presentation.
If not, then
- install Alire from here: https://alire.ada.dev/
- Install West (https://docs.zephyrproject.org/latest/develop/west/install.html)
- west init -l .
- west update
- pip3 install -r ../zephyr/scripts/requirements.txt
Then you can clone this repo: https://gitlab.com/mhermeling/ada-eoc-philosophers and run make, and it should build and flash.
We also have an Ada Office Hours every second Friday, feel free to pop in:
https://www.adacore.com/ada-spark-office-hours
As to the difference between the languages, hard to summarize in a short response. They all have their different approach to programming. Ada SPARK is more of a systems-level language and is popular where safety matters.
Regards,
Mark
Welcome to ask questions, I'll check this area daily and will respond as quickly as I can.








Hey Mark,
pretty interesting topic!
Just a quick question for now, to understand something, since I'm completely new. In your demo with the binary search in Zephyr, I understand that you get in the end a function in Ada code that is SPARK formally proven (if I use the terminology correctly). But then, what do you do with this function? What is the idea with it? Can you call it in a normal Zephyr application written in C? Or is the idea that you also write the whole application in Ada?
Nikos