We present a simple and concise semantics for temporal planning. Our semantics are developed and formalised in the logic of the interactive theorem prover Isabelle/HOL. We derive from those semantics a validation algorithm for temporal planning and show, using a formal proof in Isabelle/HOL, that this validation algorithm implements our semantics. We experimentally evaluate our verified validation algorithm and show that it is practical.
FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
Vals AI；École Polytechnique Fédérale de Lausanne (EPFL)（洛桑联邦理工学院）；Moscow Institute of Physics and Technology（莫斯科物理技术学院）；Indiana University, Bloomington（印第安纳大学布卢明顿分校）；Independent Researcher（独立研究员）
Vero: Can AI Agents Build Formally Verified Software Repositories?
University of Chicago（芝加哥大学）；California Institute of Technology（加州理工学院）；Stanford University（斯坦福大学）；UC Berkeley（加州大学伯克利分校）；Amazon Web Services（亚马逊云计算服务）；Apodex
VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
Huazhong University of Science and Technology（华中科技大学）；University of Alberta（阿尔伯塔大学）；The Chinese University of Hong Kong, Shenzhen（香港中文大学（深圳））；Hong Kong University of Science and Technology（香港科技大学）；Shanghai Artificial Intelligence Laboratory（上海人工智能实验室）
Budget-Sensitive Discovery Scoring: A Formally Verified Framework for Evaluating AI-Guided Scientific Selection
Indian Institute of Information Technology Allahabad (IIITA)（印度阿瓦德理工学院信息学院（IIITA））；National Institute of Electronics & Information Technology (NIELIT)（国家电子与信息科技研究所（NIELIT））
