Distributed systems algorithms are an essential building block to creating fault-tolerant applications. The correctness of such algorithms is crucial. The current work formalizes and specifies three generic multicast algorithms using TLA+ . We detail the formalization process, describing the problems and their corrections. On a more practical side, we implement a prototype of one of the specified algorithms. The current work aims to describe the process of (i) formalization and correction of three generic multicast algorithms and (ii) implementation of an algorithm directly from the specification.Dissertação (Mestrado)Algoritmos de sistemas distribuídos são peças essenciais para criação de aplicações tolerante a faltas. A corretude desses algoritmos é crucial. Nesse sentido, o presente trabalho formaliza e especifica três algoritmos para multi-difusão generalizada utilizando TLA+, corrigindo os problemas encontrados durante o processo. Em um lado mais prático, implementamos um protótipo de um dos algoritmos corrigidos. O presente trabalho detalha os algoritmos, os problemas encontrados e as respectivas soluções, e finalmente, o processo de especificação e implementação.