That's neat, what aspect(s) are you formalizing? That a given tax statement is correct?

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.