Masking schemes transform circuits such that even adversaries that may learn the value of some intermediate wires do not learn any information about the circuit’s secret input or state. Formal treatments of masking have been proposed but are limited to adversaries that may probe only one intermediate value, or perhaps two for small circuits. We first propose a characterization of threshold probing security as a probabilistic non-interference problem and propose a simple algorithm to prove it. We then propose an algorithm to avoid having to prove one instance of probabilistic non-interference for each possible set of adversary probes (of which there may be many). This allows us to prove the security of core circuits (AES SBox) at orders up to 5. However, practical applications are still out of reach. Therefore, we also propose simple notions of simulatability for gadgets and a simple type-based well-formedness condition on masked circuits that ensures that simulatability composes. Based on these observations, we propose a modular, optimizing and proof-producing masking compiler.