AdaCore Releases Demonstrator for Trustworthy Development with AI
AdaCore has released GNAT Foundry: Intersection, an open-source demonstrator of how human engineers can collaborate with AI to deliver high-integrity software. The demo shows how formal methods and trusted tools can guide AI in a high-integrity software development workflow.
AI serves as a powerful tool, enabling human engineers to work more efficiently and effectively. Rather than replacing human engineers, AI can automate many of the steps required to produce high-integrity software.
But AI brings two key challenges to high-integrity software development: firstly, AI fails in ways that are different from humans and are therefore difficult to predict, and secondly, AI generates artifacts so quickly that this can easily overwhelm human reviewers. GNAT Foundry demonstrates a workflow that addresses this by leveraging deterministic trust furnished by non-AI tools as guardrails around AI-generated artifacts, so that humans can focus their attention where it is required. AI drives Ada SPARK-based tools; the tools produce the evidence. The evidence is backed by formal proof, requirements-based test results, structural coverage measurements, and traceability data generated by qualified, established tooling.
AdaCore provides support for the Ada SPARK tooling to software projects that build high-integrity software through their GNAT Pro, SPARK Pro, and GNAT DAS offerings. GNAT Foundry: Intersection demonstrates how to use AI in a trustworthy way to both open-source and proprietary projects and demonstrates AdaCore’s thought leadership in high-integrity software development.
“AI can automate many of the steps required to produce high-integrity software, but as with any development project, it requires an instrumented process to build confidence in the correctness of its outcomes,” said Quentin Ochem, Chief Product Officer at AdaCore. “What our tools contribute is deterministic trust. Tools that have been proven over decades to deliver the highest levels of software quality with traditional development methodologies can now be tuned to verify AI-generated artifacts and provide evidence that is trustworthy, reproducible, and actionable. This makes AI-generated artifacts, whether tests, reviews, or even code, usable in high-integrity software.”
The demonstrator is published as a public repository that engineering teams can clone and run themselves. It is built around a traffic light controller, a complete working example, small enough to inspect and representative enough to be realistic. The workflow is agent-neutral and has been tested with multiple commercial coding AI solutions to confirm that the results do not depend on any single vendor’s model.
The demonstrator repository is available at http://github.com/AdaCore/gnat-foundry-intersection, and you can read more here.
