[AYBABTME]

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

[nextaccountic]

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