> This has been insanely valuable to me lately.
This surprises me. Formal verification so far has been a very niche thing apart from conventional type systems. I didn't think lack of vibe coding was much of a bottleneck in the past. Where do you use it?
The problem is implementing anything approximately twice is a hard sell… this is no longer true, though - TLA+ models are cheap now. You should be using them when writing any sort of distributed systems, which is basically everything nowadays.
Roughly anything that, say, has the complexity of a leetcode medium level problem that isn't already an extremely well known algorithm.
Any moderately complex thread safety thing with a few moving parts (e.g. there are multiple mutexes involved in various parts of the system, verify no deadlocks).
The lack of vibe coding has been a bottleneck for literally everything before.
When I see people say the hate vibe coding, I think "why do you hate formal verification? Because you could be spending your time on formal verification instead of removing "code smells" that don't hurt anything from vibe code."