Résumé : Declarative languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. It has been shown that they simplify greatly the code, while still offering efficient distributed execution. In this report, we show that moreover they provide a promising approach to the verification of distributed protocols. We consider the Netlog language and use the Coq proof assistant. We first formalize the distributed computation model based on message passing with either synchronous or asynchronous behavior. We then see how the declarative rules of the protocols can be simply encoded in Coq and we develop the machine embedded on each node of the network which evaluates the rules. This framework enables us to formally verify distributed protocols, as shown on a concrete case study, a spanning tree construction in both the asynchronous and synchronous setting.