FreeSpec is a framework for the Coq theorem prover which allows for implementing, specifying and verifying complex systems as hierarchies of components verified both in isolation and in composition. FreeSpec was originally designed for reasoning about hardware architectures. In this article, we present a new iteration on the FreeSpec formalism we call Mutual Obligations logic specifically designed to develop certified programs and libraries. Then, we present how we use this formalism to verify a webserver for static files. We use this opportunity to present FreeSpec proof automation tactics, and demonstrate how they successfully erase FreeSpec internal definitions to let users focus on the core goals of their proofs. Finally, we introduce FreeSpec.Exec, a plugin for Coq to seamlessly execute certified programs written with FreeSpec.