sota.io
2026-06-26·10 min read·sota.io team

Deploy Creusot to Europe — Xavier Denis 🇫🇷 + INRIA Saclay (2021), the EU-Native Deductive Verifier for Rust that Exploits Ownership to Eliminate Aliasing from Proofs, on EU Infrastructure in 2026

Rust's ownership type system guarantees, at compile time, that no two mutable references alias the same memory location. Every Rust programmer knows this property intuitively — the borrow checker enforces it. What fewer people realise is that this property has a profound consequence for formal verification: if mutable aliasing is impossible, then heap reasoning reduces to pure functional reasoning. The central difficulty of deductive verification for C and Java — proving that two pointers do not alias — simply does not arise in safe Rust.

Creusot exploits this observation to build a deductive verifier for Rust that is substantially simpler than equivalent tools for C or Java, and whose proofs are substantially more automatable. It was developed by Xavier Denis 🇫🇷, Claude Marché 🇫🇷, and Jacques-Henri Jourdan 🇫🇷 at INRIA Saclay (Université Paris-Saclay), first published at ATVA 2022. It translates Rust programs to WhyML — the verification language of Why3 — and dispatches the resulting proof obligations to Alt-Ergo 🇫🇷, Z3, and CVC5 via the Why3 infrastructure.

The institutional provenance is entirely French: Xavier Denis is a researcher at INRIA Saclay, Claude Marché co-authored Why3 (with Jean-Christophe Filliâtre) and leads the Toccata research team at INRIA Saclay, and Jacques-Henri Jourdan is a CNRS researcher at LMF (Laboratoire Méthodes Formelles). Creusot extends the EU formal verification stack — Frama-C (C), SPARK Ada (Ada), Creusot (Rust) — all routing through the same Why3 / Alt-Ergo backend, all 100% EU-origin.

The Aliasing Problem in Formal Verification

To understand why Creusot's approach is significant, it is necessary to understand why verifying heap-manipulating programs in C and Java is fundamentally hard.

In C, two pointers p and q may refer to the same memory cell. A Frama-C ACSL precondition like \valid(p) && \valid(q) does not exclude that p == q. This means that writing *p = 1 may change *q, which changes what postconditions about *q mean. Frama-C handles this via separation logic — proving that \separated(p, q) is an additional obligation the verifier must discharge, and WP must track frame conditions (ACSL assigns clauses) to reason about what memory is unchanged after a function call.

In Java, the situation is worse: objects on the heap can be reached by arbitrarily many references, and aliasing is the default. KeY uses Java Dynamic Logic (JavaDL) with heap update terms to reason about aliasing; the proof obligations are considerably more complex.

In safe Rust, the borrow checker statically guarantees that there is at most one mutable reference to any memory location at any point in time. A &mut T reference has exclusive access; no other reference to the same location exists while the &mut T is live. This means:

Creusot's translation to WhyML exploits this: Rust heap cells are modelled as logical values in the WhyML functional language, and the ownership discipline is trusted (the Rust borrow checker has already verified it). The proof obligations that Creusot generates are therefore structurally similar to obligations from functional programs — substantially more amenable to automated SMT solving than the aliasing-heavy obligations from C verification.

Pearlite: Specification Language for Rust

Creusot introduces Pearlite — a specification language embedded in Rust via proc_macro attributes. Pearlite expressions appear in Rust source annotations and are erased at compilation; they exist only for verification purposes.

The core Pearlite annotations:

use creusot_contracts::*;

// Precondition: a is non-negative
// Postcondition: result is non-negative, result * result <= a, (result+1)*(result+1) > a
#[requires(a >= 0u64)]
#[ensures(result * result <= a)]
#[ensures((result + 1) * (result + 1) > a)]
pub fn integer_sqrt(a: u64) -> u64 {
    let mut s = 0u64;
    #[invariant(s * s <= a)]
    while (s + 1) * (s + 1) <= a {
        s += 1;
    }
    s
}

