The section "So what is the helpful thing that formal verification is doing?" should be more prominent. Many devs look at FV as some kind of difficult, mathematical proof for their app. However, this motto is much more approachable, I think: "With formal verification, you can specify your intent in an almost arbitrary number of different redundant ways, and the program only verifies if they are all compatible."

And you don't need to start with Lean 4. Dafny, for example, is a bit easier https://dafny.org/