GNAT Foundry Intersection: Demonstrating Trustworthy AI Development

High-integrity software runs the world quietly; traffic lights, point-of-sale terminals, industrial manufacturing, medical devices, cars, trains, airplanes. We rarely notice it until it fails. And when it fails, the consequences are real: breaches of privacy, financial loss, injury, and even loss of life.

That's why people refer to software for these systems as high-integrity software, and high-integrity software is built differently. It is rigorously reviewed and thoroughly tested before deployment. Building high-integrity software takes more focus, more time, more people, and hence costs more. Building to a standard of high integrity keeps us safer, but the increased cost creates tension: we want more high-integrity, safe, and secure software, yet too often the economics don't allow it to be built or bought. The result is a world less safe and secure than it could be. AdaCore believes that AI has the potential to reverse these economics. Using AI, we should be able to deliver safer, more secure software faster and at lower cost.

The key barrier to realizing this potential is trust. How can we trust that the output of AI is correct and complete, especially given the importance of both in high-integrity systems? The answer to date has been “human review of all AI outputs”. But this is slow and doesn’t scale. We propose a different answer: our tools, driven by an AI with a well-defined workflow, can help furnish the required trust, dramatically lowering the barrier to using AI.

We built a demonstration project of how we think this can work and published it as GNAT Foundry: Intersection on GitHub. It showcases how our tools bring deterministic trust to AI-powered workflows. If you want to dive right in, clone the demo repository here and follow the instructions in the README. To understand better why we think our approach is unique, credible, and will change high-integrity software development, read on.

Trusting AI Authored Code

AI brings two key challenges to high-integrity software development:

1. AI fails in ways that are different from humans and therefore difficult to predict, so we must retain human accountability for all artifacts that are AI-authored;
2. AI generates artifacts so quickly that they can easily overwhelm human reviewers, so we must find ways to accelerate the review process and build trust by using deterministic tools to guard AI output.

In high-integrity software development, humans must remain accountable for the artifacts that are produced, whether AI- or human-authored. To date, the typical answer to the question “how do we ensure trust in this AI-authored code” has been “human review”. But that approach doesn’t scale and doesn’t play to human strengths.

GNAT Foundry demonstrates a stronger alternative: leverage deterministic trust furnished by non-AI tools everywhere possible, so that humans can focus their attention where it is required.

Since its inception, AdaCore has promoted languages (like Ada and SPARK¹) and built tools (like GNATprove, GNAT DAS, CodeSonar, and others) that enhance the safety and security of high-integrity software through deterministic trust. Now, we’re showcasing how our tools can be applied to AI-powered high-integrity software development at speed.

The Intersection Demo

We took a familiar, easy-to-understand system and made it the foundation of our first GNAT Foundry demo: a four-way intersection with protected left turns and pedestrian crosswalks. We call this demo GNAT Foundry: Intersection.

Some features of the demo:

• The left turns are demand-led: they are only released when there is a vehicle present.
• The pedestrian crosswalks are demand-led: they are only released when a call button is pressed.
• The pedestrian crosswalks have a call light: it turns on when pressed and turns off when the walk signal is given.
• Initially, no countdown timer is displayed when the pedestrian control head shows flashing DON’T WALK.

To get started, we built a set of comprehensive systems- and software-engineering artifacts:

• a Concept of Operations (CONOPS)
• High-Level Requirements (HLRs)
• a software architecture description document
• Low-Level Requirements (LLRs)
• a software implementation targeting native or a bare-metal Arm 32-bit

The CONOPS is derived from and traces to the US Department of Transportation Manual on Uniform Traffic Control Devices.

For demonstration purposes, we added a simulation harness that stands in for the physical hardware with which the software would interact. The simulation harness runs on Linux, but the Ada code can just as well be run on a microcontroller with an RTOS or bare-board without an RTOS.

We then developed comprehensive artifacts that verify the LLRs:

• proofs of absence of runtime errors, using SPARK (SPARK Silver)
• proofs of correctness, using SPARK (SPARK Gold)
• compile-time verifications, using Ada’s support for the same
• requirements-based tests sufficient to yield 100% MC/DC and statement coverage

Finally, we developed a comprehensive traceability matrix that is presented through an interactive HTML report.

The report clearly identifies where human review is essential:

• the CONOPS, as the root of the chain of trust
• the CONOPS elements not traced to software
• the derived requirements in the HLRs

Aside from this trust core, the report relies entirely on evidence produced deterministically by AdaCore’s tools to establish trust in the software.

How to Use the Demo

The GNAT Foundry: Intersection demo is hosted on GitHub here. The demo:

• automates setting up the tools you need
• provides a working baseline with a fully green report, out of the box
• provides a scripted change request for your AI agent to complete

Clone the demo, then run make setup-community to use the GNAT FSF tools or make setup-pro if you have the complete set of GNAT Pro tools.

