SpecForge：用Lilo语言编写形式化规范
SpecForge – A Platform for Authoring Formal Specifications
SpecForge 是一个专为混合系统设计的形式化规范编写平台，核心是 Lilo 语言。它支持通过信号、参数和定义构建系统模型，并利用丰富的时序逻辑算子（如 always、eventually）描述复杂行为。配合 VSCode 扩展和 Python SDK，开发者可以直接在编辑器中进行规范监控、示例生成、反例搜索及格式导出。通过温度控制系统的实战案例，SpecForge 展示了如何快速验证系统是否满足安全约束，让形式化方法从理论走向工程实践。
Lilo 是一种基于表达式的时序规范语言，专为混合系统设计。
HN 评论区
12- giancarlostoro
该项目的首页上醒目地写着“AI 驱动”（AI-Powered）：
一个由 AI 驱动的平台，供开发者通过形式化与分析的迭代过程来“锻造”严谨且精确的系统规范。
标题里或许应该加上这一点，以便让大家意识到，如果采用这个工具，就默认 AI 参与其中；除非这是一款 AI 可选的产品，那他们就需要明确说明。
- itomato
是谁的形式化？马还得排在前面。
- abbasov_murad
这个方法当然很适合用来学习，但我理解起来有些困难。