Coyotos is a microkernel and OS and the successor of EROS, that itself is the successor of ?KeyKOS. A more complete history can be found here. Its main objectives are to correcte some shortcomings of EROS, demonstrate that an atomic kernel design scales well, and (eventually) to completely formally verify both the kernel and critical system components by writing them in a new language called bitc.

Coyotos is an orthogonally persistent pure capability system. It uses continuation-based unbuffered asynchronous IPC (actually it's synchronous IPC with asynchronous ?system calls).

TODO: explain these terms and (more important) their consequences on system design.

The coyotos microkernel specification can be found here.

There once was the idea of a GNU/Hurd port using the Coyotos microkernel, but this didn't come live.