Agentic AI workflows to build high-integrity software backed by formal methods

Agentic AI workflows are accelerating software development in the enterprise world. Engineers drive the software development process by interacting with AI agents as they produce requirements, code, and test cases. The agentic system iterates over the code till it passes some metric of ‘good enough’, typically defined by test cases passing, maybe static analysis, or coding standard review, and the code is merged. The final code is often not even reviewed before it is merged into the main branch.

This may be fine for enterprise, but it is not fine for high-integrity software.

The premise is wrong from 3 key perspectives: 
1) The implementation technologies are dangerous. Whether it is TypeScript, C, C++, or even Rust, unexpected failures can happen, and the workflows are not set up to prevent it; 
2) Failure detection happens during the test phase of the deployment process. This is too late, agentic systems thrive when they can detect failure early.
3) Traceability and accountability are typically missing, or at least ill-defined

This presentation will document a workflow, using open-source technology to drive an agentic AI workflow for high-integrity software, backed by formal methods, using Ada SPARK. 

The workflow starts at a high level, with numbered requirements managed by an AI agent. The agent translates these requirements into SPARK code while maintaining traceability and refines it until it passes SPARK Silver, statically demonstrating the absence of runtime errors. Another agent generates test cases and manages them to achieve sufficient code coverage by executing them in an emulated embedded environment while collecting evidence. The environment can be executed by the agent on the developer workstation or in a CI/CD pipeline. Accountability is provided by the MR/PR review process.

The combination of requirements, their linking to code and test cases, and the CI/CD platform establishes a continuous traceability chain with accountability that satisfies the needs of high-integrity systems.

Speaker

Mark Hermeling

Head of Technical Marketing, AdaCore

Mark Hermeling (MSc) has over 25 years of experience in software development tooling, operating systems, virtualization and networking technology in high-integrity, safe and secure, embedded and real-time systems. He has worked on projects building automotive, networking, aerospace and defense and industrial devices in North America, Europe and Asia.

As Head of Technical Marketing at AdaCore he drives the narrative that crosses the chasm between technical capabilities and business value. Mark is a frequent author and speaker on topics ranging from the software development lifecycle, DevSecOps to formal methods and software verification.

Prior to joining AdaCore, Mark worked for CodeSecure (formerly GrammaTech), Wind River Systems, Zeligsoft and IBM Rational. He holds a Master of Science degree in Computing Science from Eindhoven University of Technology.