Why3: The EU-Native Proof Management Framework Behind Frama-C, SPARK Ada, EasyCrypt, and Creusot

Why3 is not a tool you interact with directly. It is the proof management layer that makes every major EU formal verification tool produce machine-checkable results. When Frama-C WP verifies that your C code has no runtime errors, it is Why3 doing the proof work. When GNATprove verifies a SPARK Ada procedure's postcondition, it compiles to Why3's intermediate language. When EasyCrypt produces a game-based cryptographic proof of ML-KEM, the non-probabilistic obligations go through Why3. When Creusot verifies Rust code, it compiles Rust MIR to WhyML — Why3's intermediate language.

Why3 is the connective tissue of the European formal methods stack. And it is 100% EU-native.

Developed by: Jean-Christophe Filliâtre and Claude Marché at INRIA Saclay — Île-de-France (Université Paris-Saclay), with Andrei Paskevich. First published at ESOP 2011 as "Why3: Shepherd Your Herd of Provers". The name reflects its core design: managing a herd of different provers — Alt-Ergo, Z3, CVC5, Coq, Isabelle — dispatching each proof obligation to the prover most likely to solve it.

What Why3 Provides

Why3 has three components:

WhyML — the intermediate verification language. WhyML is a typed ML-like language with logical annotations. It has algebraic data types, pattern matching, quantifiers (forall, exists), ghost variables (logical witnesses not in compiled output), mutable references with region-based aliasing, and refinement types. Frama-C, GNATprove, EasyCrypt, and Creusot all compile to WhyML as their first step. WhyML is the common denominator of the EU formal verification ecosystem.

Proof obligation generator. Why3 takes a WhyML program with pre/post-conditions and loop invariants, applies a weakest precondition (WP) calculus, and produces a set of verification conditions (VCs) — first-order logic formulas that must be true for the annotated properties to hold.

Multi-prover dispatcher. Why3 sends each VC to one or more provers in parallel: Alt-Ergo (default for EU work), Z3, CVC5, CVC4, Eprover, Vampire, Coq/Rocq, and Isabelle/HOL. If one prover times out or fails, another takes it. Results are cached in a why3session.xml file, so re-running Why3 reuses proofs already discharged. This is essential for CI pipelines: only newly added or changed obligations require fresh solver calls.

The EU-Native Solver Chain

Why3's multi-prover architecture is the critical architectural decision for EU compliance. The choice of solver determines the jurisdiction of your proof chain.

Alt-Ergo — developed by Sylvain Conchon and Évelyne Contejean at CNRS/LRI Orsay (now Université Paris-Saclay), currently maintained by OCamlPro (Paris, France). Alt-Ergo is the default solver in Frama-C WP, the recommended solver in GNATprove, and the primary solver in EasyCrypt. It handles linear arithmetic, arrays, quantifiers, and algebraic data types. OCamlPro is a French company — Alt-Ergo is 100% EU jurisdiction.

Z3 — Microsoft Research (Redmond, Washington, USA). Z3 is the most powerful general-purpose SMT solver in the Why3 stack, but it is a Microsoft product. Under the CLOUD Act, Microsoft can be compelled to produce data from its infrastructure regardless of physical location. For certification evidence that needs to remain under EU jurisdiction, Z3 as a solver — even running locally — connects your proof chain to a US-incorporated tool vendor.

Eprover — Stephan Schulz at Stuttgart University (Germany). A first-order theorem prover optimized for equational reasoning, useful for Why3 obligations that involve complex algebraic properties. EU-originated and maintained.

CVC5 — Stanford and University of Iowa (USA). Powerful for quantifier-heavy obligations, but US-originated like Z3.

Coq/Rocq — INRIA (France). For obligations that cannot be discharged automatically, Why3 can export them to Coq for interactive proof. The Coq/Rocq proof assistant itself is INRIA-developed — 100% EU.

For a completely EU-jurisdiction proof chain: Frama-C (CEA/INRIA Paris) → WP plugin → Why3 (INRIA Saclay) → Alt-Ergo (OCamlPro Paris) + Eprover (Stuttgart) — all components are EU-incorporated. No US tool vendor has any part of the proof chain.

Compare this to the Dafny/Boogie stack (Microsoft Research → Z3 as the mandatory solver): the entire verification chain terminates at a US-incorporated tool vendor.

