# Lean proof to search for US tax loopholes > Source: > Published: 2026-11-10 10:38:47+00:00 # Lean proof to search for US tax loopholes Navier stokes? That will never make money. Instead, we compiled a Lean proof to find loopholes in the US tax code. But first, a step back. This example is part of the vulnerability monitoring work we do at [global law](https://github.com/lexifina/global-law), a CC0 repo of versioned legislation and caselaw. Our argument is that we can point AI at a versioned record of the law to find contradictions and other key logical mistakes in our system of legislation and interpretation. Loopholes are usually found by someone who knows two provisions well and sees that together they allow what neither allows alone. That depends on who is looking, and nobody can say whether their route is the best one. We wrote the rules down with no strategy built in, let a search try every sequence of moves they permit, and had a theorem prover check the result, on a corner of the Internal Revenue Code where the answer is already known, so that the method could be judged. ## The routes around the rules A Roth IRA is taxed at the front and never again, which makes it valuable to people with a long time to save. Congress limits who may contribute to one. The amount a single filer may put in shrinks between $150,000 and $165,000 of modified adjusted gross income and is zero above that.[\[1\]](#ref-1),[\[2\]](#ref-2),[\[3\]](#ref-3) Since 2010, though, there has been no income limit on converting a traditional IRA into a Roth IRA, and anyone may make a non-deductible contribution to a traditional IRA whatever they earn.[\[4\]](#ref-4),[\[5\]](#ref-5),[\[6\]](#ref-6) Put those two together and the income limit stops nobody: contribute to a traditional IRA, convert it the next day, and the money is in a Roth. Practitioners call this the backdoor Roth. It is widely treated as a loophole: the House voted to close it in 2021,[\[7\]](#ref-7),[\[8\]](#ref-8) and the chair of the Senate Finance Committee was reported the same year to be preparing a crackdown on Roth accounts used by the wealthiest savers.[\[9\]](#ref-9) There is a catch, and then a way round the catch. When money comes out of a traditional IRA, all of a person's IRAs are treated as one account, and each dollar converted is deemed to be the same mix of taxed and untaxed money as the whole.[\[6\]](#ref-6) Someone with $100,000 of pre-tax savings in an old IRA who adds $7,000 of after-tax money and converts $7,000 is taxed on most of it. But money rolled from an IRA into an employer's 401(k) plan can only be the pre-tax part, and is treated as coming from that part first.[\[6\]](#ref-6) Move the old savings into the 401(k) and what is left in the IRA is all after-tax, so the conversion costs nothing. A separate route runs through the 401(k) itself: the plan can accept after-tax contributions up to the overall limit on additions, $70,000 in 2025, and move them into its own Roth account, the route known as the mega backdoor.[\[10\]](#ref-10),[\[11\]](#ref-11),[\[8\]](#ref-8) ## Writing the rules down We wrote these provisions in Lean, a programming language whose type checker can also check mathematical proofs. An earlier post discussed how far that kind of formalisation can reach in law.[\[12\]](#ref-12) Here the model is small. A taxpayer has five accounts: cash, the traditional IRAs taken together, the Roth accounts, and the pre-tax and after-tax parts of a 401(k). There are seven moves between them, each written from the provision that governs it, with the 2025 limits: contribute to a Roth IRA, contribute to a traditional IRA, convert, roll IRA money into the 401(k), defer salary, make an after-tax 401(k) contribution, and roll that into the plan's Roth account. A move either is allowed, with its effect on each balance and on taxable income, or is not. ## What the search found The search starts from one person: a single filer earning $250,000, so far above the Roth limit, with $100,000 of pre-tax money in a rollover IRA from an old job and $100,000 in savings. It tries every move with every amount the position naturally offers (what is left of each limit, each balance, the pre-tax part, the after-tax part) and keeps going, breadth first, to six moves deep. That is 345,075 distinct positions. It is asked one question: how much can go into Roth accounts without any tax? The answer is $77,000, in five moves. Contribute $70,000 after tax to the 401(k) and roll it into the plan's Roth account; contribute $7,000 to a traditional IRA; roll the $100,000 of pre-tax IRA money into the 401(k); convert the $7,000. Both the backdoor and what practitioners call the mega backdoor come out of the search without having been described to it, and so does the order the backdoor needs. Forbidden the roll-in, the cheapest way to get the same $7,000 into the Roth is to contribute and convert, with $6,543 of it taxed. Run again for the same person earning $140,000, the search simply makes a Roth contribution. ## What the proofs add A search only reports what it saw, and it stopped at six moves. The proofs cover every sequence of moves of any length, from any starting position, and Lean accepts none of them until every step checks. There are four. The first is a conservation law: pre-tax money leaves the IRAs only by being taxed or by being rolled into the 401(k). From it follows the second, that without the roll-in every pre-tax dollar is taxed on its way to the Roth, however the conversions are split, ordered or repeated. The step that needed most care was rounding. The statute's proportion has to be computed in whole dollars, and Lean's automatic arithmetic could not show that rounding never taxes more than the pre-tax money there is, so that inequality was proved by hand. The third is that for every income above the limits, and every starting set of accounts, there is a permitted sequence that puts $7,000 into a Roth with no tax. That is exactly what the income limit in section 408A is meant to prevent. The fourth is a ceiling: in a year, no plan puts more than $77,000 of new money into Roth accounts at no tax, plus whatever after-tax money was already held. Since the search found a plan that reaches the ceiling, its plan is proved to be the best one in the model. In simplified form: ``` theorem roth_ceiling (income : Nat) (moves : List Move) : ∀ before after, run income before moves = some after → after.roth − before.roth ≤ 7000 + 70000 + before.iraBasis + before.planAfterTax + (after.taxed − before.taxed) ``` ## Limits The model applies the pro-rata rule at the moment of each conversion. The Code uses the value of all IRAs at the end of the year,[\[13\]](#ref-13) which is more forgiving about order: a conversion made before the roll-in, in the same year, is also tax-free. The plan the search found works on either reading, but other orderings would come out differently, and the next version should use the year-end rule. Whether a person can use the second route depends on their employer's plan, and after-tax contributions by higher-paid employees are often cut back by the nondiscrimination test in section 401(m).[\[14\]](#ref-14) The model knows nothing about state tax, employer contributions or investment growth. And a proof says only that the result follows from the rules as written in the model. Each rule was checked against the statute by hand, and that check is the part a reader should question. ## Why it matters None of this is news to a tax adviser, which is why it was chosen. Congress has looked at these routes too. The version of the Build Back Better Act passed by the House in November 2021 would have barred converting after-tax money from 2022 and so closed both.[\[7\]](#ref-7),[\[8\]](#ref-8) The bill stalled in the Senate, and the Inflation Reduction Act that replaced it in 2022 left the provision out.[\[15\]](#ref-15) Nothing enacted since has revived it, and both routes remain available in 2026.[\[16\]](#ref-16) What is new is that the routes and their limits fall out of the rules mechanically, together with a proof that nothing in the model does better. The more interesting places to point this are those where no one has catalogued the interactions: provisions that were amended at different times, or a bill before it passes. A drafter could write the proposed change into the same model and ask the search whether the limit they are adding can be walked around, and the proofs would say whether a fix closes every route or only the one someone thought of. It is the same idea as our [search for drafting mistakes in published law](https://lexifina.com/blog/mass-zero-day-vulnerability-detection-in-legal-code), applied to what the law permits rather than how it was written. The model and the search are public in global-law; see the [lean-proofs](https://github.com/lexifina/global-law/tree/main/lean-proofs) folder. **Isn't a lot of this deliberate? Law is grey on purpose.** Often, yes. The detectors look for mechanical mistakes, not grey areas: a reference to a section that was repealed or renumbered, a fine that points at a deleted rule, a rule in force before it was published. Whether a gap is a mistake or a choice is a legal judgement, so every review gives a verdict, and most flags turn out to be lawful, cured, intended or errors in a corpus rather than defects in the law. **The law isn't software. Why apply software-style checks?** It isn't, and these checks do not try to prove a statute correct. They work like a linter: they catch the mechanical slips (references that point nowhere, impossible dates, amendments that could not be carried out) that drafters would fix if they saw them. **Who benefits, and will legislators ever adopt this?** It needs no one's adoption: published law is public, so anyone can run the checks. Finding these mistakes used to take legal training and time; publishing them puts pressure on legislatures to repair them, and lets everyone, not only well-advised insiders, see where the text fails. ## References 1. 26 USC § 408A(c)(3) [](https://www.law.cornell.edu/uscode/text/26/408A) 2. Internal Revenue Service, Notice 2024-80, ‘2025 Limitations Adjusted as Provided in Section 415(d), etc.’ (1 November 2024) [](https://www.irs.gov/pub/irs-drop/n-24-80.pdf) 3. Internal Revenue Service, Publication 590-A, ‘Contributions to Individual Retirement Arrangements (IRAs)’ [](https://www.irs.gov/pub/irs-pdf/p590a.pdf) 4. Tax Increase Prevention and Reconciliation Act of 2005, Pub L 109-222, s 512 [](https://www.congress.gov/109/plaws/publ222/PLAW-109publ222.pdf) 5. ‘Roth IRA Conversions in 2010’ (*The Tax Adviser* , October 2009)[](https://www.thetaxadviser.com/issues/2009/oct/rothiraconversionsin2010/) 6. 26 USC § 408(d)(2), (d)(3)(A)(ii), (d)(3)(H) and (o) [](https://www.law.cornell.edu/uscode/text/26/408) 7. Build Back Better Act, HR 5376, 117th Congress (as passed by the House of Representatives, 19 November 2021) [](https://www.congress.gov/bill/117th-congress/house-bill/5376) 8. ‘Build Back Better Act would curb retirement plans for the wealthy’ (*CNBC* , 19 November 2021)[](https://www.cnbc.com/2021/11/19/house-passes-build-back-better-act-retirement-plans-for-the-wealthy.html) 9. ‘The Ultrawealthy Have Hijacked Roth IRAs. The Senate Finance Chair Is Eyeing a Crackdown.’ (*ProPublica* , 2021)[](https://www.propublica.org/article/the-ultrawealthy-have-hijacked-roth-iras-the-senate-finance-chair-is-eyeing-a-crackdown) 10. 26 USC §§ 402(g), 402A(c)(4) and 415(c) [](https://www.law.cornell.edu/uscode/text/26/402A) 11. Internal Revenue Service, ‘COLA increases for dollar limitations on benefits and contributions’ [](https://www.irs.gov/retirement-plans/cola-increases-for-dollar-limitations-on-benefits-and-contributions) 12. Alan Yahya, ‘The auto-formalization of mathematics versus law’ (*Lexifina* , 7 September 2026)[](https://lexifina.com/blog/auto-formalisation-of-law) 13. Internal Revenue Service, ‘Instructions for Form 8606: Nondeductible IRAs’ [](https://www.irs.gov/instructions/i8606) 14. 26 USC § 401(m) [](https://www.law.cornell.edu/uscode/text/26/401) 15. ‘Backdoor Roth 401(k) and IRA rules for the wealthy survive — for now’ (*CNBC* , 20 December 2021)[](https://www.cnbc.com/2021/12/20/backdoor-roth-401k-and-ira-rules-for-the-wealthy-survive-for-now.html) 16. ‘Making a backdoor or mega backdoor Roth contribution in 2026’ (*Mercer Advisors* , 2026)[](https://www.merceradvisors.com/retirement/making-a-backdoor-or-mega-backdoor-roth-contribution-in-2026/)