AdaCore has released a new demonstration project, GNAT Foundry: Intersection, designed to solve the trust deficit in AI-assisted software development for high-integrity systems. Published on GitHub, the tool showcases how deterministic verification methods—such as formal proofs and structural coverage—can validate AI-generated code without requiring exhaustive manual review. This approach aims to lower the economic barrier to building safe, secure software by leveraging AI for speed while maintaining rigorous safety standards.

The Trust Problem in High-Integrity Code

Traditional high-integrity software, found in everything from traffic lights to medical devices, relies on slow, expensive human review to ensure correctness. AdaCore argues that while AI can generate artifacts rapidly, it fails in unpredictable ways that human reviewers cannot easily catch at scale. The current industry standard of reviewing every line of AI output doesn’t play to human strengths or economic realities. GNAT Foundry proposes a shift: use non-AI deterministic tools to guard AI output, allowing humans to focus only on critical artifacts like the Concept of Operations (CONOPS).

Inside the Intersection Demo

The demo uses a four-way traffic intersection with protected left turns and pedestrian crosswalks as a testbed. It includes a full software engineering chain: CONOPS, High-Level Requirements (HLRs), Low-Level Requirements (LLRs), architecture, and implementation. The key innovation is the automated verification workflow. An AI agent is given a scripted change request—adding countdown timers to pedestrian signals—and must update the entire artifact chain. The agent writes new tests, generates proofs using SPARK, and updates the traceability matrix, all while adhering to a rigid workflow defined in demo/demo-prompt.md.

Deterministic Evidence Over Human Guesswork

The system produces an interactive HTML report that visually confirms the trust chain. Green indicators show that compilation checks, SPARK proofs (for runtime error absence and functional correctness), and 100% MC/DC statement coverage are intact. Unlike typical AI coding assistants that leave you guessing about edge cases, GNAT Foundry provides mathematical and structural evidence. The report explicitly flags elements requiring human sign-off, such as the CONOPS root, while automating the verification of code and tests. This creates a 'brownfield' development pattern where AI extends an existing, verified codebase with constrained, provable changes.

Key Takeaways

  • GNAT Foundry uses SPARK and GNAT tools to provide deterministic proof of correctness for AI-generated code.
  • The demo targets 'brownfield' projects, showing how AI can safely modify existing high-integrity systems.
  • A green HTML report serves as the primary artifact for trust, replacing manual line-by-line code review.
  • The toolchain supports both open-source (GNAT FSF) and commercial (GNAT Pro) environments.

The Bottom Line

For developers working in safety-critical environments, this is the first credible workflow that lets AI write code while formal methods write the checks. If AdaCore can make this scale beyond a traffic light demo, it changes the economics of secure software development.