Dafny and Whiley are two examples with explicit verification support. Idris and other dependently typed languages should all be rich enough to express the requi

Dafny and Whiley are two examples with explicit verification support. Idris and other dependently typed languages should all be rich enough to express the required predicate but might not necessarily be able to accept a reasonable implementation as proof. Isabelle, Lean, Coq, and other theorem provers definitely can express the capability but aren't going to churn out much in the way of executable programs; they're more useful to guide an implementation in a more practical functional language but then the proof is separated from the implementation, and you could also use tools like TLA+. https://dafny.org/ https://dafny.org/ https://whiley.org/ https://whiley.org/ https://www.idris-lang.org/ https://www.idris-lang.org/ https://isabelle.in.tum.de/ https://isabelle.in.tum.de/ https://leanprover.github.io/ https://leanprover.github.io/ https://coq.inria.fr/ https://coq.inria.fr/ http://lamport.azurewebsites.net/tla/tla.html http://lamport.azurewebsites.net/tla/tla.html