This paper articulates a long-term research vision for formal methods at the intersection with artificial intelligence, outlining multiple conceptual and technical dimensions and reporting on our ongoing work toward realising this vision. It advances a forward-looking perspective on the next generation of formal methods based on the integration of automated contract synthesis, semantic artifact reuse, and refinement-based theory. We argue that future verification systems must builds towards individual correctness proofs toward a cumulative, knowledge-driven paradigm in which specifications, contracts, and proofs are continuously synthesised and transferred across systems. To support this shift, we outline a hybrid framework combining large language models with graph-based representations to enable scalable semantic matching and principled reuse of verification artifacts. Learning-based components provide semantic guidance across heterogeneous notations and abstraction levels, while symbolic matching ensures formal soundness. Grounded in compositional reasoning, this vision points toward verification ecosystems that evolve systematically, leveraging past verification efforts to accelerate future assurance.

翻译：本文阐述了在人工智能与形式化方法交叉领域的一项长期研究愿景，勾勒出多个概念性与技术性维度，并报告了我们为实现这一愿景正在开展的工作。基于自动化合约合成、语义工件重用和基于精化的理论，本文提出了对下一代形式化方法的前瞻性观点。我们认为，未来的验证系统必须从构建单个正确性证明转向一种累积性的、知识驱动的范式，在该范式中，规约、合约和证明将持续被合成并在系统间转移。为支持这一转变，我们概述了一个结合大语言模型与基于图表示的混合框架，以实现可扩展的语义匹配和验证工件的原则性重用。基于学习的组件为异构符号和抽象层级提供语义指导，而符号匹配则确保形式上的可靠性。这一愿景基于组合式推理，指向那些能够系统演进的验证生态系统，通过利用过往验证工作来加速未来的保障能力。