Show HN：IRS聯邦稅表概念驗證工具

美國聯邦個人所得稅的表格與說明層作為公開、可引用、可機器檢查的資料，首個客戶是引導式自我準備面談。面談向個人提問，決定適用哪些表格，計算它們，說明每個數值，並交回一份由該人自行提交的數值表。軟體永不提交、簽署或傳輸申報，亦不會有任何申報資料離開機器。編碼內容是 IRS 公佈的程式，而非《國內稅法》。

為何你能檢查它

編碼主要由語言模型代理撰寫，因此無法因為作者而被信任；它的構建方式讓重要內容可僅從倉庫自行檢查，且不需信任任何作者。每一層都說明其功能、保證、未保證之處，以及檢查位置。

1. 表格作為資料，每行都有引用

每個表格或工作表都是位於 forms/<year>/ 下的 YAML 檔。每行為一筆記錄：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 報告 2,384 行中 0 行使用它。未保證：為某行選擇了正確的原子。

3. 建置時檢查器

engine/src/check.ts 只有在每個 copy、運算元和 param 參照均在指定修訂內解析時才會成功建置；行圖無迴圈；每個表示式均通過型別檢查（分別為分、比率、計數和布林值，互不混合）；每個 choose 都擁有完整且互斷的保護條件，由列舉與區間分析決定；並且層 1 的來源規則得到遵守（spec/design.md 第 2.3 節）。保證：資料中不會有懸空引用、迴圈、單位混淆，或任何受保護選項中的缺口或重疊。未保證：與 IRS 文本一致；錯誤的運算元即使通過型別檢查亦會通過。

4. 渲染器

每個原子都有一個英語範本，符合 IRS 工作表措辭；渲染器將每行的英語寫入 rendered/<year>/，並附上 IRS 標籤與引用，該檔案已提交。保證：非程式設計師即可將任何行與列印表格對照閱讀，且資料變更會以可讀的英語差異顯示於審查。未保證：有人已進行此閱讀。

5. 整數算術

金錢以整數分為單位，匯率以整數對表示，評估器（engine/、BigInt）沒有浮點數。四捨五入僅在 round 原子中發生，僅在引用的指令要求四捨五入時，根據它所述的規則（spec/spec.md 第3節，第10項）進行。保證：每個值都精確，且每次四捨五入都有引用。未保證：IRS 是否意圖其算術精確；若文本留有四捨五入空間，所選閱讀方式見 ambiguities/<year>.yaml。

6. Lean

lean/TaxFormalization/ 在整數上定義每個原子（Atoms.lean），證明 spec/spec.md 第6.3節的性質（Lemmas.lean：subtractFloor0_nonneg、roundHalfUpToUnit_idem、prorate_le_amount），並擁有一個參考評估器，與 TypeScript 版的相同標準 JSON，已證明終止且確定性（EvalProps.lean）。兩個評估器都對每個測試樣本和生成的回報進行評估；reports/2025/evaluator_agreement.md 報告 1,648 個案例，2,895,826 行值對比，差異 0。保證：原子按規定運作，兩個獨立編寫的相同資料評估器計算出相同值。未保證：資料是否符合 IRS 文字說明。兩個評估器讀取相同檔案，協議證明評估器一致，而非資料正確。BUG_INVENTORY.md 入口 BUG-0001 為典型案例：1040 表第9行總計第3a行與3b行；所有測試樣本及兩個評估器都同意錯誤總和；外部引擎發現了此問題。

7. Independent constructions

未聲稱有全面的人為逐行閱讀，因此專案補充了可選閱讀，並以僅包含檔案頁面的構造（spec/spec.md 第6.5節）作為基礎：對每張工作表進行第二次轉錄，僅給予頁面和模式的隔離模型，逐原子與專案進行比較；渲染比較，隔離模型未見 YAML，將每行英文與頁面對照閱讀；M 類手工，隔離模型在印刷工作表上執行分支覆蓋輸入；以及在編碼執行前做出的整體回報值盲測。每個模型均無儲存庫存取與網路連線（tools/transcription/README.md）；每次不一致都以來源、頁面及引用記錄，並將日誌提交至 reviews/2025/。保證：對於每行，同一頁面的兩次閱讀產生相同結構，或差異已記錄並裁決。未保證：閱讀者的獨立性。

8. Engines

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. The evidence report and the scoreboard

reports/2025/evidence.md 列出每一行以及證據類別（A，官方 IRS 範例；B，人力手工；C，外部指定計算器；M，獨立模型手工；H，人力來源閱讀；E，引擎；R，專案自身回歸測試；spec/spec.md 第 6.1 節）。首行為計分板，顯示至少有一項來自 Claude 模型族外的證據所計算出的行比例。2026-10-24 重新產出的報告顯示 198 / 1,515（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%。屬性測試檢查規格 6.3 的資料層級屬性，覆蓋 400 個產生的回傳；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，"Commit guard"）。保證：缺陷記錄不可編輯，且任何提交必須在該確切樹上完成整套測試後才可落地。未保證：套件未測試專案是否被捕捉；「為何存活」欄位旨在將每一次遺漏轉化為新檢查。

這並未確立

從 spec/spec.md 第3節第11項：人為來源閱讀覆蓋僅限於逐行證據紀錄；獨立建構及其記錄的分歧提供更廣泛的驗證。 報告識別符合條件的外部族群聲稱及其來源。未完成的驗證被報告為缺口；採用該要求並不等於完成。

原始的 Layer‑7 建構使用單一模型族群 Claude。Flash 現已完成對全部 55 表單的抄錄與渲染呼叫，並處理六個活躍的 Form 2441 案件以及一份 W‑2 回報。許多來源分歧以及 Form 2441 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，"Toolchain inspected"）：Node 與 npm；透過 elan 的 Lean 4（lean/lean-toolchain 固定版本）與 Lake；Poppler 的 pdftotext；Python 3 搭配 PyYAML；curl；以及 extraction check 的 PDFKit 讀取 PDF（tools/extraction/pdfkit_text.swift）所需的 macOS 與 Swift 工具鏈。檢查在全新 clone 上離線執行。引擎差異（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 許可證 2.0 (LICENSE)。資料已捐贈至公共領域，採用 CC0 1.0 Universal (LICENSE-DATA)：forms/、params/、tables/、fixtures/、 ambiguities/ 與 interview/。存檔的 IRS 原始碼位於 sources/，為 IRS 出版物。