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.


January 25-26, 2018
The international workshop ENabling TRust through Os Proofs...and beYond (ENTROPY 2018) was held in Villeneuve d'Ascq, France. It consisted of a talk on the Pip protokernel and eleven invited talks by eminent international researchers in the field of formal verification of operating-system kernel.


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


Date Version
September 29, 2017 0.2
October 3, 2016 0.1

ChangeLog (HTML)

Last modified: Wed Feb 7 12:55:36 CET 2018