EU AI Act Compliant Deployment 2026: Formal Verification for High-Risk AI Systems

On August 2, 2026, the bulk of the EU AI Act applies. High-risk AI systems under Annex III — CV-screening tools, creditworthiness assessors, biometric categorisation systems, safety components in critical infrastructure — must comply with Articles 9 through 15. Article 9 is the centrepiece: a mandatory risk management system that identifies and mitigates "foreseeable risks."

Most compliance teams are responding with documentation. Risk registers, policy documents, audit trails, governance frameworks. These satisfy the letter of compliance in the near term. They do not provide the machine-checked guarantees that Article 9's language implies — and that regulators will increasingly expect as enforcement matures.

There is a complementary approach: formal verification. It is not new. The EU formal methods community — INRIA, ETH Zurich, TU Munich, KU Leuven, Freiburg — has been developing it for forty years. What is new is that the EU AI Act creates a legal context in which machine-checked proofs of safety properties become compliance artefacts with regulatory weight.

What Article 9 Actually Requires

Article 9(4) of the EU AI Act requires providers of high-risk AI systems to identify "reasonably foreseeable misuse" and "foreseeable risks." Article 9(5) requires the risk management system to consider "the risks arising from reasonably foreseeable use."

The phrase "foreseeable risks" is legally significant. It does not mean "risks that occurred." It means risks that a competent developer could have anticipated from the system's design — including edge cases, distribution shift, adversarial inputs, and failure modes under composition with other systems.

Traditional testing demonstrates that specific test cases pass. It does not demonstrate that properties hold universally. Formal verification does. A verified property holds for all inputs within the specified domain, not just for the test set. That is the difference between "we tested this" and "this has been proven."

Under Article 9, the distinction matters. A risk management system that documents risk identification without providing evidence of mitigation for all foreseeable cases is a weaker compliance position than one backed by formal proof.

The Formal Verification Stack for EU AI Act Compliance

Several formal verification tools map directly to EU AI Act compliance requirements for high-risk AI systems. Each addresses a different aspect of Article 9's foreseeable risk mandate.

LiquidHaskell: Refinement Types as Executable Specifications

LiquidHaskell (Ranjit Jhala, UC San Diego; now Niki Vazou GR, IMDEA Madrid ES) extends Haskell's type system with refinement types — type annotations that constrain values with logical predicates. These annotations are verified automatically by SMT solvers (Z3, CVC5).

{-@ type Prob = { v:Double | 0.0 <= v && v <= 1.0 } @-}
{-@ type Confidence = { v:Double | 0.0 <= v && v <= 1.0 } @-}

{-@ classifyRisk :: Prob -> Confidence -> { v:Double | 0.0 <= v && v <= 1.0 } @-}
classifyRisk :: Double -> Double -> Double
classifyRisk prob conf = prob * conf

The annotation { v:Double | 0.0 <= v && v <= 1.0 } is not a comment. It is a machine-checked specification. If classifyRisk can return a value outside [0,1] — through overflow, underflow, or logic error — LiquidHaskell's type checker rejects the program at compile time. The proof obligation is discharged by the SMT solver before the code runs.

For EU AI Act Article 9 compliance, this means: probabilistic outputs from classification systems can be proven to lie within their declared range. Risk scores can be proven to be monotonic. Confidence intervals can be proven to be well-formed. These properties, verified at compile time, constitute formal evidence that the foreseeable risk of out-of-range outputs has been addressed.

Vazou is affiliated with IMDEA Madrid ES — a Spanish public research institute. LiquidHaskell is MIT-licensed. No CLOUD Act exposure.

Agda and Idris: Dependent Types as Correctness Proofs

Agda (Ulf Norell SE, Chalmers University, Gothenburg) and Idris (Edwin Brady GB, University of St Andrews) are dependently-typed programming languages in which programs and proofs are unified. A type can express not just "this is a list" but "this is a sorted list of length n" or "this function terminates for all inputs in the natural numbers."

data SortedList : List ℕ → Set where
  []    : SortedList []
  [_]   : (n : ℕ) → SortedList (n ∷ [])
  _∷_p_ : (n : ℕ) {xs : List ℕ}
         → SortedList xs
         → (∀ m → m ∈ xs → n ≤ m)
         → SortedList (n ∷ xs)

The type SortedList xs is not a runtime assertion. It is a compile-time proof that xs is sorted. Functions that accept SortedList arguments cannot be called with unsorted data — the type system enforces the invariant universally.

For high-risk AI ranking systems — loan applicant ranking, job candidate ordering, credit risk scoring — dependent types allow developers to prove that ranking functions preserve specified fairness properties. A property like "no candidate with protected attribute X is systematically ranked below candidates with lower objective scores" can be expressed as a type and proven machine-checkable.

Agda is developed at Chalmers SE (Gothenburg). Idris is developed at the University of St Andrews GB. Both are free and open source. Neither has US corporate governance.

Rust and Prusti: Ownership Proofs for Safety-Critical AI Infrastructure

Rust's type system provides memory safety guarantees — no buffer overflows, no use-after-free, no data races — by construction. These are not runtime checks. They are compile-time proofs enforced by the ownership and borrow checker. The Rust compiler is a theorem prover for memory safety.

Prusti (Peter Müller CH + Malte Schwerhoff DE + Alexander Summers CH, ETH Zurich, 2016) extends Rust with full functional correctness verification using the Viper intermediate verification language and the Z3 SMT solver.

use prusti_contracts::*;