Pearlite's annotations:

The ^ operator (prophecy dereference) is Creusot's most distinctive feature and requires explanation.

Mutable References and Prophecy Variables

Safe Rust's &mut T creates a temporary exclusive borrow: the caller lends exclusive access to a value for the duration of the borrow, and the callee may modify it. When the loan expires, the caller regains access — potentially to a modified value. This creates a verification challenge: how do you specify what the callee does to the mutable reference?

Consider:

#[ensures(*x == old(*x) + 1)]
pub fn increment(x: &mut u64) {
    *x += 1;
}

The postcondition *x == old(*x) + 1 says: after increment returns, the value behind x equals the value it had when increment was called, plus one. old(*x) is the value of *x at function entry (a standard construct in Hoare logic).

For more complex specifications involving what the callee promises about the future state of a mutable reference, Creusot introduces prophecy variables — a concept from the Iris separation logic framework adapted to the non-aliasing Rust setting:

/// Specifies a function that pushes to a Vec and returns a reference to the pushed element
#[requires(v.len() < usize::MAX)]
#[ensures(v.len() == old(v.len()) + 1)]
#[ensures(*result == val)]                  // *result: current value of the returned ref
#[ensures(^result == ^(v)[old(v.len())])]   // ^result: final value = what v will contain at that index
pub fn push_and_get(v: &mut Vec<u64>, val: u64) -> &mut u64 {
    v.push(val);
    &mut v[v.len() - 1]
}

The ^result notation refers to the prophecy — the value that result will point to when the loan expires. Creusot encodes &mut T as a pair (current: T, final: T) in WhyML, where final is a logical variable (a prophecy) constrained by the postcondition. The proof that the function satisfies its specification includes proving that the prophecy is consistent — that there exists a continuation satisfying the stated final value.

In practice, most Pearlite specifications involving &mut T use the simpler *x == ... form; prophecy variables are needed only for functions that return mutable references into borrowed data structures.

Translation to WhyML

Creusot's core operation is a translation from Rust's mid-level intermediate representation (MIR) to WhyML. MIR is Rust's typed control-flow graph, produced after desugaring, type checking, and borrow checking. By translating from MIR rather than Rust surface syntax, Creusot operates on a form of Rust where ownership has already been verified and the borrow structure is explicit.

The translation proceeds:

Rust source (.rs)
    ↓ rustc type checking + borrow checking (safe Rust guarantee)
MIR (Mid-level IR: ownership explicit, lifetimes annotated)
    ↓ Creusot translator (INRIA Saclay 🇫🇷)
WhyML modules (Why3 functional/imperative verification language)
    ↓ Why3 proof session (Jean-Christophe Filliâtre 🇫🇷, INRIA Saclay)
Proof obligations (first-order formulas over program values)
    ↓ Why3 driver dispatch
    ├── Alt-Ergo 🇫🇷 (OCamlPro Paris) — primary: linear arithmetic + UF
    ├── Z3 (Microsoft Research) — fallback: nonlinear + bitvectors
    └── CVC5 (Stanford/NYU) — fallback: quantified obligations
Verified / Unverified (with counterexample generation on failure)

Key translation choices:

Ownership → pure values: Owned values (T by value) are translated directly to WhyML values. No heap modelling required.

Shared references → ghost copies: &T (shared immutable reference) is translated to its dereferenced value — since it cannot be mutated, it is logically equivalent to a copy of the value.

Mutable references → pairs: &mut T is translated to a WhyML record { current: T; final: T } where current is the value at the point of the borrow and final is the prophecy variable. The borrow checker's guarantee that no other mutable reference exists means this pair is the complete model.

Trait impls → WhyML clones: Rust trait implementations generate WhyML clone statements — parameterised modules that provide the required operations. This is how Creusot handles generic Rust code (functions parameterised by trait bounds) — it uses Why3's module system to model Rust's trait system.

Specifying Standard Library Types

