You can embed TLA+ into Lean. I don't think that there's any benefit to formalization before coding unless you're working on like million dollar projects