Show HN: A proof-of-concept formalization of the IRS federal tax forms

Category: other

Tags: tax, formal-verification, lean, data-validation, reproducibility, yaml

Score: 7.0/10 (Innovation: 8, Technical: 8, Documentation: 9, Utility: 3)

This project formalizes the IRS federal tax forms as machine-checkable data with per-line citations, a closed vocabulary of arithmetic atoms, a type checker, a Lean specification and reference evaluator, and differential testing against external tax engines. It is a rigorous exercise in reproducibility and validation, but its practical utility is limited because it only covers a narrow slice of individual tax preparation and is not a filing system.

Target audience: software engineers and researchers interested in formal methods, data provenance, and tax computation, as well as tax professionals evaluating open-source tools

Repository: https://github.com/emmilco/us-tax-model · HTML · Apache-2.0

View on Hacker News