The ML module system provides proven mechanisms for organizing and maintaining large programs through the use of {\em structures}, to implement program units, and {\em signatures}, that give an abstract specification of structures. A signature is a partial specification: it simply lists the components of the structure together with their types. For domains with security or timing requirements, it is important to give stronger guarantees about program behavior.
We address this issue by augmenting program signatures with formal specifications, and structures with proofs. Security specifications are given in terms of a type theoretic interpretation of the program implementation. The type theory required to support this extension is the translucent sum calculus of Harper and Lillibridge extended with equality and constraint types. The Curry-Howard isomorphism provides a correspondence between executable programs and their proofs, allowing control over the degree of security desired.