标签
SpecForge是一个使用Lilo时序规范语言编写形式化规范的平台,提供了VSCode扩展,包含语法高亮、类型检查以及对混合系统的可满足性分析。
Gilad Bracha 设想了一个未来,软件工程师使用AI将非正式需求转化为形式化规范并加以审查,而AI则实现代码并用定理证明器验证其是否符合规范。人类负责确保形式化规范正确,他们仅需编写自然语言。