FormalWeaver: Dependency-Aware Translation of Formal Repositories at Scale

AI agents are increasingly capable of generating formal code and proofs under given specifications, but repository construction requires coherence of specifications and proofs across dependencies, beyond isolated theorem completion. Existing evaluations largely focus on declaration-level success and therefore do not directly measure whether an agent can preserve source coverage, specification semantics, and proof correctness together while growing an integrated repository. We study this gap through formal repository translation, where the task is to translate formal source repositories into another formal language. We introduce FormalWeaver, a source-grounded translation pipeline that decomposes repository-level translation into item-level tasks according to dependency order. Applied to Coq IEEE754 formalization Flocq, the pipeline produces FloatSpec, a Lean port with 58 core files, 5,075 indexed items, and 194,704 lines of Lean code. We further conduct controlled experiments comparing FormalWeaver with different translation trategies on sub-modules of the Flocq translation task. We evaluate two aspects in sequence: whether a translation compiles and, for those that compile, whether it is semantically aligned with the source. Their conjunction defines translation accuracy. The results show that FormalWeaver substantially improves translation accuracy over simpler translation strategies.