LLMLL v0.28.0 发布：智能体填类型洞，SMT 求解器拒绝错误实现

LLMLL — v0.28.0

一项让 AI 编写代码的实验：编译器针对每个函数的契约进行证明，并在合并前反驳一个类型正确但实现错误的函数体。

LLMLL（Large Language Model Logical Language）是一种编程语言和验证流水线，专为 AI 智能体在形式化契约下编写代码的实验而构建。其主要作者是 LLM 智能体，而非人类：契约规定函数必须做什么，智能体填充带类型的洞，编译器在应用补丁前用 Z3 针对每个函数体证明其满足契约。智能体通过这些契约进行协调，而非通过对话。智能体可以幻觉出一个实现，这没关系，只要它满足契约即可：验证将幻觉从一种失败模式转变为一种搜索策略（生成候选、对照规范检查、接受或拒绝）。

当前版本：见 CHANGELOG.md § Latest。各版本的完整发布说明位于 CHANGELOG 中；本 README 不再重复。

了解更多：docs/README.md 是文档的阅读指南 · ROADMAP.md 说明已发布的内容和下一步计划 · experiments/README.md 索引了各项实验及其结果。

亲眼看看：无法被创造出来的钱，已被证明

conserve(from, to, amount) 返回转账后的两个余额，其契约将二者绑定在一起：(first result) + (second result) = from + to：总额守恒，仅此而已。一个故意写错的函数体给目标账户多记一个单位，它类型正确，检查时看起来也无害，但它破坏了守恒性，SMT 求解器会反驳它：

