Aliasing often makes programs harder to verify, reason about, and maintain. At the same time, mutation is hard to avoid when writing programs efficiently, especially when performance matters, for techniques such as memoization. As a concrete example illustrating our experience with memoization, I will present ZipLex, a verified lexical analysis framework that provides an invertible lexer satisfying longest-match semantics, and focus on how memoization can be added in a way that remains compatible with verification and avoids aliasing. Although ZipLex is specified in a purely functional style, practical lexical analysis requires memoization to achieve good performance, which is traditionally difficult to reconcile with formal verification. I will show how ZipLex addresses this challenge by using carefully encapsulated mutation that preserves the absence of observable aliasing. This design makes it possible to implement memoization in a simple and efficient way, without monadic encodings, while retaining both strong correctness guarantees and good runtime performance.