本章建立如下命题：Coding Agent 的 harness 设计，本质上是在构造一个形式系统。提示词工程师选择公理，工具接口定义签名，运行时路由提供解释函数，验证逻辑执行模型检查，扩展机制实现理论扩充。这不是比喻——这些术语在模型论中的精确含义直接映射到代码结构。

2.1 系统提示词作为理论 $T$

在一阶逻辑中，理论（theory） $T$ 是语言 L 中的一组句子（sentences）的闭包。每个句子通过逻辑连接词和量词约束着结构中谓词与函数的解释。在 Agent 系统中，系统提示词就是 $T$ 的载体——它规定了 Agent 的身份公理、协议规则、工具偏好和约束条件。LLM 的每一次推理输出构成了一个结构 $M$；当会话正确运行时，我们期望 $M ⊨ T$。

2.1.1 DS-TUI：单体公理化与 264 行公理系

DeepSeek-TUI 的系统提示词集中在 base.md 中——约 264 行的单体文件，通过 include_str!() 在编译时嵌入二进制。这种单体策略的核心优势是理论一致性：所有公理在同一逻辑空间中定义，无跨文件依赖导致的隐含不一致风险。

base.md 的公理可按逻辑类型归类：

身份公理定义模型 M 的存在性前提：

You are DeepSeek TUI. You're already running inside it.
Do not launch a nested interactive `deepseek` session
unless the user explicitly asks.

这引入了约束 $¬∃x (IsNestedSession(x))$——模型必须承认自己已在 TUI 内部运行，禁止递归启动。

协议公理定义推理规则：

PREVIEW — Before diving into a large task, survey the terrain.
CHUNK + map-reduce — split into independent sub-tasks.
RECURSIVE — decompose recursively until each leaf is tractable.

三种分解模式、验证纪律（verify before proceeding）、路径安全检查（resolve_path）以条件语句的形式约束了推理路径的选择。

工具箱公理定义函数符号的偏好排序：

### `apply_patch`
Use `apply_patch` for structural edits, coordinated changes,
or cases where line context matters. Use `write_file` for
brand-new files, full-file rewrites...

这是一个函数选择公理：对于 $c ∈ Category$，应使用 $f_C$ 而非 $g_C$。它定义了语言 L 中的标准模型约束——不是”什么可以做”，而是”做什么时应该用什么工具”。

验证公理施加证据门槛：

After every tool call that produces a result you'll act on,
verify before proceeding:
-File reads: confirm the line numbers...
-Shell commands: check stdout, not just exit code...

这是理论 $T$ 中最强的约束之一：模型不能仅凭工具名就信任结果，而必须检查输出内容。它引入了一种认知验证义务——M 必须在完成任务之前产生可观察的验证证据。

缓存感知公理是元理论层级的约束：