TLA+, P, Lean... formal methods and previously esoteric testing methods (property based, mutation... testing) should become the default. I think it's the only way we can really reap the benefits of agentic coding.
I wrote about this a bit on my blog[1], different angle but along the same line. You explain TLA+ and model checking well which makes the case concrete.
I'm curious of you have thoughts on these other methods and tools like P, Lean, Dafny, etc?
I am eagerly following https://github.com/flux-rs/flux https://flux-rs.github.io/flux/
They have a development pace very quick and can verify real world Rust code. There's a huge graveyard of Rust verification tools, but I hope this one gets broader usage