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