LLMLL 发布：基于 SMT 求解器验证 AI 智能体代码的编程语言

LLMLL 是一款专为 AI 智能体编写代码设计的编程语言与验证流水线，通过形式化契约和 SMT 求解器（Z3）在合并前自动验证或驳回代码补丁。系统采用 JSON-AST 结构化补丁和类型化空洞（typed holes）进行任务协作，将模型的幻觉转化为规范搜索过程。对于超出线性算术范围的非线性属性，支持调用 Lean 4 内核生成可独立复核的证明证书。