In 1991, Herlihy introduced waitfree linearization of data objects. The talk presents an algorithm for waitfree linearization of an arbitrary (possibly nondeterministic) object in bounded memory. It was designed and verified with the proof assistant PVS. The verification needs 70 invariants. Waitfree progress is quantified in waitfree complexity and is formally proved. The talk cannot present the algorithm in any detail, but only sketch important aspects of the problem, the design and its verification. The paper appears in Formal Aspects of Computing.