The problem with using subagents is that you often have to rewrite a chunk of a program in a more proof-friendly way, just saying "go prove this code, don't edit it" doesn't work. Maybe I'm underestimating how effectively subagents can communicate though and they'd be fine asking for changes.
Nowadays agents know a lot of tricks on how to effectively prompt subagents
Generally speaking the ouput of a subagent is sent directly to the calling agent, that can make the final edits. Or, the subagent can edit the file in a local copy, and the calling agent can diff it