Using AI and formal methods to build software

Executives deciding how to introduce AI across high-integrity software programs need an adoption strategy that increases delivery capacity while retaining human accountability and controlling risk. AI can accelerate software production, but the organization must also build confidence in that software at the same pace. Formal methods provide that confidence. A faster implementation has limited business value if verification becomes the new bottleneck or if uncertainty moves downstream into integration and certification; formal methods remove this bottleneck using mathematical proofs. This is especially important when the software needs to satisfy functional safety requirements such as DO-178C, ISO 26262, IEC 61508, or security standards such as ISO 21434, and many others.

AdaCore’s approach is to combine AI-assisted development with tools that independently check the resulting artifacts. AI can propose requirements, write code, and help construct tests and formal contracts. Deterministic tools such as compilers, verification tools, and traceability checks then provide evidence about those outputs. Engineers can review those outputs and remain accountable for the requirements and the decisions that determine what the system must do.

This is the basis for deterministic trust: deterministic acceptance rests on explicit checks and evidence about specified properties, rather than on how convincing an AI-generated explanation sounds. The opportunity is to increase development capacity while retaining an engineering basis for release decisions.

The constraint is verification capacity.

High-integrity development already assumes that people make mistakes. Teams use requirements reviews, coding rules, analysis, testing, and rigorous verification to detect those mistakes before they affect a delivered system. Introducing AI changes the volume and pace of the work passing through that process.

An agent can update a collection of requirements, implementation files, and tests in a single session. Reviewing every generated line manually can consume the capacity that the organization hoped to gain. Asking another model to review the output may be useful, but it does not provide the same assurance as checking the implementation against an explicit property using deterministic tools. Deterministic tools can be qualified against safety standards, which means engineers understand how they work and how to interpret their outputs.

The executive decision is therefore broader than selecting a coding assistant. It includes investing in a verification process that scales with the output of these assistants and integrates human- and agent-created artifacts. Measures such as accepted changes, unresolved verification obligations, review effort, and time to a verified baseline are more informative than the volume of code produced.

What deterministic trust establishes

A compiler checks language rules. A test observes behavior for particular inputs and conditions. Coverage analysis measures which parts of the implementation those tests exercised. Formal verification can establish that an implementation satisfies specified properties across the inputs and states covered by the proof assumptions.

The formal verification here is crucial as it satisfies two important aspects. First, it verifies rules against all possible execution paths through the source code. Second, it can do this during build time, no need to run exhaustive tests. The formal verification provides an ‘oracle’ for the agent. A way to, cheaply and quickly, verify the generated output. The use of formal methods improves the speed and quality of the work that AI agents deliver (https://www.anthropic.com/research/formal-verification).

These forms of evidence answer different questions. They become useful together when a team can connect them to reviewed requirements and identify where a claim still depends on human judgment. That traceability is another key aspect. Correct code is important, but that code needs to be connected to a requirement; otherwise, it has no place in the project. Conversely, all project requirements need representation in the code and tests.

The programming language SPARK provides a particularly useful foundation for this formal approach. SPARK is a subset of Ada; it restricts some of Ada’s constructs (such as requiring that pointers follow an ownership model similar to that of Rust) and allows the human or AI programmer to express formal contracts in the source code. These contracts use the Ada syntax, which is easy to read and comprehend, and describe pre-conditions, post-conditions, and invariants, among others. The SPARK tool is a formal-methods prover that runs before the compiler and can prove two distinct sets of properties. First, it can prove the absence of runtime errors, no more crashes or corrupted memory; secondly, it can prove functional safety properties.

The scope matters. A proof of a contract does not establish that the contract captures every stakeholder need. An implementation can satisfy an incomplete specification. Engineers must review the requirements, assumptions, and boundaries between verified software and its environment, and assess the traceability between them. Deterministic trust is strongest when those boundaries are visible and explicit.

A practical example from an intersection controller

The accompanying presentation discusses GNAT Foundry: Intersection as a demonstration project to make this workflow concrete. The demonstrator models a four-way traffic intersection with protected left turns and pedestrian crossings. It provides a familiar way to examine a demanding requirement: vehicle and pedestrian movements that conflict must not be permitted together.

The project connects a concept of operations to high-level requirements, low-level requirements, implementation, and verification artifacts. The project also includes a description of a set of agents, a workflow for their collaboration, and instructions on how to use deterministic tools to verify their work. Any change must propagate through that chain. The agent’s assignment includes updating the evidence needed to support the change and providing instructions on how to communicate with the engineering team to clarify objectives when needed.

The important management outcome is the ability to inspect that chain. A verification report brings together traceability, test results, coverage, and proof results. Engineers can investigate a missing link or an unproven property rather than treating an apparently plausible implementation as sufficient evidence.

This remains a demonstrator. The published repository explicitly states that it is not intended for public roads and is not certified to a safety standard. Its value is in showing an inspectable workflow that teams can evaluate against their own engineering constraints.

How AdaCore tools contribute

The tools provide deterministic checks around AI-generated work. The GNAT compiler checks the implementation against Ada’s language rules. SPARK discharges proof obligations for the properties expressed in the program. These checks can also give an agent concrete feedback as it revises an implementation.

Dynamic verification addresses execution behavior. GNATtest supplies unit-test harnesses and skeletons, while GNATcoverage measures structural coverage, including modified condition/decision coverage. These capabilities are available within the GNAT Dynamic Analysis Suite. Passing tests and achieving a coverage target remain distinct from proving a requirement.

In the demonstrator, traceability checks connect the artifacts and help reveal missing evidence. Those checks are part of the project’s workflow; their presence does not mean a general-purpose tool can decide whether every natural-language requirement is correct. Human review establishes the intended meaning at the root of the process.

For an organization, the commercial toolchain and support relationship also matter. A successful experiment must become a maintainable engineering capability across the targets and environments the business uses. GNAT Pro provides development toolchains, and AdaCore’s support and assurance offerings offer options for projects that require continuity over long lifecycles. The appropriate platform, support, and qualification arrangements must be selected for the project.

The business benefit is a more controlled path to delivery.

This approach can help teams identify defects and inconsistencies in assumptions while a change is still being developed. A failed proof or a broken traceability link creates a specific task to resolve. That feedback can reduce the amount of uncertainty carried into later stages, although the actual effect on cost and schedule must be measured in the customer’s environment.

It can also focus scarce engineering expertise. Experienced reviewers focus on intended behavior, architecture, assumptions, and exceptions that require judgment. Automated checks handle repeatable obligations and preserve their results for review. The engineer’s accountability remains, supported by a clearer evidence trail.

At division level, a common acceptance policy can make AI adoption more consistent across teams. Different projects may use different models while following the same rules for requirements review, independent verification, and release evidence. This gives leaders a way to govern the adoption of a changing technology without making confidence depend entirely on one model’s behavior.

There is a further opportunity in the economics of formal methods. AI can assist with the contracts, annotations, and revisions that proof requires. If that assistance lowers the effort needed to obtain useful proofs, teams may be able to apply stronger verification more widely. That is a proposition to evaluate on representative software, rather than a universal productivity guarantee.

Start with a measurable proof of concept.

A useful pilot starts with a bounded component, reviewed requirements, and a known baseline. Define the properties to verify, the evidence required for acceptance, and the decisions reserved for engineers. Apply an AI-assisted change and measure the full effort needed to restore a verified baseline, including review and rework.

GNAT Foundry Intersection provides an open starting point for an executive briefing with AdaCore and your engineering and assurance leaders. Use that discussion to select a representative program, agree the acceptance evidence and success measures, and decide what results would justify a wider rollout. The decision should rest on demonstrated delivery capacity and a verification process your teams can sustain.