 Matita

Matita
is an experimental proof assistant under development at the Computer Science Department of the University of Bologna.It is a tool aiding the development of formal proofs by man-machine collaboration, providing a programming environment where formal specifications, executable algorithms and automatically verifiable correctness certificates naturally coexist.