[[!meta copyright="Copyright © 2006, 2007, 2008, 2010, 2011 Free Software Foundation, Inc."]] [[!meta license="""[[!toggle id="license" text="GFDL 1.2+"]][[!toggleable id="license" text="Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.2 or any later version published by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license is included in the section entitled [[GNU Free Documentation License|/fdl]]."]]"""]] [[!meta title="Coyotos"]] [*Coyotos*](http://www.coyotos.org/) 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](http://www.coyotos.org/history.html). 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](http://www.bitc-lang.org/). Coyotos is an orthogonally [[persistent|persistency]] 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](http://www.coyotos.org/docs/ukernel/spec.html). There once was the idea of a GNU/Hurd [[port using the Coyotos microkernel|history/port_to_another_microkernel]], but this didn't come live.