Why3 and the Intermediate Language for Deductive Program Verification
Why3 made deductive verification modular by separating programs and specifications from the theorem provers that discharge their verification conditions, creating a reusable intermediate layer for many languages and proof engines.
Why3 was built to sit between programs and theorem provers
Deductive verification rarely ends with one prover. Different proof obligations are easier for different SMT solvers, first-order provers, or interactive assistants, and a source-language verifier should not have to hard-code itself to one backend. Why3, presented by Jean-Christophe Filliâtre and Andrei Paskevich in 2013, was designed as a platform that generates verification conditions and dispatches them to multiple external provers.[1] Its slogan, “where programs meet provers,” accurately describes its architectural role.
The intermediate layer decouples front ends from proof engines
A language-specific verifier can translate its semantics into Why3 once, while Why3 handles prover invocation, transformations, proof sessions, and differences among supported back ends.
WhyML combines a programming language with formal specifications
Why3 includes WhyML, a language for programs and specifications with polymorphic types, pattern matching, mutable records, invariants, ghost code, and inductive predicates.[1][2] Users can write verified algorithms directly in WhyML, but the language is also useful as an intermediate target for tools verifying programs written elsewhere. This dual role makes WhyML both a human-facing formal language and a compiler-like verification representation.
Verification conditions translate program correctness into logical goals
Why3’s verification-condition generator computes proof obligations from contracts and program structure. Its documentation describes a weakest-precondition calculation in which a function’s precondition must imply that execution establishes the requested postcondition.[3] Loops generate obligations for invariants and termination when required; mutable state and exceptions are handled through the language’s formal semantics. The result is a collection of logical formulas independent of the original program syntax.
Verification-condition generation localizes the trusted translation step
Once the program semantics have been correctly encoded into obligations, external provers do not need to understand the source language. They only need to prove the resulting logic formulas.
Prover drivers let one verification project use heterogeneous back ends
Why3 supports numerous automated and interactive theorem provers and provides a driver mechanism for adapting its logical vocabulary to each tool.[2] Arithmetic goals may be easy for an SMT solver, algebraic reasoning may benefit from another backend, and stubborn obligations can be sent to interactive proof assistants. This avoids the assumption that one prover must dominate every verification domain.
Transformations reshape difficult goals before they reach a prover
Why3 can split conjunctions, eliminate definitions, instantiate theories, or otherwise transform verification conditions to suit a target prover. The platform therefore performs proof engineering between source verification and backend solving. This middle layer is important because prover success often depends on the exact logical presentation even when two formulas are mathematically equivalent.[4]
Multi-prover verification needs reproducibility as well as choice
A useful platform must record which prover version, transformation sequence, and proof result belong to each obligation so a verification campaign can be rerun after source or specification changes.
Why3 improved on the earlier Why platform with modular architecture
The Why3 documentation describes it as a complete reimplementation of the earlier Why platform, with a new architecture for calling external provers, a richer input language, and an API intended for use as a software library.[5] Modularity was a central design goal. A verification front end could embed Why3 rather than reinventing prover discovery, invocation, transformation, and session management.
WhyML became an intermediate language for verification of several source languages
Why3’s current documentation lists WhyML as an intermediate language used by verification projects for languages including C, Java, Rust, and Ada.[2][5] The exact front ends change over time, but the architectural pattern is durable: translate source-language semantics into a stable verification IR, generate logical obligations, and let a portfolio of provers discharge them.
An intermediate verification language plays a role similar to a compiler IR
Compilers use intermediate representations so many source languages can share optimization and code-generation infrastructure. Why3 applies the same architectural idea to specifications and proofs.
Why Why3 belongs in the history of reliable software
Why3 belongs in verification history because it made prover diversity an explicit architectural assumption. Instead of binding a verification tool to one theorem prover, it created a common language, verification-condition generator, transformation pipeline, and prover interface.[1][2]
This matters because automated reasoning is heterogeneous. Solvers evolve rapidly, and a backend that is strongest for one theory may be weak for another. A verification platform should be able to adopt better provers without rewriting its source-language semantics. Why3 makes that replacement and competition possible.
The broader lesson is that formal verification benefits from intermediate representations just as compilers do. Programs begin in a language shaped for developers; proof engines expect formulas shaped for automated reasoning. Why3 occupies the middle, preserving the intended contracts while translating them into a form that multiple provers can attack. It also gives verification front ends a stable target while solver portfolios evolve independently, reducing the cost of adopting new provers or changing proof strategies. That intermediate layer has become an important part of modern deductive-verification toolchains.
Works Cited
- 01Filliâtre and Paskevich — Why3: Where Programs Meet Provers researchportal.ip-paris.fr
- 02Why3 — Official Platform Overview why3.org
- 03
- 04
- 05Why3 Documentation — Foreword and Architecture why3.gitlabpages.inria.fr
CodeHistory is a living archive. Citations document the evidence used for this edition; later evidence may refine the account.
Submit a research lead