Anti-unification is the problem of computing the commonalities between syntactic terms. Among its main applications, the detection of code regularities stands out since it is widely used in industrial settings as the foundation for technologies for the recognition of code-cloning, improvement of parallel compilation, and software error detection and correction. This paper discusses the verification of an anti-unification algorithm in the Prototype Verification System (PVS). The algorithm is based on inference rules that constructively compute the common structure between two terms, providing a substitution that expresses the least general generalizer between them as output. To the best of the authors’ knowledge, this is the first formalization of an anti-unification procedure containing proofs of relevant properties, such as termination and soundness.