[zasdffaa]

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!