A significant portion of Creusot's value is its model of Rust's standard library types — particularly Vec<T>, Option<T>, Result<T, E>, and iterators. These types appear in virtually every Rust program, and verifying code that uses them requires a logical model — a specification of what the type contains, expressible in Pearlite.

Creusot provides #[predicate] and #[logic] annotations for standard library types through a model trait pattern:

use creusot_contracts::*;

// Logical model: Vec<T> as a mathematical sequence
// ShallowModel maps Vec<T> to Seq<T> — Why3's sequence type
impl<T> ShallowModel for Vec<T> {
    type ShallowModelTy = Seq<T>;
    // Axiom: vec.model()[i] == vec[i] for all i < vec.len()
    // Axiom: vec.model().len() == vec.len()
}

// Verified sorting function using the Vec model
#[requires(v@.len() < usize::MAX)]
#[ensures((^v)@.len() == v@.len())]                          // length preserved
#[ensures(forall<i: Int> 0 <= i && i < (^v)@.len() - 1 ==>
    (^v)@[i] <= (^v)@[i + 1])]                               // sorted
#[ensures(exists<p: Permutation> p.is_permutation_of(v@, (^v)@))] // permutation
pub fn insertion_sort(v: &mut Vec<u64>) {
    // ... implementation ...
}

The @ postfix operator is syntactic sugar for .shallow_model() — it extracts the logical model of a concrete type. v@ gives the Seq<u64> model of the Vec<u64>. Proof obligations are then expressed over Seq<u64> — a mathematical sequence with Why3's built-in sequence axioms — rather than over heap cells.

The EU Formal Verification Stack: Now Covering Rust

Before Creusot, the EU deductive verification stack had strong coverage for C (Frama-C) and Ada (SPARK Ada / GNATprove), but no EU-origin verifier for Rust. Creusot closes this gap:

C source with ACSL contracts
    ↓ Frama-C WP (CEA LIST 🇫🇷) → Why3 (INRIA Saclay 🇫🇷) → Alt-Ergo (OCamlPro 🇫🇷)

SPARK Ada with subprogram contracts
    ↓ GNATprove (AdaCore 🇫🇷) → Why3 (INRIA Saclay 🇫🇷) → Alt-Ergo (OCamlPro 🇫🇷)

Safe Rust with Pearlite contracts
    ↓ Creusot (INRIA Saclay 🇫🇷) → Why3 (INRIA Saclay 🇫🇷) → Alt-Ergo (OCamlPro 🇫🇷)

All three pipelines converge on the same Why3 / Alt-Ergo backend. All three are EU-origin. The EU now has a formally verified stack covering the three dominant languages for safety-critical systems software: C (legacy and embedded), Ada (aerospace and defence), and Rust (emerging systems software and new safety-critical projects).

Claude Marché's dual role — co-author of Why3 and supervisor of Xavier Denis (Creusot) — is not coincidental. Creusot was designed from the start as a first-class Why3 frontend, reusing the entire Why3 proof infrastructure (proof sessions, SMT drivers, tactic language, prover portfolio management) for Rust verification.

Industrial Relevance: Rust in Safety-Critical EU Systems

Rust adoption in safety-critical EU contexts is accelerating. Several dynamics drive this:

CISA and EU CRA (Cyber Resilience Act): CISA's 2023 "Memory Safe Roadmap" and the EU's Cyber Resilience Act both identify memory-unsafe languages (C, C++) as a systemic cybersecurity risk. Rust — with its compile-time memory safety guarantees — is explicitly cited as a memory-safe alternative. New EU-regulated products under CRA (IoT devices, industrial control systems, critical infrastructure software) face pressure to adopt memory-safe languages.

