Lean

Programming language and proof assistant for creating formally verified code.

Links