Será possível ter a certeza se um sistema funciona corretamente, em qualquer situação? Afinal, quanto testamos um sistema, apenas estamos a verificar que ele funciona para um número limitado de casos e não para todos os possíveis. Haverá alguma forma de cobrir todas as alternativas? A resposta é: sim, e uma das formas de o fazer é com verificação formal - com lógica! Este PIC aborda a forma como a Lógica Temporal Ramificada nos pode ajudar na verificação formal de sistemas e como a ferramenta NuSMV utiliza a teoria para automatizar o processo. Através de exemplos simples e de um caso de estudo relacionado com sistemas de segurança em centrais nucleares, demonstra-se como esta abordagem permite detetar erros de conceção e garantir que certos comportamentos desejados (ou indesejados) ocorram (ou sejam evitados), contribuindo para o desenvolvimento de sistemas mais seguros e fiáveis.