DC2 is a small operating system that demonstrates interesting properties of the P programming language.
- It runs on a bare (commodity PC) hardware.
- It is composed from multiple interacting subsystems.
- It has a tiny trusted computing base (TCB).
- As a whole, it is defensively correct.

The implementation implementation is accompanied with a technical documentation.