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?

[1]: https://aybabt.me/blog/correctness-agentic-world