Mission-time Linear Temporal Logic (MLTL) is rapidly increasing in popularity as a specification logic, e.g., for runtime verification and model checking, driving a need for a trustworthy tool base. We formalize the syntax and semantics of MLTL and a library of key properties. We then formalize the algorithm and correctness theorems for MLTL formula progression, an algorithm to help decide the satisfiability of an MLTL formula along a given trace, identifying and fixing several errors and gaps in the source material. As a main motivation for our work is tool validation, we ensure the executability of our algorithms.