Verificar a corretude de um software ou hardware tem sido de grande interesse para aplicações que precisam ser à prova de falhas. Sistemas de missão-crítica, quando apresentam alguma falha, podem causar perdas financeiras ou ter consequências fatais. Por isso, a aplicação de ferramentas de verificação de sistemas tem sido usada para desenvolver sistemas com alta garantia de sucesso. Uma ferramenta para escrever definições e demonstrações formais verificadas por máquina é o assistente de provas. Como parte final do meu Projeto Orientado em Computação, o assistente de provas Coq foi utilizado para demonstrar a corretude dos algoritmos dos algoritmos de ordenação por inserção e ordenação. Um algoritmo de ordenação está correto se sua saída é uma permutação da entrada e está ordenada. Esta definição foi escrita em Coq e foi aplicada nos algoritmos de ordenação  citados para escrever suas demonstrações. O código das demonstrações encontra-se no apêndice deste trabalho. Apesar do Coq verificar se as demonstrações estão corretas, não é possível verificar por máquina se a especificação dos conceitos ou algoritmos estão corretos. Algumas novas táticas foram utilizadas em relação à primeira parte deste trabalho. É possível, por exemplo, criar novas táticas a partir das antigas. Uma possível continuação desse trabalho é a demonstração da corretude de outros algoritmos de ordenação.