2026-06-25
当AI包揽数学运算，数学家的意义何在？
随着AI技术的快速发展，数学家们正面临前所未有的挑战与思考。从菲尔兹奖得主陶哲轩探索AI辅助协作证明，到年轻研究者担忧动力与创造力的消退，数学界正在深刻讨论：当AI能代劳大量运算与推导，人类数学家的价值何在？数学家们担忧...
2026-06-18
Pramaana Labs获2700万美元融资，将形式化验证引入AI
Pramaana Labs宣布完成2700万美元种子轮融资，由Khosla Ventures领投，Accel、Nexus等机构参与。该公司专注于法律、药物研发、税务等高敏感领域的AI可靠性问题，通过将大语言模型与基于LE...
2026-06-11
EC2正式验证"隔离引擎"，从数学层面保障虚拟机安全隔离
亚马逊EC2的Nitro隔离引擎是Nitro虚拟机监控程序的核心组件，也是首个在商业云环境中部署的经过正式验证的虚拟机监控程序。该引擎采用Isabelle/HOL证明助手完成验证，生成了33万行机器验证数学代码，规模与s...
2026-06-05
经过验证的机器学习基础设施安全研究报告
随着前沿AI系统的快速发展，保障其运行基础设施的安全变得尤为迫切。恶意攻击者可能窃取模型权重或破坏系统运行，而失控的AI系统也可能利用自身基础设施漏洞绕过安全监控。研究人员于2026年初调查了23位专家，探讨形式化方法能...
2026-05-26
Apple在GitHub上发布iPhone与Mac后量子密码学代码
苹果近日在GitHub发布了corecrypto源代码库，并附上详细技术说明，介绍其在iPhone、Mac等设备上推进后量子密码学工作的成果。此次发布包含ML-KEM与ML-DSA两种后量子算法的实现代码、测试工具及形式...
2026-04-17
Isabelle/HOL：驱动Nitro隔离引擎背后的形式化证明工具
AWS在2025年re:Invent大会上发布了Nitro隔离引擎（NIE），并采用证明辅助工具Isabelle/HOL完成了其正确性与安全性的形式化验证，使NIE成为首个经过形式化验证的云虚拟机监控程序。文章详细介绍了...
2026-04-08
亚马逊推出高性能后量子密码学实现方案
亚马逊推出mlkem-native高保证、高性能的ML-KEM C语言实现，结合参考实现的简洁性与研究优化及形式化验证。利用CBMC和SLOTHY等自动化工具确保内存安全、类型安全和功能正确性，在数学确定性基础上实现激进...
2025-11-11
Ironclad OS项目：用Ada语言构建Unix内核
Ironclad OS项目正在开发一个新的类Unix操作系统内核，面向小型嵌入式系统，计划支持实时功能。该项目的独特之处在于采用Ada编程语言及其可形式化验证的SPARK子集进行开发，而非常见的C、C++或Rust语言。...