# body:  (pair (- from amount) (+ to (+ amount 1)))      ← type-correct, creates money
$ llmll verify conserve-bad.llmll
error: body verification of 'conserve-bad' failed —
       implementation does not satisfy postcondition (constraint #0)

# body:  (pair (- from amount) (+ to amount))             ← correct, conserves the sum
$ llmll verify conserve.llmll
✅ conserve.llmll — SAFE (liquid-fixpoint)

该证明同时覆盖两个返回值：这是一个关系不变量，而非对单个数值的约束。上面这个错误的函数体是脚本预设的，用于展示检查被触发；并非由智能体生成。Dafny、Liquid Haskell 或 F* 也会反驳它；LLMLL 增加的是围绕证明的循环，见下文。

_{本录制中错误的函数体是脚本预设的，用于展示检查被触发；并非由智能体生成。用 make demo-gifs 重新生成。如果本页上的动画显示为静止帧，可能是你的浏览器或 GitHub 的动画图像无障碍设置将其暂停了；点击图像可直接打开 GIF。}

完整可复制粘贴的演练：payments-core/DEMO-RUNBOOK.md —— 组合的 transfer/debit 调用链节拍和单构造器 settle 节拍也在那里。关于交互式修复循环协议——智能体检出带类型的 ?hole，提交补丁，编译器在合并任何内容之前拒绝或接受它——见 withdraw-demo/DEMO-RUNBOOK.md（讲解：DemoPost.md）。

为什么不直接让智能体编写 Dafny、Liquid Haskell 或 F*？

这些工具证明的是同一类性质，而 LLMLL 的证明路径（基于 Z3 的 liquid-fixpoint）正是 Liquid Haskell 所使用的那条。LLMLL 并不声称拥有更强的验证器。它为智能体编写代码的场景构建了围绕验证器的循环：

洞即契约。llmll checkout 给智能体一个带类型的 ?hole，附带其前置条件、必须满足的后置条件以及作用域内的名称，而不给出答案。llmll patch 仅在程序仍能通过类型检查且求解器不反驳它时才应用填充。
弱契约会被标记。--weakness-check 报告一个弱到连平凡函数体都能满足的契约；--cdp 对契约排除错误函数体的严格程度进行评分。
每个函数都带有信任级别。信任报告将每个函数标记为verified、asserted等，而verified声明绝不会悄悄依赖于未经证明的被调用者。
Agent 编辑的是结构，而非文本。每个程序还都有 JSON-AST 形式，补丁是针对它的 RFC 6902 JSON-Patch，因此不存在文本合并冲突。
分解会被检查。llmll refine 一步填补一个洞并生成带契约的子洞，并拒绝任何没有函数体能满足或什么都没说的子契约。

实验表明了什么。在 experiments/minimal-agent/ 中，三个前沿模型在专为使其出错而构建的测试夹具上，30 次中有 30 次写出了经验证正确的函数体，54 次尝试中 0 次错误填充。这些证据是为了保证：Agent 编写的代码，针对 Agent 未编写的契约进行证明。本 README 和博客中的反驳演示使用脚本化的错误版本，以表明检查有效；这些实验中的 Agent 并未产生它们。每个实验及其结果：experiments/README.md。

证明求解器无法证明的——经内核检查

并非每个性质都可由 SMT 判定。square(n) = n*n 声明 result ≥ 0——但 n*n 是非线性的，超出了 LLMLL 发送给求解器的线性算术片段，因此 SMT 验证器只能将后置条件标记为asserted（明确的“未证明”）。借助 --leanstral，LLMLL 将该义务表述为 Lean 定理，让 Leanstral 证明它，并用 Lean 内核 + Mathlib 检查该证明——记录一个verified-lean层级，并附有可独立重新检查的.lean证书。

_{实验性。在 v0.26.3 上针对 Leanstral API 实时记录；用 examples/leanstral-demo/demo.sh 重新生成（需要 API 密钥和 Lean 4 + Mathlib 项目）。}

$ llmll verify examples/leanstral-demo/square.llmll --trust-report
  square:  post: asserted                       # nonlinear: outside the SMT fragment, not proven

$ LLMLL_LEANSTRAL_API_KEY=… llmll verify examples/leanstral-demo/square.llmll \
    --leanstral --leanstral-lean-project ~/proofcheck --trust-report
  square: Leanstral proof found, Lean kernel + Mathlib CHECKED
  square:  post: verified-lean   (certificate: square.verified.lean)

证书是内核接受的 Lean 证明项，任何拥有 Lean 的人都可以检查，而无需信任 Leanstral。你仍然需要信任的是 LLMLL 将契约翻译为 Lean 定理陈述的过程。AI 证明了 SMT 求解器无法证明的东西，而你不必只听它的一面之词。

实验性。可选演示；需要 Leanstral API 密钥（LLMLL_LEANSTRAL_API_KEY）和本地 Lean 4 + Mathlib 项目。对所有义务类别的生产级 Lean 验证是推迟的LEAN-GA重建。复现：examples/leanstral-demo/（demo.sh）· 设计：docs/archive/shipped-design-specs/leanstral-demo-spec.md。

试用

完整的修复循环（洞 → 被拒绝的错误填充 → 被接受的修复 → 已验证）是可复制粘贴的 DEMO-RUNBOOK.md。

_{这两个填充是 Agent 的脚本化替代品：提交到仓库的固定补丁文件，并非由 Agent 运行产生。脚本：examples/withdraw-demo/demo.sh。}

零安装（Docker）。无需 Haskell 工具链——镜像捆绑了 llmll、z3 和 liquid-fixpoint：

# see the SMT refutation of a conservation-breaking fill (no local files needed):
docker run --rm ghcr.io/machunter/llmll verify /opt/llmll/examples/payments-core/conserve-bad.llmll
# verify your own file (mounts the current directory at /work):
docker run --rm -v "$PWD":/work ghcr.io/machunter/llmll verify myfile.llmll

从源码构建。先构建：

cd compiler && stack build
stack exec llmll -- --help

需要 GHC ≥ 9.4 + Stack ≥ 2.9。证明步骤还需要 z3 + liquid-fixpoint。

没有求解器，什么都通不过。在从源码构建的路径上，若缺少 z3/liquid-fixpoint，verify 会打印 SOLVER NOT FOUND -- NOTHING WAS PROVEN 横幅并以 3 退出，而 patch / refine 拒绝应用带契约的补丁（PatchVerifyUnavailable，退出码 3）。安装两者即可看到反驳。（Docker 镜像捆绑了两者，因此永远不会遇到这种情况。）参见 docs/getting-started.md。

它是什么

LLMLL 将验证视为协调协议。主导代理定义类型和契约（做什么）；专家代理用怎么做填充带类型的空洞；编译器在合并前根据契约验证每一次填充。代理信任彼此的契约，而不是彼此的代码。合并是结构化的 JSON-AST 补丁，而不是文本差异——因此不存在结构性合并冲突，并且每个补丁在落地前都会重新验证。

它并不声称程序正确。它保证所有代码与其声明的规范一致，并追踪每个保证的强度：verified 契约由 SMT 求解器证明；asserted 契约则没有。信任会传播——没有任何 verified 声明会悄悄依赖于未经证明的依赖项。弱点检查器（--weakness-check）甚至会标记出弱到连平凡实现都能满足的契约。其判别力姊妹工具（--cdp）则对契约排除错误实现体的锐利程度进行评分。这两项检查衡量的都是非空性，而非规范保真度：一个具有判别力但捕捉了错误行为的契约仍然会通过，代码也仍然能针对它通过验证。

已证明与未证明——在相信标题之前请先阅读此内容

已发布的证明路径是在非递归 QF-LIA 核心上运行的 SMT（通过 liquid-fixpoint 调用 Z3）——整数线性算术、let 绑定、条件语句、对带契约函数的调用（假设-保证），以及对可接受（非递归）和类型（Result 和用户 ADT，嵌套且顺序）的 n 臂匹配——并扩展了三种可判定理论：数组类（bytes[n] 内存安全，以及 map[{int,string},{int,bool,string}] put 后 get / 键存在性 / 构造 / 读-改-写）、可接受的数据类型构造，以及字符串字面量（相等性、相异性以及码点长度）。这涵盖了数值边界、守恒不变量、长度保持、数组/映射边界与存在性安全，以及字符串标签判别。其他所有内容——字符串结构（拼接、子串、正则表达式）、递归载荷 ADT、非线性算术（* / mod）、IO——回退到仅契约检查、属性测试或运行时断言，每一项都带有明确的信任标签（完整矩阵见 LLMLL.md §5.3.5）。递归位于片段内部：有了求解器可消解的 (decreases e) 度量，证明就是全的；没有它，则仅在递归终止时成立，并且 verify 标题会去掉 ✅ 并指明该函数。

非线性义务有一条实验性的 Lean 4 路径：即上文所示的可选 --leanstral 标志，它需要 Leanstral API 密钥以及本地 Lean 4 + Mathlib 项目。跨所有义务类别的生产级 Lean 验证被推迟。--leanstral-mock 针对模拟证明器运行同一流水线，用于测试。

docs/one-pager.md 包含完整的主张到证据映射——每项主张都映射到已发布的命令或明确的“计划中”/“未发布”标签。“计划中”/“未发布”标签是有意为之的；在分享之前请先阅读它。

该仓库运行于 LLMLL

这个仓库的六个 CI 门禁是 LLMLL 程序，位于 tools/：version-gate（版本横幅与 schema 版本一致）、doc-archive（每个归档设计文档都位于其状态所声称的位置）、doc-claims（文档声称编译器拒绝的内容，与编译器实际行为对照检查）、doc-path-lint（正文中的路径引用；仅供参考）、refute-crux（96 个冻结的 verify 判定结果，因此丢失的反驳会导致 CI 失败）以及 build-smoke（端到端构建并运行其他五个门禁）。CI 工作流会在每次推送到 main 以及针对它的每个拉取请求时构建并运行它们。在同一次运行中，每个门禁的决策核心（adjudicate.llmll）必须通过 llmll verify，而该核心的一个故意破坏的副本（crux-*.llmll）必须被反驳，否则运行失败。只有决策核心被证明；围绕它的文件和进程处理是构建并运行的，而非被证明。

代码树中最大的 LLMLL 程序不是 CI 门禁。tools/llmll-driver/ 是 RFC-SWARM 流水线驱动程序：39 个模块共 8522 行，包含 55 个已证明函数和 581 个按构造即无证明的有副作用 def-shell 函数（docs/design/driver-ll-campaign-close.md）。其 README 区分了哪些是被证明的，哪些只是被断言的。

编译器

当前使用的编译器是 compiler/ 中的 Haskell stack 项目。它是唯一受支持的后端。

命令	作用
`llmll check <file> [--strict]`	解析 + 类型检查；输出结构化诊断信息。使用 `--strict` 时：未绑定变量、未知函数、未知运算符以及分支类型不匹配都是硬错误而非警告。不使用 `--strict` 时：文本模式在成功时渲染累积的警告。
`llmll holes <file> [--deps] [--deps-out FILE]`	列出所有 `?hole` 表达式。使用 `--deps` 时：在 `--json` 输出中包含依赖图。使用 `--deps-out` 时：将图持久化到文件。
`llmll test <file>`	运行基于属性的测试（通过 QuickCheck 测试 `check`/`for-all` 块）
`llmll build <file> [-o <dir>]`	生成一个 Haskell 包（`src/Lib.hs` + `package.yaml` + `stack.yaml`）并用 `stack build` 编译它，或在 Stack 不存在时用 `ghc --make`。同时接受 `.llmll` S-表达式和 `.ast.json` JSON-AST 源。当 PATH 上既没有 `stack` 也没有 `ghc` 时它会失败（退出码 1）；`--emit-only` 会写出包而不编译它。
`llmll build-json <file.ast.json> [-o <dir>]`	将 JSON-AST 源编译为 Haskell 包：即读取 `.ast.json` 输入的 `build` 流水线。`--emit-only` 写出 Haskell 源但跳过内部 stack 构建；`--contracts MODE` 设置运行时断言模式（默认 `full`、`unproven`、`none`）。
`llmll run <file> [args...]`	编译程序并立即运行它；需要一个 `def-main`。该程序继承此进程的 stdin、stdout 和 stderr，且 `llmll run` 以程序自身的状态退出。末尾参数会传递给正在运行的程序，包括标志；仅当某个参数以 `-` 开头且不应被当作标志读取时，才需要 `--`。
`llmll verify <file> [--fq-out FILE] [--leanstral] [--leanstral-lean-project DIR] [--leanstral-mock] [--trust-report] [--weakness-check] [--obligations] [--obligation-report] [--spec-coverage] [--strict-verified-core] [--cdp] [--strict-verify] [--proof-artifact FILE]`	生成 `.fq` 约束文件并运行 `liquid-fixpoint`（若已安装）。使用 `--proof-artifact FILE` 时，还会写入一份统一的、可重放的验证记录，整合 trust/obligation/`.fq`/sidecar 各表面以及确定性固定项。使用 `--leanstral`（实验性）时，将非线性义务发送到实时 Leanstral 证明器，并用 Lean 内核检查返回的证明（见上文）；`--leanstral-mock` 针对模拟证明器运行同一流水线。使用 `--trust-report` 时，打印每个函数的信任摘要，包含传递闭包、认知漂移警告以及 `weakness-ok` 抑制（注意：`--trust-report` 会重新加载持久化证据而不是运行不动点，因此求解器可反驳的函数会渲染为 `asserted`，而非 `refuted`；请使用默认的 `verify` 或 `--strict-verified-core` 来暴露 `refuted`）。使用 `--weakness-check` 时，检测允许平凡实现的规格。使用 `--obligations` 时，在跨函数边界处 UNSAFE 时建议加强后置条件。使用 `--obligation-report` 时，为每个洞、未证明的契约以及失败的调用点前置条件生成结构化 JSON 义务报告。使用 `--spec-coverage` 时，对每个函数进行分类并计算有效规格覆盖率。使用 `--strict-verified-core` 时，若任何函数从体忠实验证回退、携带溢出污染的已验证证据，或被反驳（体忠实但被求解器证伪），则在调用图上传递性地硬报错，或触及一个未被证明的导入契约（回退、从未验证或此后已更改）。使用 `--cdp` 时，计算每个函数的契约区分能力：在信任报告 JSON 中，与现有证据轴并列输出一个配对的 `discriminative_axis` 块。使用 `--strict-verify` 时，一起运行 `--trust-report --weakness-check --spec-coverage --cdp`：推荐的严肃验证路径。
`llmll replay-artifact <FILE>`	重新推导并检查已记录的证明产物：重新计算源哈希，在固定求解器下重新运行存储的 VC，并在任何源/求解器确定性不匹配或 `unknown`/超时时故障关闭。
`llmll typecheck --sketch <file>`	部分程序类型推断。为每个 `?hole` 返回推断类型，外加 `holeSensitive` 标注的错误以及来自模式注册表的 `invariant_suggestions`。
`llmll serve [--host H] [--port P] [--token T]`	将 `--sketch` 暴露为面向智能体集群的 `POST /sketch` HTTP 端点。默认：`127.0.0.1:7777`。
`llmll checkout <file.ast.json> <pointer> [--multi N]`	锁定一个 `?hole` 以供智能体独占编辑。返回一个检出令牌，附带该洞的契约上下文（`contract_pre`、`postcondition_goal`、`path_condition`）和类型上下文（`in_scope`、`type_definitions`）。使用 `--release` 放弃，使用 `--status` 查询 TTL。使用 `--multi N` 时，打开或加入一个 R5 分歧会话：在一个指针上有 N 个并发草稿隔离令牌。
`llmll diverge-report <file.ast.json> <session>`	R5：收集分歧会话的填充并生成 `divergence_witness` 记录。会话 id 是 `checkout --multi` 返回的那个。求解器无法评分的填充（无求解器，或无判定）列在 `status_partition.unavailable` 下，记录携带 `solver_available`，命令以 3 退出。主体在可判定片段之外的填充列在 `status_partition.outside_fragment` 下，而非 `refuted`，且不改变退出码。
`llmll patch <file.ast.json> <patch.json>`	对已检出的洞应用 RFC 6902 JSON-Patch。在写入前对修补后的程序重新进行类型检查和重新验证（SMT）。被拒绝时以 1 退出，当求解器缺失或未返回判定时以 3 退出（`PatchVerifyUnavailable`，不写入任何内容）。成功时按修补的函数报告其主体是否被证明（`verification[].body_faithful`）；`--require-proof` 拒绝后置条件仅作为假设通过的填充（`PatchNotProved`）。
`llmll refine <file.ast.json> <refine.json>`	填充一个已检出的洞并原子性地生成其主体所调用的新契约子洞（级联分解）。生成的子契约通过可行性（无奇迹）门（任何主体都无法履行的子契约会以见证输入被拒绝）和 CDP 空洞性门；其契约包含某个生成的子契约的作用域内定义会作为建议性 `reuse_suggestions` 浮出（在完全契约等价时非阻塞 `W-REUSE`）。
`llmll hub fetch --from-file <tarball>`	将本地 `.tar.gz` 包安装到 hub 缓存中（`~/.llmll/modules/`）。仅限本地 tarball；没有按名称从 registry 拉取。
`llmll hub scaffold <template> [--output DIR]`	从 `llmll-hub` 骨架模板生成项目（`~/.llmll/templates/`）。
`llmll hub query --signature <sig>`	在 hub 缓存中搜索匹配类型签名的函数（例如 `"int -> int -> int"`）。
`llmll replay <source> <log>`	重建程序，重放事件日志输入，比较输出以进行确定性验证。
`llmll spec [--json]`	从编译器内建功能生成 agent 提示规范。文本（默认）或 JSON 输出。
`llmll version`	打印编译器版本并退出。支持 `--json` 以输出 `{"version":"…"}`。也可作为 `llmll --version` 使用。
`llmll repl`	启动交互式 LLMLL REPL

输入格式

两种源格式编译为相同的 AST 节点：

格式	扩展名	最适合
S-表达式	`.llmll`	人工编辑，简洁迭代
JSON-AST	`.ast.json`	AI agent——受 schema 约束，结构上天然有效

JSON-AST schema 位于 docs/llmll-ast.schema.json。

构建编译器

需要 GHC ≥ 9.4 + Stack ≥ 2.9。

cd compiler
stack build
stack exec llmll -- --help

→ 完整构建指南和已知良好模式：docs/getting-started.md

快速开始

cd compiler

# Check the example
stack exec llmll -- check ../examples/hangman_sexp/hangman.llmll

# Build a Haskell package in generated/hangman_sexp
stack exec llmll -- build ../examples/hangman_sexp/hangman.llmll -o ../generated/hangman_sexp

# Build from JSON-AST
stack exec llmll -- build ../examples/hangman_json/hangman.ast.json -o ../generated/hangman_json

# Run the generated game
cd ../generated/hangman_json && stack build && stack exec hangman

验证边界

LLMLL 为非递归 QF-LIA 核心提供体忠实（body-faithful）的 SMT 验证，并具备组合式调用链推理：整数和 bool 值、线性算术与比较、let 绑定、条件表达式、对已契约函数的调用（assume-guarantee，同文件或导入）、对非递归 sum 的 n 分支 match、pair、非递归数据类型构造、array 类（bytes[n] 和 map 操作）以及字符串字面量。该片段之外的程序回退到仅契约验证、基于属性的测试或运行时断言，每种都带有明确的信任标签。

构造	SMT 体忠实	回退
`ELit`、`EVar`（`int` / `bool`）、线性操作（`+ - = < <= >= > !=`）	✅	n/a
`ELet`（PVar）、`EIf`（≤4096 条路径）	✅（路径拆分）	n/a
`EApp`（已契约的被调用方，同文件或导入）	✅（assume-guarantee）	n/a
`EApp`（未契约的被调用方）	❌	仅契约
`EApp`（递归自身 / 循环）	✅ 部分；使用 `(decreases e)` 时 ✅ 完全	无 measure：`termination_unverified`；错误 measure：`measure-not-decreasing`
对非递归 sum 的 `EMatch`（`Result` 和用户 ADT，嵌套和顺序）	✅（n 元 int 标签）	n/a
`EPair` / pair 返回（`first`、`second`、`pair`）	✅（数据类型选择器）	n/a
非递归数据类型构造	✅	n/a
`bytes[n]` 和 `map` 操作（`bytes-get`/`-set`/`-length`/`-zero`、`map-has`/`-get`/`-put`/`-empty`）	✅（array 理论；索引在界内和键存在性是证明义务）	非 `{int,string}` 键、直接 `(map-empty)` 读取、整体结构 `=`：仅契约
`=` / `!=` 中的字符串字面量、字面量的 `string-length`	✅	字符串结构（concat、substring、regex）：仅契约
`EMatch`（递归 sum 载荷）、`ELambda`、`EDo`	❌	仅契约 / 运行时
`letrec`（自身 body VC）	❌	运行时 + `:decreases`
非线性操作（`*`、`/`、`mod`）	❌	运行时 + `?proof-required`（实验性 `--leanstral`）
Int 溢出	✅ 无缺口	`int` 在验证器和生成代码中都是无界的（`Integer`）

完整验证矩阵：LLMLL.md §5.3.5。

示例

从这里开始：examples/README.md 是每个示例的分层索引。

涌现式与著名 bug 旗舰示例

示例	它证明了什么
`examples/secure-channel-emergent/`	涌现式旗舰。一个 Heartbleed 领域的安全通道，25 个函数跨 7 个导入链接模块，其中 agent 通过级联 `refine` 发明了整个分解，没有参考解决方案；主干通过跨模块 assume-guarantee 组合六个模块，并拒绝了一个无引导的 goto-fail 诱饵
`examples/token-revocation-emergent/`	涌现式数据旗舰。一个 OAuth RFC 7662/7009 内省/撤销服务，8 个函数 / 5 个模块，其中契约（RFC `:source` 标记）和 agent 发明的函数体都可机器审计；5 个著名 bug 反驳孪生，CI 冻结
`examples/heartbleed/`	Heartbleed（CVE-2014-0160）+ 完整的 TLS 记录层：那个有缺陷的心跳回显了无界的 `claimed` 长度，在 `refuted` 处受 `copy-bytes` 约束；可扩展至 163 个函数的通道
`examples/gotofail/`	Apple "goto fail"（CVE-2014-1266）用真正的和类型建模：仅当签名阶段返回 `Continue` 时才 `Verified`；该缺陷（在 `Abort` 分支上返回 `Verified`）是 `refuted`

验证演示（`llmll verify`）

演示	它证明了什么
`examples/payments-core/`	旗舰示例。在一对返回值（`conserve`）上的双账户守恒——“钱不能被创造”；`transfer` 在 `debit` 调用边上得到验证（无透支）；`settle` 是一个 `Result` 匹配返回
`examples/tcp_rfc793/`	RFC 793 连接状态机在合法后继安全性上达到 `verified`；`step-bad` 是 `refuted`
`examples/session-pay/`	互联演示：协议状态安全性 + 已验证支付 + 有界金额，全部在一个 `verified` 函数中
`examples/nested-result/`	一个嵌套的 `Result` 变量匹配（在 `let` 下）达到 `verified`
`examples/refined-payload/`	一个匹配的 `Result[Pos,string]` 分支使用其载荷的 `> 0`（`verified`）；转发较弱 `Result[int]` 的调用者会被拒绝
`examples/outcome-totality/`	一个携带载荷的 `Accepted(n)`/`Rejected(n)` 结果，具有已验证的合法→Accepted / 非法→Rejected 完备性
`examples/banking_ledger/`	三级 assume-guarantee 链（`transfer → withdraw → safe-subtract`），全部已验证；丢弃一个守卫的孪生版本在调用点处是 `refuted`
`examples/withdraw-demo/`	修复循环（漏洞 → 被拒绝的错误填充 → 被接受的修复 → 已验证）+ `return-refine` 节拍
`examples/refine-demo/`	级联 `refine`：一个漏洞自顶向下分解为带契约的子漏洞树，每个中间状态都通过 assume-guarantee 达到 `verified`；两条护栏拒绝空洞或孤立的分解
`examples/bytes-bounds/`	`bytes[n]` 内存安全：正确的边界检查通过验证；差一错误（对 `<` 而言的 `<=`）和越界写入在调用点处是 `refuted`
`examples/total-recursion/`	一个带 `(decreases n)` 的递归函数验证为 total（终止性已消解）；错误的度量在独立的 `measure-not-decreasing` 通道上失败
`examples/rfc1982_serial/`	通过 spec-from-RFC 流水线实现的 RFC 1982 序列算术：全部三个函数 `verified`，并带有逐子句的 `:source`；历史上的朴素 `<` DNS 缺陷被反驳

语言 / 运行时示例

示例	格式	描述
`examples/hangman_sexp/`	S-表达式	完整的 Hangman 游戏，带 ASCII 绞刑架图案；使用 `def-main :mode console`
`examples/hangman_json/`	JSON-AST	同一程序，JSON-AST schema 约束版本
`examples/tictactoe_sexp/`	S-表达式	双人井字棋；演示 `:done?` + `:on-done`
`examples/life_sexp/`	S-表达式	康威生命游戏；多模块（`core`、`world`、`main`）
`examples/life_json/`	JSON-AST	同一 Life 程序的 JSON-AST 格式
`examples/withdraw.llmll`	S-表达式	带 `pre`/`post` 契约的简单取款；验收门
`examples/hangman_json_verifier/`	JSON-AST	带 `apply-guess` 契约的 Hangman（`llmll verify`；已断言，非求解器证明）
`examples/tictactoe_json_verifier/`	JSON-AST	带 `set-cell` 契约的井字棋（已断言，非求解器证明）
`examples/conways_life_json_verifier/`	JSON-AST	康威生命游戏——`next-cell`/`count-neighbors` 契约（见其 `VERIFICATION_SCOPE.md`）
`examples/replay-demo/`	S-表达式	`llmll replay` 演示：代码生成 + 确定性事件日志重放（由 `docs/getting-started.md` 使用）
`examples/proof_required_test/`	S-表达式	Leanstral 证明流水线验证
`examples/erc20_token/`	JSON-AST	ERC-20 基准——冻结的基准真值，带验证范围矩阵
`examples/totp_rfc6238/`	JSON-AST	TOTP RFC 6238 基准——加密内置函数，RFC `:source` 溯源

仓库布局

LLMLL.md                    ← canonical language specification
CHANGELOG.md                ← release notes
compiler/                   ← Haskell compiler (stack project)
  src/LLMLL/
    Parser.hs               ← S-expression parser (Megaparsec)
    Lexer.hs                ← Megaparsec lexer (tokens, whitespace, layout)
    ParserJSON.hs           ← JSON-AST parser
    Syntax.hs               ← AST types (incl. ModulePath, ModuleEnv, ModuleCache, TPair)
    TypeCheck.hs            ← Bidirectional type checker
    HoleAnalysis.hs         ← Hole collector (?hole expressions)
    CodegenHs.hs            ← Haskell code emitter
    AstEmit.hs              ← JSON-AST emitter (--emit round-trip)
    Contracts.hs            ← Runtime contract assertion generator
    PBT.hs                  ← QuickCheck property runner
    Diagnostic.hs           ← Structured error/warning types
    Module.hs               ← Multi-file module resolver, cycle detection, ModuleCache
    Hub.hs                  ← llmll-hub local package cache (tarball install) and scaffold
    Sketch.hs               ← Partial-program type inference (--sketch)
    Serve.hs                ← HTTP endpoint for agent swarms (llmll serve)
    FixpointIR.hs           ← .fq constraint IR + text emitter
    FixpointEmit.hs         ← typed AST → .fq + ConstraintTable builder
    DiagnosticFQ.hs         ← liquid-fixpoint output → [Diagnostic] with JSON Pointers
    Replay.hs               ← JSONL event log parser + replay execution
    LeanTranslate.hs        ← LLMLL contracts → Lean 4 theorem obligations
    MCPClient.hs            ← Leanstral client (Mistral API over HTTPS; mock-first)
    ProofCache.hs           ← per-file .proof-cache.json sidecar (SHA-256)
    TrustReport.hs          ← transitive trust closure analysis (--trust-report)
    VerifiedCache.hs        ← .verified.json sidecar read/write
    WeaknessCheck.hs        ← trivial-body spec weakness detection
    InvariantRegistry.hs    ← pattern-based invariant suggestion database
    ObligationMining.hs     ← downstream postcondition strengthening suggestions
    ObligationAssembly.hs   ← structured obligation report assembly + JSON encoding
    GuardClassifier.hs      ← shared guard classification (verifier + obligations)
    SpecCoverage.hs         ← specification coverage metric + governance guardrails
    JsonPointer.hs          ← RFC 6901 pointer resolution + descendant hole search
    Checkout.hs             ← Hole checkout with per-file lock management (llmll checkout)
    PatchApply.hs           ← RFC 6902 JSON-Patch application with scope validation + re-verification (llmll patch)
    AgentSpec.hs            ← Compiler-emitted agent spec for LLM system prompts (llmll spec)
    HubQuery.hs             ← Query-by-signature: find hub modules matching a type signature (llmll hub query)
    CDP.hs                  ← contract discriminative power evidence axis (--cdp)
    ProofArtifact.hs        ← unified, replayable verification record (--proof-artifact / replay-artifact)
  package.yaml / stack.yaml
examples/
  hangman_sexp/             ← Full Hangman (S-expression)
  hangman_json/             ← Full Hangman (JSON-AST); getting-started.md's worked example
  tictactoe_sexp/           ← Tic-Tac-Toe (S-expression)
  life_sexp/                ← Conway's Life (S-expression, multi-module)
  life_json/                ← Conway's Life (JSON-AST, multi-module)
  withdraw.llmll            ← Contract demo
  hangman_json_verifier/    ← Hangman with contracts (asserted, not solver-proven)
  tictactoe_json_verifier/  ← Tic-Tac-Toe with contracts (asserted, not solver-proven)
  conways_life_json_verifier/ ← Life with contracts (see its VERIFICATION_SCOPE.md)
  erc20_token/              ← ERC-20 benchmark (frozen ground truth)
  totp_rfc6238/             ← TOTP RFC 6238 benchmark
  benchmarks/               ← agent-fill benchmark seeds (B1/B3/B5)
  secure-channel-emergent/  ← emergent flagship: 25 fns / 7 modules, agents invented the decomposition
  token-revocation-emergent/ ← emergent data flagship: RFC 7662/7009, agent-invented bodies, 5 refute twins
  heartbleed/               ← Heartbleed (CVE-2014-0160) + TLS record layer; scales to a 163-fn channel
  gotofail/                 ← Apple "goto fail" (CVE-2014-1266) with real sum types
  payments-core/            ← flagship verified-payments demo: two-account conservation, transfer/debit call chain, settle (see "See it")
  withdraw-demo/            ← repair-loop demo: holes → checkout/patch → two-axis trust + composition + CDP + proof-artifact
  refine-demo/              ← cascading refine: one hole → contracted sub-hole tree, each state verified
  tcp_rfc793/               ← RFC 793 connection state machine, legal-successor safety
  session-pay/              ← Connected demo: protocol state-safety + verified payment + bounded amount in one verified function
  nested-result/            ← Nested Result-variable match under let
  refined-payload/          ← Matched Result payload refinement + weaker-forward refusal
  outcome-totality/         ← Payload-carrying outcome sum, verified legal/illegal totality
  banking_ledger/           ← Three-level assume-guarantee chain (transfer → withdraw → safe-subtract) + refuting twin
  orchestrator_walkthrough/ ← Auth module orchestration exercise
docs/
  UPDATE-PROTOCOL.md        ← Doc canonical-sources + per-change update matrix
  getting-started.md        ← Build guide, known-good patterns, schema versioning
  compiler-team-roadmap.md  ← Engineering backlog and shipped-releases history
  llmll-ast.schema.json     ← JSON-AST schema (use with AI agents)
  orchestrator-walkthrough.md ← End-to-end orchestration walkthrough
  one-pager.md              ← Project overview / pitch document
  design/                   ← Active design proposals (status in design/INDEX.md)
    INDEX.md                ← Reading guide for active design documents
  archive/                  ← Superseded design specs, shipped proposals, professor reviews, wasm investigations
tools/
  llmll-orchestra/          ← Python orchestrator (pip package)
    llmll_orchestra/
      orchestrator.py       ← Fill-mode orchestrator
      lead_agent.py         ← Lead Agent skeleton generation (plan/lead/auto modes)
      quality.py            ← Skeleton quality heuristics
      agent.py              ← LLM agent interface
      compiler.py           ← Compiler CLI wrapper

文档

文档	用途
`LLMLL.md`	完整语言规范——类型、语法、FFI、文法、内置函数
`docs/README.md`	`docs/` 阅读指南：先读什么，以及哪些是工作材料
`ROADMAP.md`	公开路线图：已发布内容、下一步计划、刻意划定的边界
`experiments/README.md`	实验索引及其头条结果
`docs/getting-started.md`	构建指南 + 已知良好模式 + schema 版本管理（面向代理的单一参考）
`docs/compiler-team-roadmap.md`	工程待办事项和已发布版本历史（当前版本见 CHANGELOG § Latest）
`docs/llmll-ast.schema.json`	机器可读的 JSON-AST schema
`docs/UPDATE-PROTOCOL.md`	文档规范来源表与逐项变更更新矩阵
`docs/orchestrator-walkthrough.md`	端到端多智能体编排演练，含认证模块练习
`docs/one-pager.md`	项目概述——问题、方法、状态、相关工作
`docs/design/INDEX.md`	所有现行设计文档的阅读指南
`CHANGELOG.md`	按版本划分的发布说明

许可证

GPLv3 及 LLMLL 运行时库例外——见 LICENSE。