Applpi is a library in the Coq proof assistant that enables concurrent programs to be modeled and verified in Coq, and the models to be run as OCaml programs. It contains a formalization of a concurrent language based on the pi-calculus, a formalization of a specification language based on spatial logic and lemmas for formal verification. Applpi has been applied to the verification of an HTTP server.

Here are some references:

The whole library: applpi.tar.gz.

  1. Library overview
  2. Case study
  3. Execution of applpi programs as OCaml programs
  4. Extensions

Library overview

Modeling and specification language:

Collection of lemmas:


Case study

A mail server written in applpi:

Execution of applpi programs as Ocaml programs

We use a simple example to show how we can run applpi programs using the Ocaml environment:


This extension to the specification language compiles with the library above but it cannot be used safely with the lemmas based on confluence properties: