Abstract: Netlog is a high-level language for distributed systems based on datalog, which was recently designed and implemented by Stephane Grumbach and his group at LIAMA. Key features of Netlog are locality of moves, conciseness and simplicity, opening the route to a new approach for proving correctness of distributed algorithms. We present here our formalization of Netlog in Coq, with an application to a distributed algorithm generating a breadth-first spanning tree over an arbitrary topology. The main novelty of this approach is the way we deal with global (e.g. topological) properties of a system which evolves according to local decisions. Joint work wuth Y Deng and S Grumbach.