I have long being fascinated by the the field and curious about it on an amature level, i took some basic proof verification and distributed computing classes back in the grad school days, but I'm clearly not an expert in the field by any means. From the article, it seemed like there are plenty of "traps" that i did not even consider - starting from lean hatches like assume(false), expressive power of TLA+ (CTL, ATL), and ofc challenges of tying an real implementation to a proof. To me all three of the above seem challenging enough to deserve their own tools, and i would appreciate smart people putting effort into addressing these rough edges.

Question to you: i can understand how proof verification like z3 or lean requires a special language and an inference engine; given that model checkers like tla+ are mostly about exploring possible program states and checking properties of such states and chains of states, i do not quite understand why it can't be done with a conventional imperative language to express state transitions and invariants - especially an interpreted one like python (esp with continuation support) or a language targeting a vm like wasm where one should be able to snapshot program state?

F-Star and Dijkstra Monads (which are apparently not really monads?) might get you to what you're looking for

The state space you get when using real programming languages like Python is much, much larger than the one you get when abstracting your system design into TLA+. Thus when testing real systems you can only explore very small portions of the state space. This is a real thing people do, although it isn't yet widespread - the term to look for is deterministic simulation testing. Making a DST harness that can handle exploring an application state space without requiring large modification to the application itself is very challenging. Currently Antithesis are the only ones I know who have done it (disclaimer: no connection to this company, I just think they are very cool).