Memoir—Formal Specs and Correctness Proofs

This tech report presents formal specifications for the Memoir system and proofs of the system’s correctness. The proofs were constructed manually but have been programmatically machine-verified using the TLA+ Proof System. Taken together, the specifications and proofs contain 61 top-level definitions, 182 LET-IN definitions, 74 named theorems, and 5816 discrete proof steps. The proofs address only the safety of the Memoir system, not the liveness of the system. Safety is proven by showing that a formal low-level specification of the Memoir-Basic system implements a formal high-level specification of desired behavior. The proofs then show that a formal specification of the Memoir-Opt system implements the Memoir-Basic system.