O objetivo do trabalho é escrever a especificação TLA+ do algoritmo distribuído Spanning-Tree e usar o TLC para verificar se ele implementa a especificação.
A especificação existente no repositório do Github é uma versão abstrata e não distribuída do algoritmo do artigo "An Assertional Correctness Proof of a Distributed Program", disponível em http://lamport.azurewebsites.net/pubs/pubs.html#dist.
O exerício é o número 65 da lista de exemplos disponível no link: https://github.com/tlaplus/Examples