Ferrocene (Ferrous Systems 🇩🇪 Berlin): Ferrocene is a qualified Rust compiler for safety-critical systems — IEC 62443, ISO 26262 ASIL D, IEC 62304, DO-178C. Ferrous Systems is a Berlin-based company. Ferrocene provides the ISO 26262 and DO-178C toolchain qualification artefacts (tool qualification document, test results, compiler correctness evidence) that automotive and aerospace customers require before using a compiler in certified production. Ferrocene + Creusot creates the infrastructure for EU-origin formally verified Rust in automotive (ISO 26262) and avionics (DO-178C) contexts.

Rust in Linux kernel: Since 2022, the Linux kernel accepts Rust code. EU infrastructure software (embedded in networking equipment, industrial controllers, medical devices) increasingly runs on Linux kernel Rust drivers. Formal verification of kernel Rust drivers with Creusot is technically feasible.

Aerospace interest: Airbus has published research interest in Rust for new avionics systems. With DO-178C requiring formal verification at Level A, the Creusot → Why3 → Alt-Ergo pipeline — the EU-origin Rust verification stack — is directly relevant to Airbus's future development roadmap.

Institutional Provenance

Xavier Denis 🇫🇷 completed his PhD at Université Paris-Saclay / INRIA Saclay under the supervision of Claude Marché and Jacques-Henri Jourdan, with Creusot as the primary research contribution. He now continues development of Creusot as an INRIA researcher. His work includes the formal treatment of prophecy variables for Rust's mutable references — the key theoretical contribution that makes Creusot's specification language tractable.

Claude Marché 🇫🇷 is Directeur de Recherche at INRIA Saclay, where he leads the Toccata research team. He co-authored Why3 with Jean-Christophe Filliâtre and has been the primary developer of the Frama-C WP plugin. Marché supervised Creusot as a natural extension of the Why3 ecosystem to Rust.

Jacques-Henri Jourdan 🇫🇷 is Chargé de Recherche at CNRS / LMF (Laboratoire Méthodes Formelles, Université Paris-Saclay). His research focuses on separation logic and program verification, particularly the Iris framework used at MPI-SWS — the formal foundation from which Creusot's prophecy variable model is adapted.

INRIA Saclay is a French public research institution — no US Cloud Act jurisdiction, no ITAR encumbrance for aerospace customers processing Creusot verification artefacts on EU infrastructure.

Regulatory Compliance Angles

EU AI Act Art. 9 — Technical Documentation for High-Risk AI Systems

EU AI Act Annex III includes autonomous driving, medical AI, biometric systems, and critical infrastructure AI. Art. 9 requires technical documentation demonstrating system correctness. Creusot-verified Rust components — functions with Pearlite contracts proved via Why3 — provide machine-checked formal correctness evidence: not test results, but mathematical proofs that the code satisfies its specification for all inputs. For Rust-based AI inference engines (LLM runtimes in Rust, ONNX-rs, burn, candle) deployed in Annex III contexts, Creusot verification satisfies the Art. 9 formal documentation requirement.

GDPR Art. 25 — Data Protection by Design

Creusot's Pearlite #[ensures] clauses can express data access constraints analogous to ACSL's assigns \nothing. A Rust function with #[ensures(^output == old(*input))] and no other ^ prophecy constraints on mutable references proves it modifies only its specified output — a machine-checked data minimisation guarantee. For Rust-based GDPR-regulated data processing (health records, financial data), Creusot verification provides the data protection by design evidence that Art. 25 requires.

Cyber Resilience Act — Memory Safety Evidence

The EU Cyber Resilience Act (CRA, effective 2027) requires that products with digital elements implement "state-of-the-art" cybersecurity, including handling of memory safety. Safe Rust eliminates the memory safety vulnerability class (buffer overflows, use-after-free, double-free, null pointer dereference) at the language level. Creusot adds functional correctness verification on top: CRA products implemented in safe Rust and verified with Creusot can demonstrate both memory safety (Rust type system) and functional correctness (Creusot proofs) in their technical documentation.

IEC 62443 — Industrial Control System Security

