> But code is not a closed system

Code is absolutely a closed system.

"Software" might not be, and definitely not software systems -- but code can have each part of it atomically proven to be correct, assuming you test it with a sufficiently complex simulation model (which you've already granted is within the possibilities for LLMs).

Prove all the code in the software system correct, then prove their interactions are correct, and you've achieved your goal.

(I won't claim this is inevitable with the current tools, but it's at least within the realm of possibility)