Developing High-Integrity Software with AI
AI can write code faster than your team can review it. In high-integrity software, that’s a problem, not a win. This talk shows how to close the gap.
Mark Hermeling shows how to pair AI-assisted development with formal methods, so you get AI’s speed without giving up the assurance safety-critical software needs.
The idea is simple: AI writes the requirements, code, tests and contracts. SPARK and GNAT prove they’re correct.
The second half is a walkthrough of GNAT Foundry Intersection, an open-source demonstrator where AI agents take a project from concept to verified code, with full traceability and a report the engineer signs off.
What you’ll learn:
- Why high-integrity teams are investigating AI now
- The real concerns: safety, review capacity, cost, continued access
- How formal methods and SPARK turn AI output into verified code
- The GNAT Foundry Intersection agent workflow and deterministic guardrails
- How to try the demonstrator in your own environment
- What a 40% reduction in development cost could mean for your programme
Author
Mark Hermeling
Mark has over 25 years’ experience in software development tools for high-integrity, secure, embedded and real-time systems across automotive, aerospace, defence and industrial domains. As Head of Technical Marketing at AdaCore, he links technical capabilities to business value and is a regular author and speaker on on topics ranging from the software development lifecycle, DevSecOps to formal methods and software verification.
