01
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.
↗