> But if we consider the trend is clearly toward the high-level proof-based code[1], which is way easier to audit, then open source is obviously better.

You disprove your own assertion. Cryptography is very specialized. All specializations in this world require specialized knowledge and niche experience, cryptography included. Assumptions about the obviousness of a specialization is almost itself the definition of an error.