---
layout: plugin
title: Jessie
description: A deductive verification plug-in
key: main
distrib_mode: obsolete
---

## Overview

**Warning** Jessie is currently not actively maintained and
probably incompatible with the latest Frama-C versions.

The **Jessie** plug-in allows deductive verification of C programs annotated
with [ACSL](acsl.html). It uses internally the languages and tools of the
[Why3](http://why3.lri.fr) environment.
The generated verification conditions can be submitted to many external
automatic provers including
[Alt-Ergo](https://alt-ergo.ocamlpro.com/),
[Z3](https://github.com/Z3Prover) and [CVC4](https://cvc4.github.io/).

For more complex situations, interactive theorem provers can be used to
establish validity of VCs. Please look at the
[Jessie](http://krakatoa.lri.fr) web page for more details.

## Usage

The plug-in is activated with the following command line:

    frama-c -jessie [options] <file>.c

A short manual including a tutorial and reference is available on the
[Jessie](http://krakatoa.lri.fr) web page. Please read this document for
details on other command-line options, as well as supported and unsupported
features.