A US tax calculator that shows its work — and can prove it.

Three ideas, that's the whole project:

1. Ask it a tax question with plain facts (--wages 50000).
2. It answers with a proof: every rule it applied, with the law it came from (26 U.S.C. § 63(c) …), every assumption it made.
3. Anyone can verify that proof offline. If it can't derive an answer from its encoded rules, it refuses — it never guesses.

Open source (AGPL-3.0, with commercial licenses available), exact to the cent (no floating point), built to be extended.

pnpm install && pnpm build
pnpm opentax eval --status mfj --wages 120000 --kids 2

us.federal.income_tax_after_credits  $5,640.00
├─ us.federal.income_tax_before_credits  $10,040.00   [26 U.S.C. § 1(j); Rev. Proc. 2025-32]
│  └─ us.federal.taxable_income  $87,800.00           [26 U.S.C. § 63(b)]
│     ├─ us.federal.agi  $120,000.00
│     │     ├─ fact wages = $120,000.00
│     │     └─ assumed taxableInterest = $0.00 (default)
│     └─ us.federal.standard_deduction  $32,200.00    [Rev. Proc. 2025-32 § 4.14]
└─ us.federal.ctc  $4,400.00                          [§ 24, as amended by OBBBA § 70104]

Assumptions (6): taxableInterest = $0.00, isAge65OrOlder = false, …
corpus sha256:6ff44719…

It answers under the law in force on the date you ask about — --as-of defaults to today; pass --as-of 2025-12-31 and the same facts derive under TY2025 rules instead (different standard deduction, different brackets, cited to the other Rev. Proc.).

Money is written in dollars (50000, "$50,000", "1234.56"). Not sure what inputs exist? pnpm opentax facts lists them all. More facts than fit in flags? Use a JSON file: --facts examples/mfj_120k_2kids.json.

Or skip the terminal entirely — the engine is pure TypeScript with zero platform dependencies, so the whole thing runs in a browser:

pnpm -F @invaro/opentax-playground build && open packages/playground/dist/index.html

One 130 KiB self-contained HTML file: engine + full rule corpus + verifier, no server, no network, works from file://. Compute, read the proof tree, download the proof — then paste it into the Verify tab and watch your own browser re-derive every step (alter one byte and it says exactly what broke). Same corpus Merkle root the CLI prints.

Save a proof, verify a proof:

pnpm opentax eval --status single --wages 50000 --proof proof.json
pnpm opentax verify proof.json     # ✓ VERIFIED — re-derived independently, every step matches

Change one byte of the proof — or one rule — and verify fails and says exactly what broke: the file was altered, the corpus is a different version, or a step doesn't re-derive.

Don't want to trust our verifier? The format is fully specified — canonical JSON, hashing, Merkle construction, node semantics, test vectors — in docs/PROOF-FORMAT.md, so you can write an independent checker in whatever language you trust.

It tells you, in one consistent shape, and never makes something up:

Every error is { code, message, data, hint } — same shape for humans, scripts, and AI agents.

LLMs will confidently produce wrong tax figures — most training data predates the OBBBA entirely. Two integration patterns fix that:

1. Oracle pattern (MCP) — the model never computes; it calls the engine:

claude mcp add opentax -- node packages/mcp/dist/index.js