Frama-C + Why3: The French Formal Verification Stack

The most widely deployed Why3 use case in EU industry is the Frama-C WP plugin.

/*@ requires n >= 0;
  @ ensures \result == n * (n + 1) / 2;
  @*/
int sum_to_n(int n) {
  int s = 0;
  /*@ loop invariant 0 <= i <= n + 1;
    @ loop invariant s == i * (i - 1) / 2;
    @ loop assigns i, s;
    @ loop variant n + 1 - i;
    @*/
  for (int i = 1; i <= n; i++) {
    s += i;
  }
  return s;
}

Running frama-c -wp -wp-rte -wp-prover alt-ergo sum.c invokes:

1. Frama-C WP — translates ACSL annotations and C semantics to WhyML
2. Why3 — generates VCs from the WhyML representation
3. Alt-Ergo — attempts to discharge each VC; unresolved VCs are reported as unproved

For complex industrial code, the prover order is typically alt-ergo,z3,cvc5. For certification work where CLOUD Act exposure must be avoided, the order can be restricted to alt-ergo,eprover — sacrificing some automation for complete EU jurisdiction.

Industrial deployments of Frama-C + Why3:

• EDF (Électricité de France) — nuclear safety software at SIL 4 under IEC 61508. The CEA + INRIA + OCamlPro chain (Frama-C → Why3 → Alt-Ergo) is entirely French-operated.
• Airbus (Toulouse, France) — DO-178C avionics verification. Why3 is the VC backend for the WP plugin used in Airbus verification toolchains.
• Thales (France) — defence and railway safety software using Frama-C for DO-178C and EN 50128 certification evidence.

SPARK Ada / GNATprove: AdaCore's Why3 Backend

AdaCore is a French company, founded in Paris in 1994. Its GNATprove tool — the verifier for SPARK Ada programs — uses Why3 as its intermediate language backend. The SPARK → GNATprove → Why3 → Alt-Ergo chain is the default verification path for safety-critical Ada in the EU defence and aerospace sector.

package Account
  with SPARK_Mode
is
   type Balance_Type is range 0 .. 1_000_000;

   procedure Deposit (Amount : in Balance_Type; Balance : in out Balance_Type)
     with Pre  => Balance + Amount <= Balance_Type'Last,
          Post => Balance = Balance'Old + Amount;
end Account;

GNATprove translates the Ada contract annotations and program semantics to WhyML, generates VCs via Why3, and dispatches them to Alt-Ergo (primary) and CVC5 (fallback). The proof session is stored in gnatprove/ and can be replayed without network access — critical for airgapped certification environments used by French DGA (defence procurement) and EU NATO agency contractors.

EasyCrypt: Why3 for Cryptographic Proofs

EasyCrypt — the game-based cryptographic proof system from IMDEA Madrid and Max Planck Institute — uses Why3 for the computational (non-probabilistic) parts of its proofs. When EasyCrypt proves that ML-KEM (CRYSTALS-Kyber, NIST FIPS 203) achieves IND-CCA2 security, the game reduction steps that involve deterministic computation are discharged via Why3 and Alt-Ergo.

The proofs of ML-KEM, ML-DSA, and HACL* — used in Firefox, the Linux kernel, and Signal — all go through this EasyCrypt → Why3 → Alt-Ergo chain. The cryptographic security properties of software used by hundreds of millions of people rest on an EU-native proof infrastructure.

Creusot: Rust → WhyML

