Coq

Coq is a formal verification system based on the Lambda Calculus.