FreeSpec is a framework for the Coq theorem prover whichallows for specifying and verifying complex systems as hierarchies of components verified both in isolation and incomposition. While FreeSpec was originally introduced forreasoning about hardware architectures, in this article wepropose a novel iteration of FreeSpec formalism specificallydesigned to write certified programs and libraries. Then, wepresent in depth how we use this formalism to verify a staticfiles webserver. We use this opportunity to present Free-Spec proof automation tactics, and to demonstrate how theysuccessfully erase FreeSpec internal definitions to let usersfocus on the core of their proofs. Finally, we introduce Free-Spec.Exec, a plugin for Coq to seamlessly execute certifiedprograms written with FreeSpec.