IEC 62443 security levels for industrial control systems (OT) require security by design. Ferrocene-qualified Rust + Creusot-verified correctness gives EU industrial manufacturers a complete supply chain: qualified compiler, formally verified software, EU-origin toolchain.

Deploy Creusot on sota.io

Creusot requires Rust (stable or nightly, depending on the feature set) and Why3 with Alt-Ergo:

# Install Why3 and Alt-Ergo (Ubuntu/Debian)
sudo apt-get install why3 alt-ergo

# Install Why3's prover detection
why3 config detect
# Detects: Alt-Ergo x.x, Z3 x.x, CVC5 x.x

# Install Creusot via cargo
cargo install cargo-creusot

# Verify Creusot sees Why3 and Alt-Ergo
cargo creusot setup --check
# OK: why3 x.x detected, alt-ergo x.x detected

Annotating a Rust project with Creusot:

# Cargo.toml
[dependencies]
creusot-contracts = { git = "https://github.com/creusot-rs/creusot" }

Running verification:

# Verify the current Rust crate with Creusot
cargo creusot verify

# Output: proof obligations per function
# ✓ integer_sqrt — 3 obligations proved (Alt-Ergo, 0.12s)
# ✓ insertion_sort — 7 obligations proved (Alt-Ergo + Z3, 0.84s)
# ✗ binary_search — 2 obligations unproved (timeout: increase with --timeout)

sota.io Dockerfile for a Creusot verification CI pipeline:

FROM sotaio/builder:ubuntu-24.04

# Install Why3 backend tools (EU formal verification stack)
RUN apt-get update && apt-get install -y \
    why3 \
    alt-ergo \
    z3 \
    && rm -rf /var/lib/apt/lists/*

# Configure Why3 with detected provers
RUN why3 config detect

# Install Rust (stable)
RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
ENV PATH="/root/.cargo/bin:${PATH}"

# Install cargo-creusot
RUN cargo install cargo-creusot

WORKDIR /verification

COPY . .

# Run Creusot verification
RUN cargo creusot verify \
    --output-format json \
    --timeout 60 \
    > verification-report.json

# Inspect results
RUN cat verification-report.json | python3 -c "
import json, sys
report = json.load(sys.stdin)
proved = sum(1 for r in report['results'] if r['status'] == 'proved')
total = len(report['results'])
print(f'Creusot: {proved}/{total} obligations proved')
if proved < total:
    sys.exit(1)
"

sota.io manages the Linux environment — OCaml runtime for Alt-Ergo, Z3 binary, Rust toolchain isolation between builds — so the verification pipeline runs without DevOps overhead. The free tier (512 MB memory) supports Creusot verification of typical Rust crates (5,000–50,000 LOC). Larger codebases scale on the standard tier.

Creusot vs. Other Rust Verifiers

Prusti (ETH Zurich 🇨🇭): Also a deductive Rust verifier, uses the Viper intermediate verification language (also from ETH Zurich), which dispatches to Z3. Prusti is Swiss-origin — EU but not EU-mainland French-origin. Creusot uses Why3/Alt-Ergo — the same French formal methods stack as Frama-C and SPARK Ada. For organisations that want a uniform EU formal methods toolchain, Creusot provides better integration with the existing Frama-C / SPARK / Why3 ecosystem.

Verus (Carnegie Mellon, US): SMT-based Rust verifier, uses Z3. US-origin — ITAR and Cloud Act considerations apply.

Kani (Amazon Web Services, US): Model-checking approach for Rust, uses CBMC (bounded model checker). US-origin.

RustBelt (MPI-SWS 🇩🇪): Semantic model of Rust's type system in Iris, mechanised in Coq/Rocq. Foundation-level research, not a verification tool for Rust programs.

Creusot's position: EU-origin, deductive (strongest guarantees), Why3 integration (reuses the entire EU Why3 ecosystem), prophecy variables for mutable references (theoretically clean), Alt-Ergo as primary prover (100% EU backend).

See Also