Of course such proofs come with caveats - in particular the proofs assume your cryptographic primitives work as intended (e.g. that AES isn't broken) and that you've implemented the specification and not something else - but our experience has been that it's valuable to get those proofs, and where proof turns out to be difficult it's a valuable pointer to weaknesses in your design.
As far as I know nobody has done such a proof for the Noise design, and so we only have our intuition that it looks safe.