Descrição
Scripts de prova formal podem ser editados e controlados pelo Emacs por uma interface comum para assistentes de prova. Isso é útil para pesquisadores, estudantes e desenvolvedores que trabalham com prova de teoremas e matemática ou software verificado.
É uma integração de editor, não um assistente de prova por si só. O usuário ainda precisa do provador subjacente, e a correção da prova depende desse provador e dos scripts verificados.