Velvet

Velvet is a foundational multi-modal verifier for imperative programs in Lean 4: write imperative algorithms with contracts, prove them automatically, and finish anything left over by hand.