UTF8 is one nasty little standard. So many edge cases.
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.
But UTF-8 is also extremely well-studied.
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.
I think such constructs should be part of the language or at least of the standard runtime library and not re-implemented by every Tom, Dick, Harriet & HAL.