I should check it against my email address validator that would be a nice benchmark. It's interesting that there are people that are using email addresses that are not actually valid according to the standard.
We can have an LLM enumerate all those edge cases, and we can assemble them into a spec. Then we can integrate that spec into a proof.
And because the spec is functional rather than expressive, we can produce copyright-free, provably correct reference implementations whose correctness is as strong as our spec and our proof process.
This reference implementation would then be available for use by a language like PHP, or perhaps an LLM generating a vibe-coded dependency.
Over time, then, the accumulation of such proven reference works grows. We'll never prove all the application code out there correct, but incremental progress is possible.