---
layout: plugin
title: WP
description: Deductive proofs of ACSL contracts.
key: main
distrib_mode: main
priority: 0
manual_pdf: /download/frama-c-wp-manual.pdf
additional:
  - name:  "ACSL by Example, by Fraunhofer FOKUS"
    short: "ACSL by Example"
    link:  https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf
  - name:  "Introduction to C program proof with Frama-C and WP, by Allan Blanchard"
    short: "Tutorial on Frama-C/WP"
    link:  https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf
---

## Overview

This plug-in allows proving that ACSL contracts are
fulfilled for all possible executions of the code. It is based
on weakest-precondition calculus and relies on external
automated provers and proof assistants to finalize the assessment of the
desired properties.

Proving properties by WP is a modular approach, which makes
it a strong alternative to consider in replacement of
traditional unit testing.

## Quick Start

    frama-c -wp file.c

## Technical Notes

- Maturity: industrialized.
- **WP** has an internal prover, **Qed**, which is also used to simplify
  proof obligations before they are sent to external provers.

Recommended External Provers:
- Alt-Ergo
- Coq
- Z3
- CVC4

And all other provers supported by the [Why3](http://why3.lri.fr) platform.

## Further Reading

For more details about the **WP** plug-in, including installation instructions,
please consult the [WP manual]({{page.manual_pdf}}).

Besides the manual, the **WP** plug-in is used in some tutorials:

- [{{page.additional[0].name}}]({{page.additional[0].link}});

This tutorial, written by the Fraunhofer **FOKUS** team, provides an extensive
corpus of [ACSL](/html/acsl.html) annotations for typical C programs to be proved by
**WP**. It is available online and a public repository hosts the annotated
source examples.

- [{{page.additional[1].name}}]({{page.additional[1].link}});

This tutorial, written by Allan Blanchard, introduces several notions of program
proof before describing [ACSL](/html/acsl.html) and **WP**, and how to perform
proofs using Frama-C.

## Dependencies

This plug-in can (optionally) use the results of the [RTE](rte.html) plug-in.