Show HN: A proof-of-concept formalization of the IRS federal tax forms

US-TAX-MODEL is a proof of concept for encoding US federal individual income tax forms and instructions as cited, machine-checkable data, with a guided self-preparation interview as its first application. It asks questions, determines which forms apply, calculates values, explains them, and produces a values sheet for the user to file. It does not sign or transmit returns, and tax data stays on the user’s machine. The project formalizes the IRS’s published procedures, not tax law itself. Its 2025 form lines cite archived IRS material, and each calculation uses a small, fixed set of operations. A build-time checker catches broken references, cycles, incompatible units, and gaps or overlaps in decision branches; a renderer turns calculations into readable explanations. Money is calculated in integer cents, with rounding only where the cited instructions specify it.

The project’s central claim is that its work can be inspected and tested, not that the encoding is already proven correct. A Lean formalization checks properties of the calculation operations, and an independent evaluator agrees with the TypeScript evaluator across 1,648 cases and nearly 2.9 million line values. Differential tests compare 1,700 generated returns with three external tax engines, with no unexplained differences reported. These checks still cannot catch a mistake shared by the data and its evaluators: the project documents a wrong Form 1040 line 9 sum that both evaluators and all fixtures initially accepted. Its evidence scoreboard records outside assertions for 198 of 1,515 computed lines (13.1%), with no current human reading or hand-work credited. The repository therefore emphasizes traceable evidence and known gaps rather than claiming comprehensive validation.