Nine tools: calculate_tax, verify_tax_claim, verify_fact (fact-check any claimed dollar amount — "CTC is $2,000/child" → refuted, it's $2,200, § 24(h)(2) as amended by OBBBA), lookup_tax_parameter, is_tipped_occupation (the full Treasury occupation list as data), list_input_facts, explain_rule, find_tax_cliffs, compare_filing_statuses. Every response carries its assumptions and the corpus hash, so the agent can quote the law and the user can re-verify.

2. Guardrail pattern (opentax check) — the model answers, your harness gates it:

$ opentax check --status mfj --wages 120000 --kids 2 --expect 6600
✗ REFUTED   claimed $6,600.00, but the law derives $5,640.00 (off by $960.00)
$ echo $?
1        # wire this into your eval suite / response pipeline

Exit 0 = verified, 1 = refuted (with the correct value), 2 = the claim can't be checked without more facts. A one-line post-processing step turns any tax-adjacent agent from "plausible" to "provable."

Plus the general contract: add --json to any command — single JSON object, ok: true|false, stable error codes and exit codes, no ANSI. Full agent docs in AGENTS.md.

Every W-2 household, all five filing statuses, refunds included. The default answer is net tax — negative means the government owes you.

• Individual (Form 1040) — brackets, standard & itemized deductions (Schedule A with the OBBBA SALT cap), capital gains & qualified dividends with full § 1222 Schedule D netting, AMT, Social Security taxation, retirement income incl. the § 72(d) pension Simplified Method, residential rental income with § 168 depreciation, SE tax, NIIT & Additional Medicare, kiddie tax, capital losses, HSA, student-loan interest, IRA deduction, foreign earned income exclusion.
• Credits — CTC/ACTC + ODC, EITC (all child counts), education (AOTC/LLC), child & dependent care, saver's, adoption, premium tax credit (2025 no-cliff / 2026 cliff) — plus proof-backed dependent determination.
• OBBBA, both years — tips & overtime deductions (with the 71-occupation eligibility list), senior deduction, car-loan interest, non-itemizer charitable, § 68 haircut, and the 2026 parameter shifts throughout.
• Business & corporate (Form 1120) — QBI § 199A full mechanics, SEP/solo-401(k), § 179 + bonus + R&D expensing + § 163(j), K-1 pass-through, entity classification, flat 21% with charitable/DRD/NOL mechanics, BEAT, corporate FTC, § 250, penalty taxes, QSBS, buyback excise, corporate estimates.
• Estates & trusts (Form 1041), household employment (Schedule H), farmers & fishermen, estimated-tax safe harbors + annualized installments, withholding checkup.
• Out of scope refuses loudly — consolidated returns, REIT/RIC, fiscal-year returns, CAMT: a named refusal, never a silent wrong answer. (State returns for IL/VA/CA/NY/PA live in the composer, via the MCP server and opentax state — PA includes the eight-class netting rules, Schedule SP Tax Forgiveness, and the new Working Pennsylvanians Tax Credit.)

Independently validated (full methodology in docs/METHODOLOGY.md): a differential harness runs 572 TY2025 scenarios through both opentax and PolicyEngine US, a separately-built open-source model. Result: 533 agree to the exact cent, zero unexplained disagreements, and every explained difference is triaged with a primary-source citation in known-differences.json. The harness once caught a real bug in us — fixed, fixture-pinned, both engines now agree to the cent.

Is it correct? Exact bigint-cents math — floats never enter · golden fixtures asserting every intermediate to the cent · below $100,000 the engine reproduces the printed IRS Tax Table method exactly (verified against 41 sampled rows of the 2025 Publication 1040 table, all four statuses) · every rule and the fact catalog Merkle-pinned in corpus.lock.json · every fixture round-trips through verify · every dollar read from the primary source text.

Honest caveats. Where the engine approximates, the rule's own citation says so; where a condition can't be verified, the default is conservative — $0 or a refusal, never a guess. The big ones: earned income ≈ wages and MAGI ≈ AGI in several phase-outs; EITC qualifying children approximated by the CTC child count; a handful of niche interactions refuse outright.

Because the rules are pure functions, opentax can reason about the tax code, not just evaluate it — and every data point is a real, proof-backed evaluation:

$ opentax cliffs --status hoh --wages 30000 --kids 2 --vary taxableInterest --from 10000 --to 14000

1 cliff(s) found:
  ▮ at $11,950.00: one more cent of taxableInterest costs $3,234.84

That's the § 32(i) EITC kill switch, located to the exact cent by bisection over real evaluations — one cent of interest income destroys the family's entire earned income credit.

opentax compare --wages 50000            # net tax under every filing status
opentax marginal --status single --at 50000    # your true marginal rate
opentax sweep --vary wages --from 0 --to 200000 --step 5000 --csv   # the whole curve

cliffs also finds every $50 CTC phase-out step (§ 24(b)'s "or fraction thereof" makes one cent past $412,000 cost $50); invert answers "what income first reaches tax X" by bisection — and refuses with not-monotone when the EITC region makes the answer ambiguous, rather than returning a plausible root. This is "policy simulation" as an open-source CLI command.

This is a computation-and-citation tool, not tax advice.

All tax knowledge is data — you add coverage by writing a rule object with a citation and a hand-computed test, never by touching engine code:

1. Write the rule (id, citation with statute + excerpt, validity dates, formula).
2. Statutory exceptions are their own rules that override the base with a guard — the proof shows why they did or didn't fire.
3. Add a golden fixture with expected cents you computed from the statute by hand.
4. pnpm test && pnpm -F @invaro/opentax-corpus-us-federal gen:lock

Full walkthrough: CONTRIBUTING.md.

All take --json. In this repo, prefix with pnpm: pnpm opentax …

packages/core — the engine (domain-general, zero deps, browser-safe) · packages/corpus-us-federal — the tax rules as cited data + golden tests · packages/solve — the reasoning layer (also domain-general) · packages/compose — printed-form state-return composers · packages/cli — the opentax command · packages/playground — the browser playground (one self-contained HTML file).

Natural-language fact extraction (LLM in front, never inside the math) → statute→rules autoformalization pipeline → education credits → proof-format spec → state corpora. (Done: OBBBA amendments · TY2026 · all five filing statuses · EITC/ACTC/refunds · tips & overtime · the solver layer · differential testing vs. PolicyEngine · itemized deductions & the OBBBA SALT cap · the browser playground.)

Currency policy: the corpus tracks current law — when the IRS or Congress changes the numbers, the change lands as a new rule version with its own validity window and citation, never an in-place edit. Old proofs stay verifiable against the corpus root they were computed under.

OpenTax is free software under the GNU AGPL-3.0: use it, study it, fork it, run it as a service. The one condition is the AGPL's share-alike rule: a product or service built on this engine must publish its own complete source under the AGPL too.

Building something closed-source or proprietary? You need a commercial license from Invaro. That is the deal: open products use it free, closed products pay for it. It keeps the engine funded and the corpus current.

Versions through 0.2.1 were released under Apache-2.0 and remain so; all later versions are AGPL-3.0-only. "OpenTax" is a trademark of Invaro Inc.