Secure multiparty computation (hereafter, SMC) refers to cryptographic protocols that allow multiple parties to jointly compute a function over their inputs while keeping them private. The main security property of SMC protocols is information leakage freedom, whose proofs can be found in the scientific literature for idealized models. But how does one guarantee that information leakage freedom still holds once SMC is implemented as a concrete piece of software? As a step toward solving this problem, we use the proof assistant Rocq to formalize the security claims of an SMC stack. We develop a method based on an interpreter for a subset of the \(\pi \) -calculus in which protocols can be modeled as programs and then input traces verified for correctness and information leakage freedom. Thanks to this approach, the properties of SMC can be established in a clearly defined trusted base that can be reused to verify other SMC stacks.