aallan/vera

解决的问题

LLM 在代码连贯性、维护大型代码库中的不变性以及状态推理方面经常遇到困难。它们容易出现命名错误并丢失变量标识。Vera 通过将变量名替换为结构化引用，并要求每个函数都具有显式且可验证的契约来解决这些问题。

工作原理

Vera 使用一种独特的方法来确保代码的正确性：

• 结构化引用： 使用带类型的 De Bruijn indices（例如 @Int.0）而不是变量名，以避免与命名相关的错误。
• 强制契约： 每个函数必须声明 requires（前置条件）、ensures（后置条件）和 effects（副作用）。
• 静态验证： SMT 求解器 (Z3) 尝试在编译时证明这些契约成立。
• 三层验证： 如果契约无法通过静态方式证明，编译器会插入运行时守卫，以便在发生静默失败之前捕获错误。
• 以智能体为中心的诊断： 错误被设计为 LLM 的指令，提供解决问题的原理和具体的代码示例。

适用对象

• LLM 智能体： 该语言专门为 AI 模型编写而优化，具有针对智能体工作流定制的文档 (SKILL.md) 和指令 (AGENTS.md)。
• 构建 AI 驱动系统的开发人员： 那些需要由模型生成高保证代码的人员。

亮点

• 编译为 WebAssembly，可在 CLI、浏览器或 WASI Preview 2 宿主机中执行。
• 具有显式的副作用系统，用于跟踪 <Inference> 或 <Http> 等副作用。
• 包含用于编辑器支持的语言服务器协议 (LSP)。
• 包含基准测试 (VeraBench)，显示与传统语言相比，模型编写 Vera 的成功率更高。