文章介绍了 Theoric Labs 的 LeanDB 实验，旨在将形式化方法与 AI 智能体结合应用于数据库领域：用 Lean 语言描述数据及其属性，同时使用 SQL 数据库进行存储和查询。文章通过咖啡菜单示例系统讲解了 Lean 的类型系统，包括归纳类型（如 Temperature、MenuItem）、细化类型（如限制浓缩咖啡份数为 1-4 的 ShotCount 子类型）、依赖类型（杯型大小依赖于冷热温度的 CupSize 索引族），以及元类型（FieldSpec 宇宙设计模式，用数据描述类型）。作者认为，强类型能让编译器在运行前阻止非法数据写入，将验证结果显式化，从而构建无 bug 的软件系统。
Ars Umbris 是一款可塑的 Agent 原生 IDE，将知识库视为代码库，通过类型引擎为笔记、来源等知识对象定义类型与关系，并像编译器一样对知识结构进行校验。其仓库以本地 Markdown/YAML 文件组织，包含知识、类型、技能、MCP 工具、投影与 Agent 配置，支持跨仓库引用与依赖复用。它通过 MCP 适配器连接 Claude Code、Codex 等 Agent 框架，让多个会话共享同一份持久化状态，形成「元 harness」。项目目前处于早期 Alpha，仅支持 macOS 且需自行编译。
文章探讨如何让人们对 AI Agent 承担更重要的工作建立信任。作者提出需要让 Agent 在工作过程中留下“回执”——即不可变的、有类型的工作工件（如证据、假设、评估、建议、审批等）。通过将“工作本身”建模为产品的一等数据，定义工件类型及其依赖关系，并强制 Agent 遵守这些结构（如建议必须基于评估、评估必须引用证据），系统能客观验证工作是否真正完成，而非依赖 Agent 自述。工件不可变可保留决策演变过程，且每个工件需指明所用上游工件的精确版本，从而形成可审计、可信任的工作链路。
