ABSTRACT. Modern systems have grown in complexity, and the attack surface has increased accordingly. Even though system components are generally carefully designed, and even verified, by different groups of people, the composition of these components is often regarded with less attention. This paves the way for “architectural attacks,” a class of security vulnerabilities where the attacker is able to threaten the security of the system even if each of its component continues to act according to their specifications. In this article, we introduce FreeSpec, a Coq framework built upon the key idea that components can be modelled as programs with algebraic effects to be realised by other components. FreeSpec allows for the modular modelling of a complex system, by defining idealised components connected together, and the modular verification of the properties of their composition. In doing so, we propose a novel approach for the Coq proof assistant to reason about programs with effects in a modular way.