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.