SE Gyges

so if i want examples of maximally clean verifiable languages I want lean or ocaml, do i have other options? do i want to even consider haskell