Yes I think fundamentally the effort required to understand, write, and verify a formal specification is just way higher than is reasonable in most situations.

There are some cases where it is pleasingly simple - usually low level algorithms like compression, sorting, search etc. Basically things you'd find in leetcode questions.

Most software isn't like that.

I think the actual answer is just that the very latest models (e.g. Astra) are actually quite good at writing normal tests, and you can just skim them to make sure they're doing something sane.