Coq

A proof assistant, written in Objective CAML.