#[requires(0.0 <= score && score <= 1.0)]
#[requires(0.0 <= threshold && threshold <= 1.0)]
#[ensures(result == (score >= threshold))]
fn classify(score: f64, threshold: f64) -> bool {
    score >= threshold
}

The #[requires] and #[ensures] annotations are Prusti specifications. The compiler verifies that the implementation satisfies the contract for all inputs satisfying the preconditions. A post-condition is proven to hold — not tested, proven.

For EU AI Act Article 9, Prusti-verified Rust provides a deployment stack where safety-critical inference code carries machine-checked proofs of its specified behaviour. ETH Zurich is a Swiss federal university. Switzerland is an EU associate, subject to GDPR via the Swiss Federal Act on Data Protection. No CLOUD Act exposure.

Isabelle/HOL and Rocq: Full Formal Proof for Annex III Systems

For the highest-risk categories under Annex III — biometric identification, critical infrastructure safety components, law enforcement AI — interactive theorem provers provide the strongest formal guarantees available.

Isabelle/HOL (Lawrence Paulson GB, Cambridge; Tobias Nipkow DE, TU Munich; Makarius Wenzel DE) is an interactive theorem prover in which complex system properties can be stated and proven using higher-order logic. The Isabelle Archive of Formal Proofs contains over 700 verified mathematical theories.

Rocq (formerly Coq; Pierre-Yves Strub FR, Thierry Coquand SE/FR, Hugo Herbelin FR, INRIA Paris) provides a constructive proof assistant where proofs are executable programs. The Curry-Howard correspondence means a Rocq proof of "function f satisfies property P" is simultaneously a certified program and a mathematical proof.

CompCert — the formally verified C compiler (Xavier Leroy FR, INRIA Paris, Collège de France) — uses Rocq to prove that compiler transformations preserve program semantics. The same infrastructure that verifies compiler correctness can verify AI system properties. INRIA is a French public research institution under the Ministry of Research. Rocq is developed and maintained entirely within EU academic institutions.

The Deployment Dimension: Why EU-Native Infrastructure Matters

Formal verification addresses the software-level compliance requirements of Article 9. The deployment context introduces additional requirements that formal verification alone does not address.

Article 9(4)'s "foreseeable risks" include data protection risks. Under the CLOUD Act (2018), US law enforcement can compel US cloud providers to produce data stored anywhere in the world. AWS Frankfurt, Azure Netherlands, and Google Cloud Frankfurt are operated by US-incorporated entities. A warrant served on Amazon Web Services, Inc. is legally effective against all AWS infrastructure globally, including EU datacenters.

For high-risk AI systems under the EU AI Act, the foreseeable risk of unauthorised data disclosure under US law is non-trivial. Model weights represent trained intellectual property. Inference inputs may contain personal data subject to GDPR. Audit logs required by Article 12 constitute personal data records. If these are stored or processed on US-incorporated cloud infrastructure, the risk of CLOUD Act compulsion is foreseeable — and therefore must appear in the Article 9 risk management system.

EU-native deployment on infrastructure incorporated under EU law — no US parent company, no CLOUD Act exposure — addresses this risk at the infrastructure layer. When the AI system's formal verification proofs, model weights, inference pipeline, and audit logs all reside on EU-native compute, the foreseeable risk of cross-border disclosure is eliminated by architecture rather than addressed in documentation.

The August 2026 Timeline

The EU AI Act's high-risk AI provisions under Article 9 apply from August 2, 2026. Notified bodies are already preparing EU AI Act conformity assessments. Providers of CV-screening tools, creditworthiness systems, biometric categorisation systems, and safety-critical infrastructure components are working through compliance now.

The formal verification toolchain requires lead time. Integrating LiquidHaskell type annotations into an existing codebase, writing Prusti specifications for Rust inference code, or developing an Isabelle/Rocq proof of a key safety property takes weeks of engineering work, not hours. Teams that start in Q2 2026 have time to integrate formal evidence before the August deadline. Teams that start in July do not.

The INRIA ecosystem — Rocq, Why3 (Jean-Christophe Filliâtre FR, INRIA Saclay), Alt-Ergo (CNRS/Université Paris-Saclay FR), Frama-C (CEA-List / INRIA Paris) — provides a complete EU-native formal verification stack for C, OCaml, and interoperating languages. The ETH Zurich ecosystem provides Prusti and the Viper framework for Rust, Java, and Python. These are not exotic research tools; they are production-grade verifiers with industrial deployment histories in aerospace, automotive, and critical infrastructure.

From Documentation to Proof

EU AI Act compliance for high-risk AI systems will stratify into two tiers over the next three years: providers who document compliance and providers who prove it.

Documentation-based compliance satisfies current regulatory requirements. As the European AI Office and national supervisory authorities develop enforcement practice and notified body assessment criteria, the distinction between "we identified this risk and wrote it in our register" and "we identified this risk and proved it cannot occur" will become material.

Formal verification gives developers and organisations the ability to move from the first tier to the second. The tools are mature, the EU research community that builds them is active, and the legal framework that creates demand for them is now in force.

The foreseeable risk that Article 9 asks you to manage — build proof that it cannot occur.

sota.io deploys your containers on EU-incorporated infrastructure in Germany. Model weights, inference pipelines, audit logs, and formal verification artefacts stay under EU jurisdiction — no CLOUD Act exposure. Compliant with GDPR, EU AI Act Article 9 risk management requirements, and the coming CADA sovereign infrastructure standard. Free tier available.