注意：如果你是从 Hacker News 来的，(1) 是的，这全是 vibe-coded 的；(2) 关于该项目更易读的说明可以在这里找到：https://github.com/emmilco/us-tax-model/blob/main/spec/spec.md
美国联邦个人所得税的表格与说明层，作为公开、有引用、可机器校验的数据，并以一个引导式自助申报访谈作为其首个客户端。该访谈向个人提问，判断适用哪些表格，进行计算，解释每一个数值，并交回一份数值表，由个人自行提交。该软件从不提交、签署或传输申报表，且没有任何申报数据离开本机。所编码的是 IRS 已发布的流程，而非《国内税收法典》。
为什么你可以检查它
该编码主要由语言模型智能体编写，因此不能因为作者是谁就信任它；它的构建方式使得真正重要的部分可以由一个不信任任何作者的人仅凭仓库本身进行核查。每一层都说明它是什么、它保证什么、它不保证什么，以及该去哪里查看。
1. 表格即数据，每一行都有引用
每个表格或工作表都是位于以下路径下的 YAML 文件forms/<year>/。一行就是一条记录：id、印刷行号、IRS 标签、类型、一个表达式，以及一条引用，指明文档、纳税年度、修订版本、定位符，以及归档页面在以下路径下的哈希sources/<year>/它读取自（spec/spec.md第 5 节）。保证：如果任何行、参数、门控或问题缺少引用，或引用了清单中不存在的哈希，构建就会失败，并且tools/citations.py会对照归档文本校验每一处引文和定位符；reports/2025/citations.md报告了 2,313 个锚点和 1,252 条引文，0 条没有记录裁决的发现，以及 305 个过于粗略而无法校验的计算行定位符片段。不保证：表达式所表达的内容与所引用页面所述一致。引用只能证明某一行指向了某个页面，而不能证明它被正确读取。
2. 封闭的原子词汇表
每个计算行都是对以下列表中某个原子的一次应用spec/spec.md第 4.2 节（sum、subtract_floor0、smaller_of、multiply_rate、round、table_lookup、choose以及其他十几个）；不存在用户自定义函数、循环、变量、字符串或递归。保证：数据的全部含义就是大约二十个操作的含义，每个操作都小到可以通读；唯一的例外，opaque，一个宿主语言函数，被计数并发布，并且reports/2025/coverage.md报告 0 个，共 2,384 行使用了它。不保证：为某一行选择了正确的原子。
3. 构建时检查器
engine/src/check.ts会使构建失败，除非每个copy、操作数和param引用都在所述修订范围内解析；行图是无环的；每个表达式都通过类型检查（分、费率、计数和布尔值不会混用）；每个choose都有穷尽且互斥的守卫，由枚举和区间分析判定；并且第 1 层的来源规则成立（spec/design.md第 2.3 节）。保证：数据中任何地方都没有悬空引用、循环、单位混淆，或受守卫备选方案中的间隙或重叠。不保证：与 IRS 文本一致；一个通过类型检查的错误操作数会通过。
4. 渲染器
每个原子都有一个采用 IRS 工作表措辞的英文模板，渲染器将每一行的英文写在 IRS 标签和引用旁边，写入rendered/<year>/，该文件被提交。保证：非程序员可以对照打印表格阅读任何一行，并且对数据的更改在审查中会以可读的英文差异形式出现。不保证：有人真的做过这种阅读。
5. 整数运算
金额是整数分，费率是整数对，求值器（engine/，BigInt）没有浮点数。舍入只发生在round原子中，只在被引用的指令要求舍入的地方，按照其规定的规则（spec/spec.md第 3 节第 10 项）。保证：每个值都是精确的，并且每次舍入都有引用。不保证：IRS 本意是让其算术精确；在文本对舍入留有开放之处时，所选择的解读在ambiguities/<year>.yaml中。
6. Lean
lean/TaxFormalization/在整数上定义每个原子（Atoms.lean），证明第 6.3 节的性质（spec/spec.md：Lemmas.lean，subtractFloor0_nonneg，roundHalfUpToUnit_idem，prorate_le_amount），并且有一个与 TypeScript 版本使用相同规范 JSON 的参考求值器，已证明其终止且具有确定性（EvalProps.lean）。两个求值器都在每个 fixture 和生成的返回上运行；reports/2025/evaluator_agreement.md报告 1,648 个案例，比较了 2,895,826 个行值，0 处差异。保证：原子按规范行事，并且同一数据的两个独立编写的求值器计算出相同的值。不保证：关于数据是否与 IRS 文本匹配的任何事情。两个求值器读取相同的文件，因此一致性表明求值器一致，而不是数据正确。BUG_INVENTORY.md条目 BUG-0001 是典型案例：Form 1040 第 9 行把第 3a 行和第 3b 行一起求和；每个 fixture 和两个评估器都认可了这个错误的和；一个外部引擎发现了它。
7. 独立构造
不声称进行了全面的人工逐行阅读，因此项目用一些构造来补充可选的阅读，这些构造除了归档页面之外没有任何共同点（spec/spec.md第 6.5 节）：由隔离模型仅给定页面和 schema 对每个工作表进行第二次转录，并与项目的转录逐原子比较；渲染比较，其中未见 YAML 的隔离模型将每一行的英文与页面进行对照阅读；class M 手工工作，其中隔离模型在打印的工作表上处理覆盖分支的输入；以及在编码运行之前对整个申报表数值进行的盲预测。每个模型运行时无仓库访问、无网络（tools/transcription/README.md）；每一处分歧都依据源文件裁定，并记录页面和引文，日志提交在reviews/2025/。保证：对于每一行，同一页面的两次阅读产生了相同的结构，或者差异已连同其裁定记录在案。不保证：阅读者的独立性。
8. 引擎
tools/engines/生成完整申报表并通过三个引擎运行它们：PolicyEngine-US 2.49.4、Tax-Calculator 6.8.5 和 OpenTaxSolver 23.06，在引擎计算某一行的范围内逐行比较；reports/2025/engine_differential.md覆盖 1,700 份申报表。每一处差异都必须解释到有引用的原因，否则运行失败；从不接受误差范围，当前报告未列出任何未解释的差异。行级 OpenTaxSolver 适配器已在使用；UsTaxes 仍有待添加，见docs/2026-10-22_integrity_plan.md。保证：引擎得出的汇总行与其他人员根据规则编写的代码一致。不保证：引擎不计算的任何工作表行；前两个主要达到汇总行，而 OpenTaxSolver 也达到工作表行。
9. 证据报告和记分板
reports/2025/evidence.md列出每一行以及断言它的证据类别（A，官方 IRS 示例；B，人工手工工作；C，具名的外部计算器；M，隔离模型手工工作；H，人工源阅读；E，引擎；R，项目自身的回归；spec/spec.md第 6.1 节）。其第一行是记分板，即计算行中至少含有一条来自 Claude 模型家族之外断言的比例。2026-10-24 重新生成的报告显示为 1,515 条中的 198 条（13.1%）；H：0，B：0，第二家族 M：44，E：163（各子计数存在重叠）。这反映的是跳过响应审计之后记录的数值断言；它并不确立完整表单或整份申报的覆盖。Form2441 的三个缺失 STOP 输出仍未计入，其表单级审查仍待进行。可选的人工发现不再阻止报告生成。本次报告刷新不是一次新的全套件通过。保证：任何一行背后的证据都可查，且项目正在推动的那个数字被印在最前面。H 为一次来源阅读记入信用，需有当前回执及其具名阅读者提交的确切日志；它不提供任何已算出的值，也从不填充 B。所有者完成了第一个数据包；原始发现被保留，当前 H 信用仍为零。进一步的人工数据包与裁定样本在2026-10-24 政策修订下为可选。不保证：仅含 A、Claude 家族 M 或 R 断言的一行已由单一模型家族之外的任何人检查过。
10. 变异测试、属性、访谈检查
变异工具对数据施加单原子变异（交换smaller_of为larger_of、删除一个下限、更改一个操作数），并询问检查器或测试夹具是否察觉；reports/2025/mutation.md报告 2,278 个变异体，128 个存活，每个都附有书面的等价性证明，因此原始为 94.4%，排除等价项后为 100.0%。属性测试在 400 份生成的申报上检查规范 6.3 的数据级属性；reports/2025/properties.md报告 8 条属性，全部成立。访谈的有限路径检查（engine/，spec/spec.md第 6.4 节）枚举答案组合：每条路径都以完整的表单集或引用的拒绝告终，答案顺序不改变申报，且不会提出其答案无法到达任何一行的问题。保证：测试夹具对其声称测试的数据敏感，所述不变量成立，且访谈没有死胡同。不保证：任何变异无法表达或测试夹具已错误编码的内容（又是 BUG-0001）。
11. 缺陷清单与提交守卫
BUG_INVENTORY.md记录任何检查或阅读所捕获的每一个缺陷，在其修复之前或同时记录：它是如何被捕获的、症状、根本原因、为什么现有检查漏掉了它、修复及其提交。它是仅追加的；check-all如果已提交的前缀发生变化，或 id 不是连续的，则失败。tools/hooks/pre-commit拒绝任何树不是最后一次绿色通过的树的提交npm run check-all经过测试，并且一次运行只有在运行期间其自身输出之外没有任何变化时才算绿色（tools/README.md，“提交守卫”）。保证：缺陷记录无法被编辑，并且没有任何提交会在整个测试套件未在该确切树上通过的情况下落地。不保证：测试套件能捕获它未测试的内容；“为何存活”字段的存在是为了将每一次这样的遗漏转化为一项新检查。
这并未确立什么
来自spec/spec.md第 3 节，第 11 项：人工源码阅读覆盖范围仅限于逐行证据记录；独立构建及其记录的分歧提供了更广泛的验证。报告识别出符合条件的家族外断言以及每一项的来源。未完成的验证被报告为缺口；采纳该要求并不确立其已完成。
最初的 layer-7 构建使用了一个模型家族，Claude。Flash 现已完成对所有 55 种表单的转录和渲染调用，并处理了六个活跃的 Form 2441 案例和一个 W-2 申报表。仍存在许多来源分歧，以及在 Form2441 STOP 之后出现的三个空白数值输出；第二个家族尚未被提升。重新生成的记分板在已记录的引擎和第二家族已处理值断言中计入了 198 行计算行；完整表单覆盖仍单独统计。当前源码阅读资格在reports/2025/second_family.md转录/渲染读数受各自的门控约束。BUG-0129 暴露了转录比较器中的单元擦除问题；在审计该缺陷及先前协议之前，转录资格认定暂缓。模型演算值与外部引擎断言与此暂缓无关。源读数单独报告，尚未接入记分板。修订后的完整性计划加强了第二家族与引擎检查，人工读数可选。在线税务解释被记录为非权威性佐证，依据research/secondary/；它不获得记分板分数，并与仅基于源数据的盲测模型请求保持分离。
IRS 表格和说明并非法律。它们嵌入了关于《国内税收法典》的未公开判断，本项目将已发布的程序（包括其中的判断）编码实现；当文本存在歧义或未作规定时，所选择的解读记录于ambiguities/<year>.yaml，并在影响用户申报表时向用户展示。没有律师审查过本项目所依据的法律立场（spec/spec.md第 9 节）。
范围与覆盖
所计算的表格和行项目列于spec/spec.md第 2.1 节，被拒绝的情形及引用说明见第 2.2 节，其余新增项的顺序见第 2.4 节；该工具从不静默拒绝。覆盖率以整份申报表为单位衡量（仅当申报表上没有任何项目被拒绝时才计入），由tools/coverage/estimate.py计入reports/2025/filer_coverage.md，目前覆盖 68.6% 的个人申报表。其注意事项：157 个拒绝门控中有 148 个未被测量（无 IRS 计数或微观数据变量），因此该数字仅反映已测量的情形，真实覆盖率因未测量门控所占份额而更低。
如何运行全部流程
一条命令即可重建数据、运行所有检查并记录受测代码树：
npm install npm run check-all
前提条件，如首次检查工具链时所查验（tools/README.md，“工具链已查验”）：Node 与 npm；通过 elan 安装的 Lean 4（lean/lean-toolchain固定版本）及 Lake；Poppler 的pdftotext；带 PyYAML 的 Python 3；curl；以及，为提取检查中 PDFKit 对 PDF 的读取（tools/extraction/pdfkit_text.swift），需要带 Swift 工具链的 macOS。该检查在全新克隆上离线运行。引擎差分（tools/engines/README.md）需要安装两个外部引擎，并tools/engines/setup.sh，这是唯一的网络步骤；没有它们，该步骤会被明显跳过，检查也不会被声明。提交守卫是一个 git hook，通过git config core.hooksPath tools/hooks启用。
常驻提示
在首次运行时以及每次输出时显示（spec/spec.md第 8 节）：
- 这不是税务或法律建议。
- 用户对申报表负责。
- 该工具实现了已发布的 IRS 表格和说明，而这些本身并非法律。
- 它与 IRS 无关联，也未获其认可。
- 其覆盖范围与不覆盖范围的清单（见上文）。
各部分的位置
PROJECT_INDEX.md列出了每个目录、其内容以及命名约定。HANDOFF.md以及当前的HANDOFF-STAGE-*.md是继续构建的会话的阅读顺序。
许可证
代码依据 Apache License, Version 2.0（LICENSE）授权。数据依据 CC0 1.0 Universal 贡献至公有领域（LICENSE-DATA）：forms/，params/，tables/，fixtures/，ambiguities/以及interview/。位于以下路径的归档 IRS 来源sources/是 IRS 出版物。