[nextos]

Lean is great, but if someone's primary interest is SWE, I think there are better choices. The Lean community is primarily focused on formalizing mathematics right now. This might change in the future. Lean is nice to learn theorem proving, but once you learn the basics, you'll hit a roadblock when trying to move to software verification applications.

For SWE, the most mature option is probably Isabelle. It's also a classical theorem prover, and it's perhaps easier to start with something that doesn't have dependent types. A cool thing is that the canonical Isabelle book [1] has been rewritten in Lean [2].

[1] http://concrete-semantics.org

[2] https://github.com/lean-forward/logical_verification_2025

[nextos]

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

[2] https://fstar-lang.org/tutorial

[gaogao]

The future is now. The recent couple of Lean releases have leaned more on software verification, I believe in part due to Amazon hiring a number of the core devs.