Show HN: Statespace – learn formal methods by building a tiny checked language

I had claude build a course optimized for me (backend engineer with some systems experience) to learn formal methods. Main idea being - I want to build a checked application language which finds bugs with z3, prove things in lean, model concurrency/dist sys behaviors in TLA+, connect it to postgres. It's a static site hosted via gh pages.

Sharing primarily for feedback and suggestions from experts as someone who lacks experience in field. My intuition is that what I enjoy about coding and the demand in my field will eventually turn into this sort of thing - where we control agents using proofs and verification systems.