AdaCore выпустила GNAT Foundry для формальной проверки ИИ-кода

AdaCore представила открытый демонстратор GNAT Foundry: Intersection, который прогоняет изменения ИИ-агента в высоконадёжном ПО через формальные доказательства SPARK, тесты по требованиям и анализ покрытия. Базовый проект — светофор с защищёнными поворотами — даёт 100% MC/DC и statement coverage; прогон изменения с frontier-моделями занимает около двух часов и стоит примерно $50.

• Демонстратор доступен в открытом репозитории на GitHub
• Базовый светофор достигает 100% MC/DC и statement coverage
• Прогон изменения ИИ-агентом занимает ~2 часа и стоит ~$50
• Поддерживаются Claude Code и Codex, workflow не привязан к модели