Run the baseline with make run-native. You’ll see a graphical representation of the intersection, the traffic lights, and the crosswalks. Play around with the simulation for a bit to get a feel for how things work.

Then, run make report. The baseline report shows all green: the human-reviewed elements are signed off; the deterministic trust is intact: all of the traceability, requirements verification, proof, and structural coverage evidence is present and correct. Play around with the report: follow the traceability links, read some of the documents, compare what you see to the simulation. You should come away from your review of the report confident that the baseline system is correctly and completely implemented, based on the verification evidence presented.

Finally, the meat of the demo: the change request, which adds countdown timers to the pedestrian control heads. Fire up your AI agent and instruct it to read and follow the prompt contained in demo/demo-prompt.md. The agent will apply a patch to the CONOPS that represents the initiation of a formal change-request process. This patch is preapproved, so no new/additional human review is needed. From there, the agent follows a rigorous workflow to:

• update the HLRs, architecture, LLRs, implementation;
• write new requirements-based tests; write additional proofs;
• run the full set of verifications; and
• update the report.

The result will be a report that’s at least mostly green: all of the elements of deterministic trust will be green; the agent may introduce one or more additional items for human review.

This step illustrates how detailed workflows can be applied to guide the AI agents in going from CONOPS, via HLR, LLR, to code and tests, and how they can measure correctness and completeness. GNAT Foundry includes definitions for subagents that are invoked to drive the change-request process from start to finish.

Trust the Evidence

The central message of GNAT Foundry is that you should trust the deterministic evidence furnished by our tools. You don’t have to review all of the code to know that it does all and only what you intend; the evidence furnishes this trust and focuses your review on the key artifacts in which the trust is rooted. Here’s how that trust is built.

• Compilation: GNAT tells you that the code is type-safe and complies with the compile-time checks that were written to verify specific requirements.
• Proof: SPARK proves that the code is free of runtime errors (SPARK Silver) and that the code complies with proof obligations that were written to verify specific requirements (SPARK Gold).
• Tests: tests are executed using GNAT Test, which ensures that all of the requirements-based tests pass.
• Coverage: structural coverage is measured using GNAT Coverage during execution of the requirements-based tests, the report shows that 100% MC/DC and statement coverage are obtained.

While GNAT Foundry: Intersection is not demonstrating any particular certification process, all of the tools listed above have been qualified against various standards across many different target environments.

The report that GNAT Foundry produces offers a quick entry into the artifacts and supports drilling down to the lowest level of detail, exposing all of the requirements, code, tests, outputs from the verification tools, and, critically, traceability between all of these artifacts. Our claim is that by verifying that the report is green after the agent has finished its work, you have the evidence you need to conclude that the work is correct and complete. Of course, in a certified software project, you would need to review the edits to the HLRs, LLRs, and confirm that the test cases are correct and complete for their requirements. But the key elements of trust are automatically and deterministically put in place by the workflow the agent follows and the tools it uses.

GNAT Foundry: Intersection is unique. Nowhere else will you find an agent driving a complete chain of deterministic trust from a single vendor that includes formal proof, MC/DC coverage, qualifiable tools, certifiable runtimes, and support for embedded targets.

Brownfield v Greenfield

GNAT Foundry: Intersection demonstrates brownfield AI-powered development. Because we start from a complete baseline with an existing, complete chain of deterministic trust, the AI agent both benefits from what’s already there (via in-place learning) but also has to fit into what’s already there (constraining the choices it may make). Many high-integrity systems fit this pattern: an established, existing system with established, existing evidence into which teams are struggling to figure out how to use AI in a trustworthy manner. If you’re such a team, we built GNAT Foundry: Intersection for you.

But GNAT Foundry also works in a greenfield context. The workflow that the AI agent follows enables trustworthy use of AI for brand new systems as well, instructing the agent how to write and verify all of the artifacts demonstrated, from the CONOPS to the tests. We’ll have a follow-up demonstration soon that illustrates using GNAT Foundry in a greenfield context; in the meantime, you can try it yourself using the resources provided in the GNAT Foundry: Intersection demo.

Next Steps

GNAT Foundry: Intersection demonstrates deterministic trust in AI-produced outputs in the context of a high-integrity system. If you can’t run the demo yourself, reach out to us and we'd be happy to show it to you.

If you want to learn more about AdaCore’s tools and how the deterministic trust they provide can help your team develop high-integrity software, with or without AI involvement, reach out to us here.

And stay tuned for more. This is just the beginning.

¹_{For people who are not familiar with Ada and SPARK: Ada is a modern programming language that has been used in the delivery of high-integrity systems for decades. Ada has object orientation, built-in concurrency, generics and is inherently type-safe and memory safe. SPARK is the formal subset of Ada that enables the use of formal methods to prove the absence of runtime errors (absence of undefined behavior) and can prove functional correctness of an implementation against a specification.}