第一个可核查案例：核对一张采购单

十分钟跟做：让智能体核对一张采购单——材料上板、立一条规则、板精确算出金额、每条结论带依据，再用目标看板怎么报缺口。全程只用今天云端已开放的能力（逐项记录见现况页），可以原样照抄。

场景

采购单两行：钢筋 3850 元 × 12，水泥 420 元 × 80。要求很朴素：每行金额由板算出来，不由模型报；算完之后，每个数都能问"凭什么"。

第一步：把材料和规则交给智能体

前提：已按5 分钟上手接好客户端。对智能体说（可原样复制）：

用 rulith 记下这几行订单（钢筋 3850×12、水泥 420×80），立一条"金额=单价×数量"的规则，让板推出每一行的金额，再把材料、规则、结论和直接依据列给我看。

它会把两行材料与一条规则写上板。落板的真实形状（智能体替你写的 JSON，你不必手写；想手写也可以，字段见参考）：

{ "operations": [
  { "op": "assert_fact", "id": "L1", "predicate": "line",
    "args": { "item": "钢筋", "unit": 3850, "qty": 12 } },
  { "op": "assert_fact", "id": "L2", "predicate": "line",
    "args": { "item": "水泥", "unit": 420, "qty": 80 } },
  { "op": "add_axiom", "id": "ax_cost", "label": "金额 = 单价 × 数量",
    "when": [
      { "predicate": "line", "args": { "item": "?i", "unit": "?u", "qty": "?q" } },
      { "predicate": "mul",  "args": { "left": "?u", "right": "?q", "result": "?t" } }
    ],
    "then": [ { "predicate": "cost", "args": { "item": "?i", "total": "?t" } } ] }
] }

第二步：板推出结论，每条带依据

cost(item=钢筋, total=46200) [derived] <- ax_cost, L1
cost(item=水泥, total=33600) [derived] <- ax_cost, L2

46200 和 33600 不是模型报的，是板精确算出来的（±2⁵³ 内不舍入，算不准会明确报错而不是给近似值）。<- ax_cost, L1 就是依据：哪条规则、哪项材料。单价录错了，顺着依据一眼看到是哪条材料的问题；规则写错了，看到的是规则本身。

打开控制台的智能体页，同样能看到这四样：材料、规则、结论、依据。

第三步：用目标看它报缺口

再声明一个目标，看板怎么对待"还没做完的事"。对智能体说"立一条'核价通过才算定价'的规则，再声明目标：钢筋这一项已定价"，落板形状：

{ "operations": [
  { "op": "add_axiom", "id": "ax_priced", "label": "核价通过才算定价",
    "when": [ { "predicate": "checked", "args": { "item": "?i" } } ],
    "then": [ { "predicate": "priced",  "args": { "item": "?i" } } ] },
  { "op": "declare_goal", "id": "G1", "label": "钢筋已定价",
    "desired": [ { "predicate": "priced", "args": { "item": "钢筋" } } ] }
] }

板会如实回答目标状态——目标没达成，缺口具体到差哪一步：

goals:
- G1: priced(item=钢筋) [open] (钢筋已定价)
-   needs via ax_priced: checked(item=钢筋)

这里的物料名 钢筋 与第一步的材料逐字相同，不是巧合：板按标识精确匹配，不做模糊匹配——写成 steel 的目标与写成 钢筋 的材料是两件东西，命令照样被接受，但永远推不出结果。

若你没有立那条 ax_priced 规则就直接声明目标，板会换一句话回答，同样是可执行的下一步：

goals:
- G1: priced(item=钢筋) [open] (钢筋已定价)
-   no rule derives this yet: add_axiom whose "then" matches it, or assert the fact directly

[open] 不是失败，是诚实：目标翻成 [satisfied] 的唯一方式，是推导真的支持它——说得再流畅也不算数。智能体的下一步不靠猜，照着缺口去补材料或补规则即可。

这个案例证明了什么

• 数是算的：结论由规则＋材料推出，模型没有机会把"差不多是这个数"混进来；
• 错可定位：依据链把问题钉到具体一条材料或一条规则，不散落在对话里；
• 缺口明说：没做完就挂 [open]，差什么逐条列出，不因为没人反对就算过。

走完之后

• 换成你自己的制度：编写领域能力（现成的先装上：使用领域能力）；
• 让证据从你的真实系统进板（实证档，模型伪造不出）：接入传感器；
• 想看一件完整的事——缺料、挑错、拦截、放行、回放——怎么走：完整架构案例。