If verification is the goal, but you don't want to learn theorem proving yet, Dafny is really approachable and practical [1]. F* is also worth considering as a

If verification is the goal, but you don't want to learn theorem proving yet, Dafny is really approachable and practical [1]. F* is also worth considering as a proof-oriented alternative to Isabelle that is focused on software verification [2]. Why3, Rocq and Agda are other obvious contenders. [1] https://dafny.org/latest/OnlineTutorial/guide https://dafny.org/latest/OnlineTutorial/guide [2] https://fstar-lang.org/tutorial https://fstar-lang.org/tutorial