望安科技创始人受邀作 ICFEM 2025 Keynote报告

    ICFEM 国际形式化方法与工程会议是全球形式化方法领域最具影响力的会议之一。自1997年创办以来，ICFEM 始终致力于推动形式化技术在实际工程项目中的应用，成为连接理论研究与产业实践的重要桥梁。会议邀请来自工业界、学术界与政府机构的研究人员和工程师参与，通过展示最新研究成果和交流实践经验，共同推动形式化方法的理论创新与工程化落地。ICFEM 既注重已经应用于实际工程系统的技术，也关注具有潜力推动产业变革的理论创新，是全球形式化技术前沿交流的重要平台。

    第26届国际形式化方法与工程会议邀请了来自世界各地的顶尖学者和技术专家担任特邀嘉宾，涵盖学术研究和工业实践的前沿方向。望安科技创始人、浙江大学教授赵永望与中国科学院院士何积丰、英国约克大学教授 Jim Woodcock、荷兰特温特大学教授 Mariëlle Stoelinga 在会议中分享了各自研究方向的最新进展，从概率建模、语义基础到系统可靠性分析与形式化验证实践，为参会者带来多元视角的技术思考，全面展现了形式化方法在最新科研与产业实践中的丰富应用。

    作为大会特邀嘉宾，望安科技创始人、浙江大学博士生导师，赵永望教授发表Keynote报告《TRust2: Towards Formally Verified Toolchain of Rust Language in Isabelle/HOL》。近年来，Rust 语言因兼具高性能与内存安全而受到广泛关注，已成为系统级开发与安全关键软件的重要选择。然而，其复杂的所有权模型、生命周期及借用检查机制为程序验证带来了重大挑战。形式化验证提供了一种严格的方法来应对这些挑战，Verus 和 Kani 等工具就是为此目的开发的，并已成功应用于 Rust 系统。

    赵永望教授介绍了开源项目 TRust2，该项目通过 Isabelle/HOL 构建形式化验证的 Rust 工具链，涵盖语义建模、验证器、分析器、编译器及代码生成器等多个环节。项目结构分为三层：语义基础、验证工具链与工业应用，目前正在进行 Rust MIR 语义形式化、Isabelle/HOL 与 Rust 之间的双向对应关系构建，以及 Solana 区块链组件的验证工作。未来将进一步开发 Rust 形式化规范语言，并通过验证技术确保映射过程的正确性，为安全关键软件提供可靠的形式化保证。

    作为国内形式化验证技术的领军企业，望安科技始终致力于将前沿学术成果转化为可实际应用的技术能力，并已将核心形式化验证技术和工具成功应用于多项国家重大项目。未来，望安科技将继续深化技术研究，推动形式化方法在更多领域中的应用，为数字世界的安全建设提供坚实技术支撑。