Proof-of-concept encodes US federal tax forms as cited, machine-checkable data

What the project does

A proof-of-concept repository on GitHub, emmilco/us-tax-model, reached the Hacker News front page after presenting the forms-and-instructions layer of US federal individual income tax as public, cited, machine-checkable data. Its first client is a guided self-preparation interview: it asks a person questions, decides which forms apply, computes them, explains every value, and hands back a values sheet the person files themselves. According to the project's documentation, the software never files, signs or transmits a return, and no return data leaves the machine. Notably, what is encoded is the IRS's published procedure, not the Internal Revenue Code itself.

Built to be checked, not trusted

The encoding was written largely by language-model agents, and the project is blunt that it cannot be trusted because of who wrote it. Instead, it is structured so that what matters can be checked from the repository alone by someone who trusts none of the authors.

Each form or worksheet is a YAML file in which every line carries an ID, printed line number, IRS label, type, a single expression, and a citation naming the document, tax year, revision, locator and the hash of the archived page it was read from. The build fails if any line, parameter, gate or question lacks a citation, and a verification script checks every quote and locator against the archived text. The 2025 citations report covers 2,313 anchors and 1,252 quotes, while 305 computed-line locator segments are flagged as too coarse to verify.

Every computed line applies exactly one atom from a closed vocabulary of roughly twenty small operations, including sum, subtraction floored at zero, smaller-of, rate multiplication, rounding, table lookup and guarded choice. There are no user-defined functions, loops, variables, strings or recursion. A build-time checker then rejects dangling references, cycles, type confusion between cents, rates, counts and booleans, and any gap or overlap in guarded alternatives.

Two further layers target readability and exactness. A renderer writes each line's English, in IRS worksheet phrasing, beside the official label and citation, so a data change appears in review as a readable English diff. Arithmetic is integer-only: money is integer cents, rates are integer pairs, and the evaluator uses BigInt with no floating point. Rounding occurs only where a cited instruction says to round, and unresolved readings are recorded in a separate ambiguities file.

Formal proofs and differential testing

The repository includes a Lean formalization that defines every atom over the integers, proves properties such as idempotent half-up rounding, and ships a reference evaluator proved to terminate and to be deterministic. The TypeScript and Lean evaluators were run over every fixture and generated return: 1,648 cases and 2,895,826 compared line values, with zero differences.

The project is quick to note what this does not prove. Agreement between evaluators shows the evaluators agree, not that the data is right. Its canonical example is BUG-0001: Form 1040 line 9 summed line 3a as well as 3b, and both evaluators agreed with the wrong sum until an outside engine caught it.

To probe the encoding against the source, isolated models with no repository access and no network re-transcribe worksheets, compare rendered English against archived pages, and hand-work branch-covering inputs; every disagreement is ruled against the page with the quote recorded. Generated returns are also pushed through three independent engines — PolicyEngine-US 2.49.4, Tax-Calculator 6.8.5 and OpenTaxSolver 23.06 — across 1,700 returns, with every line-level difference required to be explained to a cited cause. The current report lists no unexplained differences, though two of the engines primarily reach summary lines rather than worksheet lines.

Honest limits

According to the evidence report, 198 of 1,515 computed lines — 13.1 percent — currently have at least one assertion from outside the Claude model family, with zero human hand-work credits and zero human source-reading credits recorded so far. Form 2441's three missing STOP outputs remain uncredited and its form-level review is still pending. The project prints this scoreboard first, treating outside verification coverage as the one number it is trying to move.

Why it matters

Tax preparation is a domain where a single wrong line can cost money or trigger penalties, yet the rules live mostly as prose. This project is a serious attempt to turn that prose into a small, auditable formal system: a closed operation vocabulary, citations down to archived page hashes, machine-checked proofs and differential testing against established engines. Just as notable is its stance on AI-generated code — rather than asking anyone to trust model-written encodings, it tries to make verification independent of authorship, and it publishes its own bugs and gaps. If the approach scales, it points toward tax software whose arithmetic anyone can check, and toward a reusable template for validating LLM-generated formalizations in other regulated domains.