AdaCore GNAT Foundry Intersection: Formal Proof and MC/DC Checks for AI-Written SPARK
AdaCore's GNAT Foundry: Intersection is an open-source demonstration of an AI-assisted development workflow for high-integrity software. Released on September 14, 2026, the project surrounds an agent-driven code change with deterministic checks from Ada and SPARK tooling: compilation, formal proof, requirements-based tests, structural coverage and requirements-to-code traceability.
The public repository provides a complete traffic-controller example and a scripted change request. It runs on Ubuntu 24.04 on x86_64 or AArch64, supports community and commercial AdaCore toolchains, and can use Claude Code or Codex for the agent-driven change. AdaCore estimates the supplied change request takes about two hours and costs about $50 with frontier AI agents.
The useful engineering idea is reproducibility. The AI edits requirements, implementation and tests, while established analysis tools produce evidence that reviewers can inspect independently of the model's own explanation.
What the demo contains
GNAT Foundry models a four-way intersection with protected left turns and pedestrian crosswalks. The repository includes a Concept of Operations, high-level requirements, software architecture, low-level requirements, Ada/SPARK implementation, requirements-based tests, proof artifacts and an interactive HTML report.
The baseline controller supports demand-led turns and crosswalks, pedestrian call lights and lead-lag left-turn scheduling. The supplied change request adds a countdown display during the flashing DON'T WALK phase.
The implementation can target native Linux or a bare-metal 32-bit Arm target. A simulation harness replaces physical intersection hardware for the demonstration.
| Layer | Evidence produced |
|---|---|
| Ada compilation | Type and compile-time checks |
| SPARK Silver | Proof of absence of runtime errors |
| SPARK Gold | Selected functional-correctness proofs against requirements |
| GNAT Test | Requirements-based test execution |
| GNAT Coverage | Statement and MC/DC structural coverage |
| Report/traceability | Links requirements, implementation, proofs, tests and results |
AdaCore reports 100% statement and modified condition/decision coverage (MC/DC) for the controller's requirements-based test suite in the supplied baseline. That figure describes this demonstration and should be read as project-specific evidence, rather than a general benchmark for AI-generated software.
Hardware and software requirements
The repository README currently specifies Ubuntu 24.04 on x86_64 or AArch64. Required host tools include Git, Make, curl, tar, unzip, Bash, build-essential and libgmp-dev. The setup process also needs network access and approximately 10 GB of free disk space.
Bare-metal Arm builds additionally use qemu-system-arm. The community setup path installs the required open-source tooling; the Pro path expects GNAT Pro, SPARK Pro and GNAT DAS tooling through an eligible GNAT Tracker account or an existing installation.
The repository is dual-licensed under Apache License 2.0 or Creative Commons Attribution 4.0 International, at the user's option.
How the workflow runs
The baseline can be built and inspected before an AI agent changes anything. After cloning the repository, the community path starts with:
make setup-community
make run-native
make report
The generated report is available under reports/report/html/index.html. It establishes the initial evidence set for the baseline implementation.
For the provided change request, the repository instructs Claude Code or Codex to read and execute demo/demo-prompt.md. The agent updates the engineering artifacts needed for the requested behavior, including high-level requirements, low-level requirements, code and requirements-based tests. It also runs the proof and coverage workflow and repairs issues encountered during that process.
After the change completes, make run-native exercises the modified controller and make report regenerates the evidence package. Reviewers can then inspect requirements, code, tests, proof output, coverage and traceability from the report.
Where deterministic checks help
AI coding systems can produce a large patch quickly, which shifts part of the review problem from writing code to establishing whether the resulting artifacts satisfy explicit requirements. GNAT Foundry demonstrates several complementary checks for that problem.
SPARK proof addresses classes of runtime failures and selected functional properties. Requirements-based testing exercises specified behavior. MC/DC coverage shows whether test execution independently exercises conditions that influence decisions, a form of structural evidence widely used in high-integrity development. Traceability connects requirements to implementation and verification artifacts so reviewers can follow the evidence chain.
These mechanisms test different properties. A green compiler result, successful proof, passing tests and complete coverage each answer a different question; the report brings those results together instead of treating one signal as a universal correctness score.
Human review remains part of the trust boundary documented by the project. The report explicitly identifies the Concept of Operations, CONOPS elements outside software traceability and derived high-level requirements as areas requiring human review. AdaCore also describes the current example as a demonstration rather than a certification process.
Community versus Pro setup
The project is usable with the community Ada/SPARK toolchain. make setup-community provisions the open-source path, which makes the core demonstration accessible without purchasing AdaCore's commercial products.
make setup-pro is intended for GNAT Pro, SPARK Pro and GNAT DAS customers. That route can use Pro tool archives staged under pro-downloads/ or tools already available on the system path.
This separation is important for evaluation: developers can inspect and reproduce the workflow with public artifacts, while organizations already using AdaCore's commercial high-integrity stack can evaluate it in a closer approximation of their supported environment.
What the demonstration establishes
GNAT Foundry is most relevant to teams evaluating AI assistance in software where requirements, verification artifacts and review evidence matter as much as source-code generation. The project provides a concrete reference workflow instead of only proposing that formal methods could supervise an AI coding agent.
Its strongest reusable pattern is the separation between generative work and deterministic verification. The agent can modify multiple engineering artifacts, but acceptance evidence comes from compilers, provers, test execution, coverage measurement and traceability. That architecture gives reviewers concrete artifacts to inspect and makes failed verification visible in the same workflow that produced the change.
The present Intersection project is a brownfield demonstration built from an established baseline. AdaCore says a greenfield demonstration is planned. The current repository therefore provides the clearest evidence for AI-assisted modification of an existing high-integrity system with an existing verification chain.
Bottom line
GNAT Foundry: Intersection is a practical open-source example of combining an AI coding agent with Ada/SPARK formal methods and conventional verification tooling. It packages requirements, source code, proof, testing, MC/DC coverage and traceability into a reproducible workflow that can be run with community tooling on Ubuntu 24.04.
For engineering teams considering agentic coding in high-integrity environments, the project is useful as an architecture reference: let the agent generate and update artifacts, then require deterministic evidence from independent tools before accepting the change.
Sources
- AdaCore press release, September 14, 2026: https://www.adacore.com/press/adacore-releases-demonstrator-for-trustworthy-development-with-ai
- AdaCore GNAT Foundry: Intersection technical page: https://www.adacore.com/gnat-foundry-intersection
- AdaCore technical article: https://www.adacore.com/blog/gnat-foundry-intersection-demonstrating-trustworthy-ai-development
- GNAT Foundry: Intersection repository and README: https://github.com/AdaCore/gnat-foundry-intersection
- Independent coverage from Unmanned Systems Technology: https://www.unmannedsystemstechnology.com/2026/09/adacore-demonstrates-deterministic-guardrails-for-ai-high-integrity-software-development/