One way to slice it: there are three kinds of underspecification an agent has to close.
Intent: what the user wanted (JWT vs cookies, should free users see this feature). Verification can't close this and probably shouldn't try.
Structural e.g. null, types, exhaustiveness, ownership. Sound static analysis closes this by construction.
Domain e.g. auth on every route, error propagation, contract stability. A domain-shaped apparatus closes this because it knows what kind of program is being built.
Babysitter, auditor, prayer is the right taxonomy of bad options. The fourth option is making the LLM a component inside an apparatus that handles structural and domain statically, and leaving the human on intent.