Many software systems interact with their environment: a typical application creates files, send datagrams through network sockets, and more generally traverses many software layers to achieve basic effectful mechanisms. To get strong guarantees about the execution of these systems, one can implement a software stack from the ground up using a proof assistant like Coq and prove every desired property along the way.

Another plan would be to implement the system with a mixture of untrusted and certified modules, gradually extending the portion of certified code. This method shortens the path to getting runnable software but it requires modularity mechanisms for implementations, specifications, and proofs.

FreeSpec is a Coq library and plugin that offers that kind of modularity mechanisms to implement, to verify and to compose effectful components. In this talk, we will present these mechanisms as well as several applications ranging from building secure hardware architectures to UNIX-style standalone programs. This is joint work with Thomas Letan, Guillaume Hiet and Pierre Chifflier.