Description
Formal proof scripts can be edited and driven from Emacs through a common interface for proof assistants. This is useful for researchers, students, and developers working with theorem proving and verified mathematics or software.
It is an editor integration, not a proof assistant by itself. Users still need the underlying prover, and proof correctness depends on that prover and the scripts being checked.