Guarding AI with Deterministic Trust

From medical devices and automotive systems to traffic control networks, high-integrity software quietly underpins modern infrastructure. Achieving absolute software integrity demands exhaustive manual verification, driving engineering costs to unsustainable levels. This economic friction creates an operational bottleneck: the market demands safer software, yet traditional deployment methodologies remain cost-prohibitive. Artificial intelligence (AI) allows software development teams to deliver reliable yet economical code by accelerating code generation. However, AI’s non-deterministic nature presents a fundamental barrier: trust.

Mitigating this trust barrier has historically relied on manual human review of all AI outputs. However, human auditing simply cannot scale alongside the velocity of generative pipelines, bottlenecking development. To utilize AI safely in safety-critical domains, engineering frameworks must pivot toward deterministic guarding mechanisms by introducing automated, mathematical validation tools to enforce strict architectural and structural limits on AI-generated artifacts.

The open-source project GNAT Foundry: Intersection provides a concrete blueprint for this hybrid pipeline. By modeling a complex traffic infrastructure layout, the project demonstrates how deterministic toolchains can independently establish structural and functional safety, providing mathematical verification of AI-authored code without scaling manual oversight.

Trusting AI-Authored Code

Integrating artificial intelligence into high-integrity software development introduces two systemic engineering challenges:

• Unpredictable Failure Modes: AI agents fail in non-human, asymmetric patterns that are difficult to anticipate, making continuous human accountability over AI-authored artifacts mandatory.

• Reviewer Cognitive Overload: The velocity of AI generation easily outpaces human auditing capacity, requiring automated, deterministic safeguards to validate output integrity at scale.

While human oversight remains the baseline for legal and operational accountability, relying exclusively on manual code audits introduces an operational bottleneck that fails to leverage human cognitive strengths. Traditional verification paradigms cannot absorb the volume of code generated by automated pipelines.

The architecture modeled in GNAT Foundry addresses this imbalance by shifting the burden of verification onto non-AI deterministic tools. This framework confines the AI agent's output within strict mathematical and algorithmic boundaries, allowing human engineers to focus exclusively on high-level conceptual validation.

Historically, safety-critical software engineering has relied on strongly typed languages like Ada and its formally verifiable subset, SPARK, alongside validation tooling such as GNATprove, GNAT DAS, and CodeSonar to establish absolute mathematical certainty. The current shift lies in adapting these classic deterministic ecosystems to act as automated verification gates, validating AI-generated software pipelines at machine speed.

The Intersection Demo

To evaluate the viability of deterministic AI guarding, the framework utilizes a model of a four-way traffic intersection featuring protected left turns and demand-led pedestrian crosswalks. This layout introduces enough concurrent state variables to simulate real-world safety-critical constraints:

• Vehicle Detection: Left-turn signals are demand-driven and trigger only upon vehicle presence.

• Pedestrian Actuation: Crosswalk signals activate exclusively via call-button input.

• State Indication: Actuated pedestrian call lights illuminate upon registration and clear when the walk signal initiates.

• Dynamic Displays: Pedestrian control heads suppress countdown timers during active flashing "DON'T WALK" cycles.

System Architecture & Artifact Hierarchy

The baseline demonstration constructs a rigorous, vertically integrated engineering stack derived from the US Department of Transportation Manual on Uniform Traffic Control Devices. This baseline serves as the formal boundary that constrains AI modification requests.

• Execution Environments: The core software implementation is written in Ada/SPARK and compiles natively for Linux simulation harnesses, or directly onto bare-metal ARM 32-bit microcontrollers (with or without an RTOS).

• Deterministic Verification Layers: Rather than relying on human evaluation to confirm that the code matches the Low-Level Requirements (LLRs), the platform deploys a multi-tiered verification stack:

  • SPARK Silver Level: Automated mathematical proofs establishing the complete absence of runtime errors (preventing undefined behaviors, overflows, and out-of-bounds access).

  • SPARK Gold Level: Formal proofs of functional correctness verifying that the implementation complies exactly with formal specifications.

  • Compile-Time Enforcement: Strict static type-safety checks enforced natively by the Ada compiler.

  • Dynamic Analysis: Requirements-based testing frameworks engineered to yield 100% Modified Condition/Decision Coverage (MC/DC) and statement coverage.

