I have a background in formal methods and PLs, and never used it. I understand the supposed benefits but IME they never got used. Clearly you have used it, so

I have a background in formal methods and PLs, and never used it. I understand the supposed benefits but IME they never got used. Clearly you have used it, so I'll take time looking over your stuff (though I don't know lean). I appreciate you taking the time to write a comprehensive answer, as I said, I'll try to do it justice!