Not quite. The formalization covers the IRS's published procedure, i.e. the questions and calculations that go into the published forms, worksheets, and instructions. It's not a formalization of the tax code itself, and it's not a tax calculator, though a client of the underlying code could function as a tax calculator. (The project includes such a client, a CLI tax interviewer, just to exercise the code.)

In more detail:

- every line of every form gets a YAML representation which includes the source text, a data type, and an expression built from a small set of lean atoms, plus a citation pointing to the exact location of the rule in the original official document.

- underneath the yaml layer there's a lean formalization of the atoms showing that they behave as specified, that all comuptations use only the allowed atoms and operations, etc. There's also a typescript evaluator that's used to cross check the lean for agreement, so we have the arithmetic represented two ways.

The critical failure point for an LLM-produced formalization like this is the interpretation of the form text. Since I'm not a tax lawyer and don't intend to become one, this is an explicitly owned weakness and one I've structured the project around. Publicly available tax calculators (PolicyEngine, UsTaxes, OpenTaxSolver, etc.) are used to cross check derived numbers from this system. Mutation testing ensures the test suite is robust against bugs and arithmetic errors. Interpretations are cross checked by different model families (Claude, GPT, Deepseek). Etc.

The idea is to derive confidence from the formal properties of the system itself, and to allow theoretical future users of such a system to derive confidence in the interpretation of specific forms by making it easy to cross check line-level formalizations against the source documents.

There's a lot more detail in the (alas, Claude-authored) README. When I have time I'm going to write my own version of the README expressing my vision of the project, but I'm not there yet.

I'm not sure it matters. The IRS killed Direct File under lobbying pressure from the tax prep industry. In my opinion the public is owed a free version of this sort of tool. If the IRS doesn't produce it, then citizens ought to. If Google or Anthropic or whoever wants to offer a free version of this, more power to them, but I don't see why they'd bother. They could have done it decades ago.

And to be clear: my vision here isn't "have an agent do your taxes", it's to have agents build a hardened and thoroughly verified deterministic tool that can help you navigate the (somewhat bewildering) forms and instructions decision tree when filing your own taxes.

I think that assuming work can be done more easily in the future should not stop people from doing work that needs to be done in the present.

(If a painter knew that the camera was coming out I would not want them to throw their canvas away)

Years ago I had a similar issue. Accountant did something incorrect, increasing my liability by around $50k. Tax date came so I paid it, but moved accountants. New person fixed the issues, refiled, but it took a long time to get the refund back. IIRC, the IRS did include some nominal interest for the time they had the money.

People misunderstand the concept of liability. Yes your tax professional is liabile for fraud or gross misconduct, but if they make a mistake which results in unpaid taxes or fees you're still the one on the hook.

Yeah, I looked him up just now actually, and he has a 3-star rating on Yelp... Which I think is pretty low for accountants?

I think the red flag should have been when he printed out all my tax returns and made me pick them up in person, and didn't even send a digital copy.

In this case accountant DID NOT take liability for mistakes.

It's not the accountant that paid $20k for his mistake but the accountant's client.

i'm a bit unclear who has the liability even when you use a CPA. accountants are humans that sometimes make mistakes.

> Someone still needs to take liability for mistakes.

I am not aware of setups available to me that would transfer liability onto accountant.

So in either case I am taking liability.

(also, I am pretty sure that if corporation loses 10 millions over accountant making bad decisions, they are not going to recover that funds either)

I'm also 0 for 4 on tax preparers / tax accountants, so I concur with you its best to just do it yourself, which is what I now do. Only time I ever got audited (and failed) was when I had employed an accountant, since then I've never had a problem including passing audits. The tax code isn't /that/ complicated for most people's situation, and it's well worth understanding it.

In my experience agents will reach for numpy for any non trivial math without being instructed

So, GPT Sol outputted tax return PDFs that you were able to submit to the IRS? (I'd imagine that you couldn't directly e-file like you could from TurboTax.)

I appreciate the recommendation, but as it happens I have already solved the estimated issue (mostly by just preparing a full return with estimated next year's figures, which while time-heavy is going to be more accurate). And for what it's worth, I suspect it wouldn't work for me - cross-border is extraordinarily complicated because of the tax treaties (indeed there is a dedicated IRS form to disclose the effect and rationale of any treaty based position), and given there is no obvious note on the documentation for it that there is cross-border support I doubt there is.

(And as I said to another commenter, I think it would be advisable in this thread for people to expressly acknowledge or disclaim any interest in or prior experience with any particular product)

you were consulted by an LLM?

Are you saying I should use this (or it looks like one of their portfolio companies) as my return preparer, or as a replacement for Claude my return-checker? If the former, I would want to know why I should trust it; if the latter, I would want to know why I should pay for their services given I am already playing Anthropic for a subscription plan anyway.

(It would also help to know if you had a financial interest in or prior experience with this company)

They exist in USA - eg: freetaxusa.com

Most accountants will not in fact share client data with an LLM company.