Lambda the Ultimate

Estasis have provided an approach to theorem proving, the Falso system, leveraging a very proof-theoretically strong axiomatic system - indeed the strongest possible in the tower of consistency strengths, far stronger than Woodin cardinals - together with elegant economy to provide highly compressed proof techniques. It is evidently much easier to prove theorems in this system than, for example, in Coq.

Past discussions here, such as On the (Alleged) Value of Proof for Assurance, show that the great speed-up in providing correctness proofs offered here is to be valued. I cannot bring myself to recommend this system too highly.