BRIDGE: Building Representations in Domain-Guided Verified Program Synthesis

Large language models (LLMs) are increasingly used to write code, but generated programs can look correct while still containing subtle bugs, missing edge cases, or mismatched assumptions. This motivates verifiable coding, where the output includes not only code but also formal artifacts that justify the code against a specification. In proof assistants such as Lean4, this is a multi artifact prediction problem: executable code, specifications, theorem statements, and proof attempts must remain mutually consistent. We present BRIDGE, a structured prompting framework that decomposes this process into Code, Specification, and Theorem/Proof domains. BRIDGE uses reasoning tailored to each domain, together with checks across artifacts, to reduce semantic drift. Our primary code metric is Lean executable correctness: the generated program must elaborate, satisfy Lean's termination and totality checks, and pass benchmark tests. This metric is stricter than ordinary unit test accuracy, but it is not a substitute for full semantic verification. Across our 178 problem Lean benchmark and the public VERINA and CLEVER benchmarks, BRIDGE improves executable correctness by up to 1.5× and reaches comparable success with up to roughly 2× fewer Lean evaluations. Supervised fine tuning on BRIDGE style functional traces improves over matched direct trace fine tuning, suggesting that the representation can be internalized rather than used only as a prompt. BRIDGE also improves specification guided code generation and downstream theorem/proof diagnostics, producing more Lean elaborating theorem statements and more completed proof attempts aligned to the implementation. Overall, BRIDGE provides a verification oriented inductive bias for connecting code, specifications, theorem statements, and proof attempts, while leaving full semantic proof completion at scale as an open problem.