Because guaranteed to never fail requires some UX inconveniences, and the industry (and the market) doesn't seem in a mood to tolerate inconvenience for the sake of security.
Agents themselves are inherently probabilistically correct. Often correct more often than humans at this point!
But that doesn't mean they don't have >0% failure modes, often in very non-human, unexpected, even dangerous ways.
Whether that's "sloppy"?
Eh, it's just the nature of the tool, like a perfect screwdriver that randomly strips 1% of screws.
> it's extremely easy to ask a coding agent to prove code correctness
That statement is categorically wrong.
If you're talking about a formal proof for non-trivial, real-world code, no.
If you're talking about a comprehensive set of tests... well, I'd challenge you to elucidate how you see creating a comprehensive set of tests as trivial.
And if the answer is more LLM... then I think we're at a fundamental disagreement about what satisfies "guarantee" or "provable".
Because I must warn you - it's extremely easy to ask a coding agent to prove code correctness before committing his work.