The Pip Protokernel

About Pip

Pip is a protokernel: it allows for kernels, ranging from hypervisors to monolithic kernels, to be developped as user mode applications. Pip only provides system calls for managing isolated partitions of the memory and basic dealing of control flow, thus reducing the trusted computing base to its bare minimum.

The logic of Pip is implemented in Gallina — the language of the Coq proof assistant — and it is in the process of being equipped with a formal proof that it ensures memory isolation. For efficiency, it is automatically translated into freestanding C code.

The architecture-dependent part of Pip is implemented in C and assembly language. It consists of a thin layer giving access the hardware.

Get Pip

You can download the latest alpha release of Pip from its Git repository:

git clone


General documentation

Commented source code



You can interact with Pip's developers and other users through the The Pip-club mailing list.


June 16, 2019
The international workshop ENabling TRust through Os Proofs... and beYond (ENTROPY 2019) was held in Stockholm, Sweden.
December 7, 2018
The first Pip Club Meeting will be held at IRCICA, Villeneuve d'Ascq, France.
January 25-26, 2018
The international workshop ENabling TRust through Os Proofs... and beYond (ENTROPY 2018) was held in Villeneuve d'Ascq, France.


This research project was partially funded by the European project ODSI.


Date Version
November 15, 2018 0.3
September 29, 2017 0.2
October 3, 2016 0.1

ChangeLog (HTML)

Last modified: Fri Aug 2 13:17:27 CEST 2019