Traceability Matrix

The cornerstone of this architecture is an interactive HTML traceability matrix that maps the complete chain of custody from the root Concept of Operations (CONOPS) down to individual lines of code and proof obligations.

By automating the generation of this evidence, the system isolates exactly where human authority is required, explicitly restricting manual sign-offs to:

1. The CONOPS (serving as the foundational root of the chain of trust).

2. Operational CONOPS elements not traced directly to software execution.

3. Derived architectural requirements within the HLRs.

Every subsequent downstream artifact—including code generation, test compliance, and proof coverage—is validated automatically by the toolchain, eliminating the need for human code-auditing loops.

Executing the Change-Request Workflow

The GNAT Foundry: Intersection repository provides a pre-configured, automated sandbox designed to evaluate AI capabilities under rigorous engineering constraints. Out of the box, the framework establishes a fully validated, stable baseline.

The environment can be initialized and evaluated natively on Linux through the following sequence:

# Step 1: Initialize the toolchain (FSF Open-Source or Pro tools)
make setup-community  # Alternative: make setup-pro

# Step 2: Execute the real-time intersection graphical simulation
make run-native

# Step 3: Compile and generate the comprehensive verification report 
make report

To simulate a real-world engineering pipeline, the demo includes an automated change request scenario located in demo/demo-prompt.md. This workflow tasks a downstream AI agent with adding countdown timers to the pedestrian control units.

Upon execution, the AI agent applies a pre-approved patch to the root CONOPS and initiates a multi-tier pipeline. The agent autonomously updates HLRs, refactors the underlying Ada SPARK implementation, generates new requirements-based test scripts, and re-runs the entire mathematical verification stack without human intervention.

Quantifying Certainty: The Deterministic Evidence Layer

The core architectural thesis of the GNAT Foundry framework is that code-level verification should rely on mathematical and algorithmic certainty rather than subjective human inspections. When the AI agent completes an engineering modification, the system generates a definitive verification report.

Trust in the modified system is established across four distinct deterministic gates:

• Compilation Defensibility: The GNAT compiler verifies type-safety and validates localized, compile-time contract checks embedded within the source architecture.

• Mathematical Proof: The SPARK analysis engine mathematically proves the absolute absence of runtime errors (SPARK Silver) and verifies compliance with functional correctness contracts (SPARK Gold).

• Requirements Compliance: Automated test execution via GNAT Test ensures that all requirements-based functional tests achieve a passing state.

• Structural Coverage Validation: GNAT Coverage performs dynamic analysis during test execution, ensuring the modified code achieves 100% statement and Modified Condition/Decision Coverage (MC/DC).

Architectural Context: Brownfield vs. Greenfield Deployment

The GNAT Foundry: Intersection project specifically models a brownfield development pipeline. The AI agent is injected into a mature ecosystem with an established, rigid chain of deterministic evidence. This represents the most common enterprise use case: engineering teams seeking to accelerate legacy system iterations without compromising historical safety metrics. Under these constraints, the pre-existing verification framework limits the AI’s decision-making freedom, preventing unverified regressions.

However, the underlying workflow scales identically to greenfield projects. In new development lifecycles, the automated verification toolchain enforces safety metrics from day one, guiding the AI agent through the synthesis of clean-sheet artifacts—from initial CONOPS definition down to hardware-targeted test execution.

Algorithmic Verification as the Future of Safety-Critical Pipelines

Shifting the burden of proof from human code review to automated validation engines solves the fundamental scaling problem of generative AI in critical systems. By wrapping non-deterministic agents in rigid mathematical guards, engineering organizations can safely capture the velocity benefits of AI. GNAT Foundry demonstrates that development speed and high-integrity software compliance are no longer mutually exclusive paradigms.

Learn more about AdaCore’s integrated tools and expert services for high-integrity software.