Why3

Why3 is a platform for deductive program verification developed at INRIA, the French national research institute for computer science. It is not merely a tool but an integrated environment that unifies the specification, implementation, and proof of correct software — a full-stack verification infrastructure that bridges the gap between program source code and the automated theorem provers that establish its correctness.

The platform's architecture is explicitly modular, separating three concerns that are typically entangled in other verification systems: the programming language in which algorithms are expressed, the logical theories in which properties are stated, and the automated or interactive provers that discharge proof obligations. This separation is not cosmetic. It reflects a systems-level insight: the language of programs, the language of specifications, and the language of proofs have different expressive requirements, and forcing them into a single formalism produces either unreadable programs or inexpressible specifications.

WhyML: A Language for Verification

The programming layer of Why3 is WhyML, an ML-family language designed from the ground up for deductive verification. WhyML combines imperative features — mutable state, loops, exceptions — with functional-programming constructs and, crucially, with specification annotations embedded directly in the code. A function in WhyML carries not only its type signature and implementation but also preconditions, postconditions, loop invariants, and variant expressions that guarantee termination.

These annotations are not comments. They are part of the abstract syntax tree, parsed and type-checked alongside the code itself. The WhyML compiler extracts verification conditions — logical formulas whose validity implies that the program satisfies its specification — and translates them into the platform's intermediate logic. This extraction is the heart of the Why3 workflow: the programmer writes code and specifications in a single, familiar language, and the platform generates the logical machinery required to prove correctness.

The Logic Layer and Standard Theories

Why3 provides a comprehensive standard library of logical theories — integer and real arithmetic, arrays, lists, sets, maps, and higher-order functions — expressed in a polymorphic first-order logic with algebraic data types. These theories are not hard-coded into the tool; they are written in Why3's logic language and can be extended, refined, or replaced by users. The logic layer is therefore a living library, not a fixed calculus.

This design choice has important consequences for scalability. A verification engineer working on floating-point numerical software can import a theory of IEEE-754 arithmetic. One working on security protocols can define a theory of cryptographic primitives. The platform does not dictate what can be reasoned about; it provides the infrastructure for defining the reasoning domain. This is the same architectural principle that makes Iris powerful in concurrent verification: a fixed core with user-extensible invariants.

Prover Drivers: The Bridge to Automation

The most distinctive feature of Why3 is its treatment of automated provers. Rather than committing to a single backend — whether an SMT solver like Z3 or a proof assistant like Coq — Why3 maintains a collection of prover drivers, each translating Why3's intermediate logic into the native input format of a specific prover. Supported backends include SMT solvers (Z3, CVC4, Alt-Ergo), TPTP-compliant first-order provers, and interactive proof assistants (Coq, Isabelle/HOL, PVS).

This multiplicity is not redundancy. It is a recognition that different proof obligations demand different reasoning strategies. A linear arithmetic inequality is best dispatched by an SMT solver in milliseconds. An inductive invariant over a recursive data structure may require the structural induction capabilities of Coq. A proof involving complex set-theoretic reasoning might be most tractable in Isabelle. Why3's driver architecture lets the user send each proof obligation to the prover most suited to its structure, or to multiple provers in parallel, accepting the first successful proof.

Industrial Adoption and the Frama-C Connection

Why3 is not merely a research artifact. It is the verification backend for Frama-C, the industrial-strength C code analysis platform developed by CEA LIST. The Frama-C WP (Weakest Precondition) plugin translates annotated C programs into WhyML, which Why3 then verifies. This pipeline — C source → WhyML → verification conditions → automated provers — represents one of the most mature practical deployments of deductive verification for systems software.

The connection to Frama-C reveals a pattern: verification infrastructure succeeds not when it is self-contained, but when it can be embedded in existing engineering workflows. Why3's driver architecture enables this embedding by allowing the verification backend to evolve independently of the frontend programming language. New SMT solvers can be added without changing WhyML. New programming languages can be supported by writing new frontends that target Why3's logic.

The common framing of the verification landscape positions SMT solvers and proof assistants as competitors in a zero-sum contest for the future of formal methods. Why3 reveals this framing as false. The competition is not between tools but between integration strategies — between the monolithic approach that forces all reasoning into a single formalism, and the modular approach that composes specialized provers into a unified pipeline. Why3's architecture suggests that the future of verified software lies not in finding the one true logic or the one true solver, but in building the infrastructure that lets each proof obligation find its natural home. In this respect, Why3 is less a verification tool than a coordination protocol — a distributed system for reasoning, in which the nodes are provers and the messages are proof obligations.