Creusot is the Rust deductive verifier from INRIA Saclay — Xavier Denis, Claude Marché, and Jacques-Henri Jourdan. (Marché and Jourdan are Why3 contributors; Filliâtre is Denis's co-author.) Creusot compiles Rust MIR (Mid-level Intermediate Representation) to WhyML, exploiting the fact that Rust's ownership model maps cleanly to Why3's region model.

#[requires(a.len() > 0)]
#[ensures(result@ <= a@.len())]
fn find_first_zero(a: &[i32]) -> usize {
    let mut i = 0;
    #[invariant(i@ <= a@.len())]
    #[invariant(forall<j: Int> 0 <= j && j < i@ ==> a@[j] != 0i32)]
    while i < a.len() {
        if a[i] == 0 {
            return i;
        }
        i += 1;
    }
    a.len()
}

Creusot compiles this to WhyML, Why3 generates the VCs, and Alt-Ergo discharges them. The INRIA Saclay team is effectively building Creusot and Why3 simultaneously — the Rust front-end and the proof backend are co-developed by the same group.

Why3 vs. Boogie (Microsoft Research)

Both Why3 and Boogie (MSR Redmond) serve as intermediate verification languages — the proof obligation layer between source code annotations and SMT solvers. For EU teams choosing between the Frama-C/Why3 stack and Dafny/Boogie/Viper:

For teams running certification evidence that must remain under EU jurisdiction: the Why3 + Alt-Ergo chain provides a documented basis for excluding US-corporate tool dependency. This matters for EU AI Act Article 9 proof artifacts and for CRA 2027 supply chain arguments.

Running Why3 in CI on EU Infrastructure

Why3 is distributed via opam (the OCaml package manager) and as distribution packages:

# Install via opam
opam install why3 why3-ide alt-ergo

# Initialize Why3 with detected provers
why3 config detect
# Output: Found Alt-Ergo 2.x, Z3 4.x, CVC5 1.x ...

For a Frama-C + Why3 CI pipeline restricted to EU-jurisdiction solvers:

FROM debian:bookworm
RUN apt-get update && apt-get install -y \
    frama-c \
    why3 \
    alt-ergo
# Note: Z3 not installed — proof chain is 100% EU-native

RUN why3 config detect
# Only Alt-Ergo detected — this is intentional for certification

Running on sota.io — hosted in Germany, operated under EU law — puts your entire Why3 verification CI under EU jurisdiction. Proof artifacts generated on sota.io (the WhyML files, the session XML, the generated VCs, the Alt-Ergo proof logs) have no CLOUD Act exposure. This is the hosting argument for formal verification teams that Polyspace Cloud on MathWorks infrastructure cannot make.

# sota.io deployment for Why3 CI
# All verification artifacts stay in EU
sota deploy --region eu-west ./verification-ci/

The EU Formal Methods Stack — Complete Picture

Why3 is the middle layer that connects all the EU formal verification tools. Reading this from bottom to top:

Level 0 — Interactive proof assistants: Coq/Rocq (INRIA), Isabelle/HOL (TU Munich + Cambridge), PVS (NASA/SRI — US, but less common in EU industry).

Level 1 — SMT and ATP solvers: Alt-Ergo (OCamlPro Paris), Eprover (Stuttgart), Z3 (Microsoft — US jurisdiction if required), CVC5 (Stanford/Iowa — US jurisdiction if required).

Level 2 — Proof management (Why3): INRIA Saclay. Manages VCs, dispatches to level 1, caches results, provides WhyML as the shared intermediate language for level 3 tools.

Level 3 — Domain-specific verifiers: Frama-C WP (CEA/INRIA Paris), GNATprove/SPARK (AdaCore Paris), EasyCrypt (IMDEA/Max Planck), Creusot (INRIA Saclay).

Level 4 — Source languages: C (via ACSL annotations), Ada/SPARK (via contract aspects), OCaml (via Gospel), Rust (via Creusot attributes), probabilistic programs (via EasyCrypt's pRHL logic).

Every tool at level 3 and above in this EU stack is French or German. Why3 at level 2 is French. Alt-Ergo at level 1 is French. For a certification case that must demonstrate EU-jurisdiction provenance of proof artifacts, this stack provides it from language to proof.

EU Formal Methods Series:

• Frama-C: CEA/INRIA Paris, C Formal Verification — the WP plugin generates Why3 obligations
• EasyCrypt: IMDEA/Max Planck, Game-Based Crypto Proofs — uses Why3 for non-probabilistic obligations
• Creusot: INRIA Saclay, Rust Deductive Verification — compiles Rust MIR to WhyML
• HACL*: INRIA Paris, Verified Cryptographic Implementations — production crypto in Firefox/Linux/Signal
• EU CRA 2027 and Formal Verification — supply chain argument for EU verification tools
• EU AI Act Hosting Compliance — why proof artifact jurisdiction matters
• RATP Line 14: 26 Years of B-Method in Paris Metro — formal verification in production at scale

Why3 and Alt-Ergo are open source and run on standard Linux. sota.io provides EU-native CI infrastructure for formal verification workloads — GDPR-compliant, hosted in Germany, no CLOUD Act exposure. Free tier available.