AdaCore GNAT Foundry puts AI code through formal proof

AdaCore released GNAT Foundry: Intersection, an open-source demonstrator that runs AI-generated changes to high-integrity software through SPARK formal proof, requirements-based tests and coverage analysis. The baseline traffic-light controller reaches 100% MC/DC and statement coverage, and applying a change request with frontier models takes about two hours and costs roughly $50.

• Demonstrator is available in a public GitHub repository
• Baseline traffic-light controller hits 100% MC/DC and statement coverage
• AI-driven change request takes ~2 hours and costs ~$50
• Claude Code and Codex are supported; workflow is agent-neutral