Writing tax law in Lean and checking the product's tax calculation for every input (税法を定理証明支援系 Lean で書いて、プロダクト実装を「全入力で」確かめる)
A · Strong evidence Detailed engineering post by a freee engineer on formally verifying production tax calculations in Lean with AI agents; method, scope limits and concrete results (76,165 inputs, zero mismatches, derived deduction amounts matching the National Tax Agency) are shown and checkable.
Summary based on the full text·Original: about 30 minutes to read
In short
A freee developer blog post (November 2026) by engineer kyasu describes checking the company's tax calculations against the law for every possible input, not just chosen test cases. Tax provisions are written in the Lean theorem prover by AI agents (Claude) from the statute alone, without looking at the code. Production Ruby is copied into Lean and checked by property-based testing, and theorems link the two Lean models. Human review shrinks to the propositions and the inputs used as oracles. The work found proven equivalences, a deduction order the rules leave open, and choices that change the tax due.
Key numbers
- 76,165distinct inputs on which production Ruby and its Lean copy were compared for the income-tax rate table, with 0 mismatches
- 78 / 34form fields compared per case for loss carry-forward and for loss offsetting
- 13income categories a carried-forward casualty loss can be deducted from
- 7categories whose deduction order a tax circular lets the taxpayer change
- 306,300 vs 204,200 yentax in a fictional example under two legal deduction orders, a 102,100-yen difference
As reported by the source.
Japanese·Web page·opens developers.freee.co.jp
What it reports
- Scope: income tax, corporate tax, local taxes, consumption tax and items such as depreciation; only pure calculation functions whose inputs are explicit arguments. Screens, databases and external links are out of scope.
- Two comparisons: production Ruby vs "Ruby-like Lean" (a literal copy) by property-based testing; Ruby-like Lean vs "Elegant Lean" (written from the statute only) by proof.
- Income-tax rate table: 76,165 distinct inputs, 0 mismatches between production and the Lean copy. The product's quick-calculation table was proven equal to the statute's band-by-band sum for all taxable incomes; the NTA's published deduction amounts (97,500 to 4,796,000 yen) follow from that equality.
- Housing-loan credit: the code caps and rounds in the opposite order to the statute; proven equal for all balances from Reiwa 4 onward, because rounding down is monotone and the cap constant has no sub-100-yen fraction.
- Spousal special deduction: a 27-value constant table in the code was proven to match the statute's formula within the stated income range.
- Casualty-loss carry-forward: a circular lets taxpayers reorder 7 of 13 categories. The product uses the circular's default order. The carried-forward amount is the same for every legal order (proven), but which category keeps the remainder changes, so tax differs; the default order is not always the cheapest.
- Fictional example: 306,300 yen vs 204,200 yen tax under two legal orders.
- Next step: putting both comparisons into pre-release QA and into development as a shift-left check.
How they got it
AI agents wrote both Lean models and most proofs; tactics such as omega and decide close the arithmetic; the Lean kernel checks every proof. Property-based testing mixed random inputs (0 to 100 million yen, 30% blanks, 10% losses), exhaustive axis combinations and boundary values taken from the theorems, and measured that every branch condition was hit both true and false. Fields were compared one by one without rounding.
Limits
- The all-input guarantee holds between the two Lean models; the link to production Ruby rests on finite property-based tests.
- Both models could share the same misreading of the law; agreement is strong evidence, not proof of legal correctness.
- Results are machine checks before review by a licensed tax accountant; the order choice rests on a circular, not statute.
- No defect counts or effort figures are given; the work started as a personal project in September 2026.
Why it matters for companies
Formal verification used to be too costly for business rules; with agents writing the formal models and proofs, one engineer reached production-scale tax logic in a few months. The pattern carries over to any rule-heavy calculation (payroll, pricing, regulatory reporting): write the rule independently from the code, prove where the two agree, and let testing cover the rest. It also changes what a person reviews: the proposition, not the agent's long code.
Key passages in translation
Japanese original
人が確認する対象が、AI の書いた長いコードではなく、命題とオラクルとしての入力に絞られること
What a person has to check narrows to the propositions and the inputs used as oracles, rather than the long code the AI wrote.
Japanese original
Elegant Lean を書くときは既存の実装を参照せず、条文だけを出発点にして Claude に書かせた
When writing Elegant Lean we did not refer to the existing implementation; we had Claude write it starting only from the statute.
Japanese original
ソフトウェアテストは点で確かめ、証明は条件式で確かめます。
Software tests check at points; proofs check with conditions.
Summary based on the full text. Read the original for the full argument and data.Read the original on developers.freee.co.jp
- Tags
- Formal verification, Qa