WhyML

WhyML is the specification and programming language at the core of the Why3 verification platform. Designed as an ML-family language with built-in support for deductive verification, WhyML allows programmers to write code, specifications, and proof hints in a single unified syntax. Functions declare preconditions and postconditions; loops declare invariants and variants; and the Why3 toolchain automatically extracts verification conditions that discharge to SMT solvers or interactive proof assistants.

WhyML's design reflects a rejection of the separation between programming