I really like F* . It is very close to OCaml in design but allows you to write proofs using a SMT solver or tactic based proofs when the SMT solver gives up. In

I really like F* . It is very close to OCaml in design but allows you to write proofs using a SMT solver or tactic based proofs when the SMT solver gives up. Instead of a proof theoretic language like Coq, the language feels closer to something we regularly program with and the F* compiler can output OCaml and C code. The proofs are erased from the final executable code so you still end up with a program that you would write without proofs. Microsoft Research's project Everest is using it to write a verified HTTPS stack. Edit: formatting