LLMLL v0.28.2 发布：让 AI 智能体在形式化契约下写代码、编译器用 Z3 证明后再合并

LLMLL（Large Language Model Logical Language）v0.28.2 是一门以 LLM 智能体为主要作者的编程语言与验证管线：契约规定函数目标，智能体填写类型化 ?hole，编译器在合并前用 Z3（经 liquid-fixpoint）对每个函数体做 SMT 证明，补丁以 RFC 6902 JSON-Patch 形式作用于 JSON-AST，避免文本合并冲突。实验记录中三个前沿模型在 54 次尝试中 0 次错误填充；SMT 不可判定的非线性义务可用实验性 --leanstral 交由 Leanstral 证明并由 Lean 4 内核加 Mathlib 复核，生成可独立验证的 .lean 证书。