Jean-François Monin，法国Verimag和格勒诺布尔-阿尔卑斯大学计算机科学教授。Monin教授曾在法国电信研究与发展部门领导一个专注于形式方法的研究小组，并成功地将其应用于工业环境中软件设备正确性属性的证明。他的研究工作致力于类型理论、交互式定理证明工具，以及在分布式算法、信息安全问题和嵌入式软件等领域的应用。除了在这些领域发表多篇研究论文外，他还出版了一本名为《Understanding Formal Methods》的书籍，涵盖了这一热门领域中各种最新方法。他曾在多个地方教授Coq、函数式编程和形式方法，包括5届亚太夏季形式方法学校（APSSFM）。

施晓牧，中国科学院软件研究所计算机科学国家重点实验室可信智能系统组副研究员。法国格勒诺布尔大学博士，曾在清华大学做博士后研究工作、在深圳大学计算机与软件学院任副研究员。研究专注于定理证明器相关的形式化验证，包括密码程序验证、硬件描述语言编译过程验证、硬件模拟器的正确性等研究，其中密码验证的工具CryptoLine已成功应用于多种后量子密码程序验证上。相关研究成果发表在CAV、CCS、CHES等国际会议与期刊上。

詹博华，华为编程语言实验室技术专家。2014年博士毕业于普林斯顿大学数学系，之后在麻省理工学院和慕尼黑工业大学任博士后。2018-2024年在中科院软件所任副研究员。2024年加入华为编程语言实验室。研究工作包括证明自动化方法和交互式定理证明器的设计与实现，嵌入式系统的建模与验证，以及在程序验证、操作系统、分布式系统、量子程序验证的应用。在CAV, IJCAR/CADE, TACAS, ITP, J. Automated Reasoning等形式化方法领域的主要会议和期刊发表文章30余篇。

曹钦翔，上海交通大学长聘教轨副教授、博士生导师。2013年本科毕业于北京大学，2018年在普林斯顿大学获得博士学位，曾获上海浦江人才计划资助。曹钦翔长期从事基于定理证明的程序验证与程序逻辑研究，论文主要发表在POPL、OOPSLA、JAR等国际著名会议或期刊，其代表性工作VST、VST-A程序验证工具是目前世界范围内最知名的几个程序验证工具之一。