GNAT Foundry : Intersection
Since its inception, AdaCore has promoted languages and built tools that promote the safety and security of high-integrity software by establishing deterministic trust. Now, we’re showcasing how these tools can be applied to AI-powered high-integrity software development at speed.
AI Development is Different
AI-powered software development differs from traditional software development in two key ways:
AI Makes Mistakes
We must maintain human accountability over AI-authored artifacts to ensure the trustworthiness of the results.
AI Is Fast
AI generates or updates artifacts really fast. Without care, the sheer velocity of output can easily overwhelm human reviewers. So we must accelerate the review process and equip humans with tools that enable review of artifacts at speed and at scale.
How Do You Trust AI?
AI changes the cost equation in high-integrity software development. With AI, we have the potential to have high-integrity software in more places. This means safer, more secure software everywhere. Everybody wins. But first, we have to figure out how to trust the software that AI writes.
AdaCore’s answer to this challenge is simple. Don’t. Don’t trust the software that AI writes. Subject it to the same rigor as software written by humans. Use the same languages and tools that have been used successfully for over 30 years in high-integrity software development and apply them to AI-developed software. Let us show you how.
The Intersection Demo
We built a demo around an easy-to-understand concept: a four-way intersection with protected left turns and protected pedestrian crosswalks. This demo is GNAT Foundry: Intersection.
Demand-Led Left Turns
Left turns are released only when a vehicle is present.
Demand-Led Crosswalks
Walk signals are only produced in response to a pressed walk button.
Pedestrian Call Light
A call light indicates when a pedestrian has pressed the walk button.
Lead-Lag Left Turns
Left turns are released with their adjacent through movement.
How to Use the Demo
GNAT Foundry: Intersection is designed to run on Ubuntu 24.04 on aarch64 or x86_64. We recommend creating a container to run the demo, to provide isolation for when yourun the AI agentt.
GNAT Foundry: Intersection is on GitHub at https://github.com/AdaCore/gnat-foundry-intersection. Follow the instructions there to clone the repository.
If you are a GNAT Pro customer with GNAT Pro for Ada, SPARK Pro, and GNAT DAS, run `make setup-pro` and follow the instructions.
If not, run `make setup-community` and the demo will install the required tools from the community index.
Run `make run-native` to build and run the demo. Experiment with calling for crosswalks and left turns to get a feel for how the system works.
Run `make report` to establish the full set of artifacts that furnish deterministic trust in the correctness of the baseline. Once the report is built, open it in your browser and explore the evidence to get a feel for what's there. The report is fully green at the outset, as expected for the baseline.
Using your AI agent, load our prompt with `@demo/demo-prompt.md`. The agent will apply a diff to the CONOPS that represents the approached change request. Then, the agent will follow the workflow we've defined to edit all of the artifacts, from requirements to code to tests to proofs. This takes about two hours and costs about $50 using frontier AI agents.
Run `make report` again to see what the agent did. All report items should be green showing that deterministic trust in the correctness of the system has been reestablished after the change was made. If human review is needed, it will be called out clearly in the report.
You should also run `make run-native` again to see the change to the system in action: now, when a crosswalk enters flashing DON'T WALK, a countdown time is displayed for that crosswalk!
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 demonstrates 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.
Trust the Workflow
GNAT Foundry: Intersection also demonstrates critical elements of an AI-powered high-integrity software-development workflow.
High-Integrity Workflows
Detailed workflows guide the AI agents in going from CONOPS, via HLR, LLR to code and tests and how they can measure correctness and completeness.
Reporting
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, and outputs from the verification tools.
Traceability
The report offers comprehensive traceability from requirements to code, proofs, tests, and test results.
See it for Yourself
Help your team understand the value of Ada and SPARK when building high-integrity systems using AI. Reach out and we will show you how the deterministic trust our tools provide applies to your code, with or without AI involved.
Get the Demo
Want to try GNAT Foundry : Intersection yourself? Go to the GitHub repository, clone it, and follow the instructions in the README.
FAQs
No, it is not an actual implementation of a traffic light control system. We used the traffic light example as it is something that is easy to understand, still sufficiently complex and safety related. This project demonstrates how a software development team can use artificial intelligence to develop high integrity software. The project uses Ada SPARK and formal methods to deliver deterministic trust in the artifacts generated by AI.
No, the Ada SPARK toolchain is open source, tools and provers are readily available and this project can be completely run using the open source toolchain, including formal methods and code coverage.
Correct, the brownfield project has requirements, an architecture, and source code that AI can extend. We are now working on a demonstration that describes how to apply this in a greenfield project.