This vision paper articulates a long-term research agenda for formal methods at the intersection with artificial intelligence, outlining multiple conceptual and technical dimensions and reporting on our ongoing work toward realising this agenda. 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 move beyond isolated 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.

翻译：本愿景论文阐述了形式化方法与人工智能交叉领域的长期研究议程，勾勒了多个概念与技术维度，并报告了我们为实现该议程正在开展的工作。论文基于自动化契约合成、语义构件复用和基于精化的理论整合，提出了面向下一代形式化方法的前瞻性视角。我们认为未来的验证系统必须超越孤立的正确性证明，转向累积性、知识驱动的范式——在该范式中，规约、契约和证明能够在系统间持续合成与迁移。为支持这一转变，我们提出了结合大语言模型与图结构表示的混合框架，以实现可扩展的语义匹配与验证构件的规范化复用。基于学习的组件为异构表示法和抽象层级提供语义引导，而符号匹配则确保形式严谨性。这一植根于组合推理的愿景指向能够系统演化的验证生态系统，通过利用过往验证成果来加速未来的可信性保障。