We present Fun2spec, the first industrial-strength tool guiding LLMs to synthesize C++ specifications in first-order logic with quantifiers. Fun2spec’s very high accuracy (85%) employs an automated validation procedure with error-driven oracle feedback, and can even generate the \emph{strongest} code contract 60% of the time. Our approach significantly outperforms previous methods, achieving \imp{} higher validity on standard benchmarks. We applied Fun2spec to very large scale industrial C++ codebases containing many millions of lines of code and performed comprehensive manual validation to confirm the quality and utility of the specification. Fun2spec stands as the first effective code contract synthesis tool for real-world large-scale low-level C++ programs, advancing the state-of-the-art in automated software analysis using LLMs.