Proving correctness of distributed or concurrent algorithms is a mind-challenging and complex process. Slight errors in the reasoning are difficult to find, calling for computer-checked proof systems. In order to build computer-checked proofs with usual tools, such as Coq or TLA + , having sequential specifications of all base objects that are used as building blocks in a given algorithm is a requisite to provide a modular proof built by composition. Alas, many concurrent objects do not have a sequential specification. This article describes a systematic method to transform any task, a specification method that captures concurrent one-shot distributed problems, into a sequential specification involving two calls, set and get. This transformation allows system designers to compose proofs, thus providing a framework for modular computer-checked proofs of algorithms designed using tasks and sequential objects as building blocks. Moir & Anderson implementation of renaming using splitters is an iconic example of such algorithms designed by composition, although the actual algorithm is not modular. Moir & Anderson algorithm is adaptive and non-blocking, and, being the assembly of wait-free concurrent objects, the splitters, it resists testing, because of the cost of covering all its states and transitions even with a small input set. Using the get/set transformation, a modular description of the algorithm can be obtained. A proof of the modular algorithm has been conducted in TLA + and verified with TLAPS, the TLA + Proof System. As far as we know, this is the first time this algorithm is mechanically verified.