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."