us-tax-model

De laag van formulieren en instructies van de Amerikaanse federale inkomstenbelasting voor individuen, gepresenteerd als openbare, geciteerde en machine-controleerbare data, met een begeleid zelfhulpmenu ('interview') als eerste cliënt. Het interview stelt een persoon vragen, bepaalt welke formulieren van toepassing zijn, berekent deze, legt elke waarde uit en geeft een waardenblad terug dat de persoon zelf indient. De software dient, ondertekent of verzendt nooit een aangifte, en er verlaat geen aangiftegegevens de machine. Wat is gecodeerd, is de gepubliceerde procedure van de IRS, niet de Internal Revenue Code.

Waarom u het kunt controleren

De codering is grotendeels geschreven door taalmodel-agenten, dus deze kan niet worden vertrouwd enkel op basis van wie het heeft geschreven. Het is zo gebouwd dat de essentiële zaken vanuit de repository alleen kunnen worden gecontroleerd door iemand die geen van de auteurs vertrouwt. Elke laag beschrijft wat het is, wat het garandeert, wat het niet garandeert en waar men moet kijken.

1. Formulieren als data, met een bronvermelding op elke regel

Elk formulier of werkblad is een YAML-bestand onder forms/<year>/. Een regel is een record: id, gedrukt regelnummer, IRS-label, type, één expressie, en een citatie die het document, het belastingjaar, de revisie, de locatie en de hash van de gearchiveerde pagina onder sources/<year>/ noemt (zie spec/spec.md sectie 5).

• Garanties: De build mislukt als een regel, parameter, poort of vraag een citatie mist of verwijst naar een hash die afwezig is in het manifest. tools/citations.py verifieert elk citaat en elke locatie tegen de gearchiveerde tekst; reports/2025/citations.md rapporteert 2.313 ankers en 1.252 citaten, 0 bevindingen zonder geregistreerde uitspraak, en 305 berekende regel-locatiesegmenten die te grof zijn om te verifiëren.
• Geen garantie voor: Dat de expressie zegt wat de geciteerde pagina zegt. Een citatie bewijst dat een regel naar een pagina wijst, niet dat deze correct is gelezen.

2. Een gesloten vocabulaire van 'atoms'

Elke berekende regel is één toepassing van één 'atom' uit de lijst in spec/spec.md sectie 4.2 (sum, subtractfloor0, smallerof, multiplyrate, round, tablelookup, choose en een dozijn andere); er zijn geen door de gebruiker gedefinieerde functies, lussen, variabelen, strings of recursie.

• Garanties: De volledige betekenis van de data is de betekenis van ongeveer twintig operaties, die elk klein genoeg zijn om te lezen. De enige ondoorzichtige ontsnapping, een host-taalfunctie (opaque), wordt geteld en gepubliceerd; reports/2025/coverage.md rapporteert dat 0 van de 2.384 regels deze gebruiken.
• Geen garantie voor: Dat het juiste atom is gekozen voor een regel.

3. De build-time checker

engine/src/check.ts laat de build mislukken tenzij elke kopie, operand en parameterreferentie wordt opgelost binnen de opgegeven revisie; de regelgrafiek acyklisch is; elke expressie type-controleert (cents, rates, counts en booleans worden niet gemengd); elke choose uitputtende en disjuncte bewakers heeft, bepaald door enumeratie en intervalanalyse; en de herkomstregels van laag 1 gelden (spec/design.md sectie 2.3).

• Garanties: Geen hangende referenties, cycli, eenheidverwarring, of gaten of overlap in een bewaakte alternatief overal in de data.
• Geen garantie voor: Overeenstemming met de IRS-tekst; een verkeerde operand die type-controleert, wordt goedgekeurd.

4. De renderer

Elk atom heeft één Engels sjabloon in de bewoordingen van de IRS-werkbladen, en de renderer schrijft de Engelse tekst van elke regel naast het IRS-label en de citatie in rendered/<year>/, wat vervolgens wordt gecommit.

• Garanties: Een niet-programmeur kan elke regel afzetten tegen het geprinte formulier, en een wijziging in de data verschijnt in de review als een leesbaar Engels verschil (diff).
• Geen garantie voor: Dat iemand die lezing daadwerkelijk heeft uitgevoerd.

5. Integer-aritmetiek

Geld wordt uitgedrukt in integer cents, tarieven zijn integer-paren, en de evaluator (engine/, BigInt) maakt geen gebruik van floating point. Afronding gebeurt alleen in het round atom, alleen waar een geciteerde instructie zegt af te ronden, volgens de regel die daar wordt gesteld (spec/spec.md sectie 3, item 10).

• Garanties: Elke waarde is exact en elke afronding is geciteerd.
• Geen garantie voor: Dat de IRS bedoelde dat haar aritmetiek exact zou zijn; waar de tekst afronding openlaat, is de gekozen lezing opgenomen in ambiguities/<year>.yaml.

6. Lean

lean/TaxFormalization/ definieert elk atom over de integers (Atoms.lean), bewijst de eigenschappen van spec/spec.md sectie 6.3 (Lemmas.lean: subtractFloor0nonneg, roundHalfUpToUnitidem, prorateleamount), en heeft een referentie-evaluator over dezelfde canonieke JSON als die van TypeScript, waarvan is bewezen dat deze termineert en deterministisch is (EvalProps.lean). Beide evaluatoren draaien over elke fixture en gegenereerde aangifte; reports/2025/evaluator_agreement.md rapporteert 1.648 gevallen, 2.895.826 vergeleken regelwaarden, 0 verschillen.

• Garanties: De atoms gedragen zich zoals gespecificeerd, en twee onafhankelijk geschreven evaluatoren van dezelfde data berekenen dezelfde waarden.
• Geen garantie voor: Iets over de vraag of de data overeenstemt met de IRS-tekst. Beide evaluatoren lezen dezelfde bestanden, dus overeenstemming toont dat de evaluatoren het eens zijn, niet dat de data juist is. BUG_INVENTORY.md vermelding BUG-0001 is het canonieke geval: Form 1040 regel 9 telde regel 3a én 3b op; elke fixture en beide evaluatoren stemden overeen met de verkeerde som; een externe engine ontdekte dit.

7. Onafhankelijke constructies

Er wordt niet beweerd dat er een volledige menselijke regel-voor-regel lezing heeft plaatsgevonden, dus het project vult optionele lezingen aan met constructies die niets delen behalve de gearchiveerde pagina's (spec/spec.md sectie 6.5):

• Een tweede transcriptie van elk werkblad door een geïsoleerd model dat alleen de pagina's en het schema krijgt, vergeleken atom-voor-atom met die van het project.
• Een render-vergelijking, waarbij een geïsoleerd model dat de YAML niet heeft gezien, elke Engelse regel afzet tegen de pagina.
• 'Class M' handwerk, waarbij een geïsoleerd model werkt met input die de branches bestrijkt op het geprinte werkblad.
• Blinde voorspellingen van totale aangifte-waarden gemaakt voordat de codering werd uitgevoerd.

Elk model draait zonder repository-toegang en zonder netwerk (tools/transcription/README.md); elk meningsverschil wordt beslist in het voordeel van de pagina, waarbij het citaat wordt geregistreerd, en de logs worden gecommit onder reviews/2025/.

• Garanties: Voor elke regel hebben twee lezingen van dezelfde pagina dezelfde structuur geproduceerd, of het verschil is geregistreerd met de bijbehorende uitspraak.
• Geen garantie voor: Onafhankelijkheid van de lezers.

8. Engines

tools/engines/ genereert volledige aangiften en laat deze door drie engines lopen: PolicyEngine-US 2.49.4, Tax-Calculator 6.8.5 en OpenTaxSolver 23.06, waarbij regel voor regel wordt vergeleken waar de engine een regel berekent; reports/2025/enginedifferential.md bestrijkt 1.700 aangiften. Elk verschil moet worden verklaard door een geciteerde oorzaak, anders mislukt de run; een marge wordt nooit geaccepteerd, en het huidige rapport vermeldt geen onverklaarde verschillen. De regel-niveau OpenTaxSolver-adapter is in gebruik; UsTaxes moet nog worden toegevoegd onder docs/2026-10-22integrity_plan.md.

• Garanties: De samenvattingsregels die de engines bereiken, stemmen overeen met code die door andere mensen is geschreven op basis van de regels.
• Geen garantie voor: Iets over werkbladregels die de engines niet berekenen; de eerste twee bereiken voornamelijk samenvattingsregels, terwijl OpenTaxSolver ook werkbladregels bereikt.

9. Het bewijsrapport en het scorebord

reports/2025/evidence.md somt elke regel op met de klassen van bewijs die deze bevestigen (A: een officieel IRS-voorbeeld; B: menselijk handwerk; C: een genoemde externe calculator; M: geïsoleerd model handwerk; H: menselijke bronlezing; E: een engine; R: de eigen regressie van het project; spec/spec.md sectie 6.1). De eerste regel is het scorebord: het aandeel berekende regels met ten minste één bevestiging van buiten de Claude-modelfamilie.

Het geregenereerde rapport van 2026-10-24 vermeldt 198 van de 1.515 (13,1%); H: 0, B: 0, tweede-familie M: 44, E: 163 (de sub-tellingen overlappen). Dit weerspiegelt de geregistreerde numerieke bevestigingen na de audit van overgeslagen antwoorden; het vestigt geen volledige dekking van formulieren of volledige aangiften. De drie ontbrekende STOP-outputs van Form2441 blijven onbevestigd en de review op formuliereniveau staat nog open. Optionele menselijke bevindingen voorkomen de generatie van het rapport niet meer. Deze rapportverversing is geen nieuwe volledige pass.

• Garanties: Het bewijs achter elke regel kan worden opgezocht, en het enige getal dat het project probeert te verbeteren, wordt als eerste geprint. H-credits zijn een bronlezing met een actueel bewijs en het exacte logboek gecommit door de genoemde lezer; het levert geen berekende waarden en vult B nooit in. De eigenaar heeft het eerste pakket voltooid; oorspronkelijke bevindingen zijn bewaard en de huidige H-credit blijft nul. Verdere menselijke pakketten en uitspraakmonsters zijn optioneel onder de wijziging van het beleid van 2026-10-24.
• Geen garantie voor: Dat een regel met alleen A, Claude-familie M of R-bevestigingen is gecontroleerd door iemand anders dan één modelfamilie.

10. Mutatietesten, eigenschappen en interview-controles

De mutatietool past enkelvoudige atom-mutaties toe op de data (bijv. smallerof vervangen door largerof, een floor verwijderen, een operand wijzigen) en vraagt of de checker of een fixture dit opmerkt; reports/2025/mutation.md rapporteert 2.278 mutanten, waarvan 128 overleven, elk met een geschreven bewijs van equivalentie, wat resulteert in 94,4% ruw en 100,0% exclusief equivalenten. Eigenschapstesten controleren de data-niveau eigenschappen van spec 6.3 over 400 gegenereerde aangiften; reports/2025/properties.md rapporteert 8 eigenschappen, die allemaal standhouden. De finite-path checks van het interview (engine/, spec/spec.md sectie 6.4) enumereren antwoordcombinaties: elk pad eindigt in een complete set formulieren of een geciteerde weigering, de volgorde van antwoorden verandert de aangifte niet, en er wordt geen vraag gesteld waarvan het antwoord geen regel kan bereiken.

• Garanties: De fixtures zijn gevoelig voor de data die ze claimen te testen, de gestelde invarianten houden stand, en het interview heeft geen doodlopende wegen.
• Geen garantie voor: Iets wat een mutatie niet kan uitdrukken of wat een fixture al onjuist codeert (BUG-0001 opnieuw).

11. Het bug-inventaris en de commit-bewaker

BUG_INVENTORY.md registreert elk defect dat is gevangen door enige controle of lezing, vóór of samen met de fix: hoe het is gevangen, het symptoom, de bronoorzaak, waarom bestaande controles het misten, de fix en de commit. Het is append-only; check-all mislukt als het gecommitte prefix verandert of de ids niet sequentieel zijn.

tools/hooks/pre-commit weigert elke commit waarvan de tree niet de tree is die de laatste succesvolle npm run check-all heeft getest, en een run is succesvol alleen als er niets buiten de eigen outputs is veranderd terwijl deze draaide (tools/README.md, "Commit guard").

• Garanties: Het defectenregister kan niet worden bewerkt, en geen enkele commit wordt geaccepteerd zonder dat de volledige suite is geslaagd op exact die tree.
• Geen garantie voor: Dat de suite vangt wat deze niet test; het veld "waarom het overleefde" bestaat om elke dergelijke misser om te zetten in een nieuwe controle.

Wat dit niet vaststelt

Conform spec/spec.md sectie 3, item 11: de menselijke bronlezing-dekking is beperkt tot de bewijsrecords per regel; onafhankelijke constructies en hun geregistreerde meningsverschillen bieden de bredere verificatie. Het rapport identificeert kwalificerende bevestigingen van buiten de modelfamilie en de bron van elk. Onvoltooide verificatie wordt gerapporteerd als een gat; het adopteren van de vereiste vestigt niet de voltooiing ervan.

De oorspronkelijke laag-7 constructies gebruikten één modelfamilie, Claude. Flash heeft nu transcripties en render-aanroepen voltooid voor alle 55 formulieren en zes actieve Form 2441-gevallen en één W-2 aangifte uitgewerkt. Veel bronmeningsverschillen en drie lege numerieke outputs na een Form2441 STOP blijven bestaan; de tweede familie is nog niet gepromoveerd. Het geregenereerde scorebord credits 198 berekende regels over de geregistreerde engine- en tweede-familie bevestigingen; volledige formulierdekking blijft apart.

De huidige geschiktheid voor bronlezing staat in reports/2025/second_family.md. Transcriptie/render-lezingen zijn onderworpen aan hun individuele poorten. BUG-0129 legde een eenheid-uitwissing bloot in de transcriptie-vergelijker; de kwalificatie voor transcriptie wordt vastgehouden tot dat defect en eerdere overeenstemmingen zijn geaudit. Model-berekende waarden en externe-engine bevestigingen staan apart van deze hold. Bronlezingen worden apart gerapporteerd en zijn nog niet gekoppeld aan het scorebord. Het gewijzigde integriteitsplan versterkt de tweede-familie en engine-controles, waarbij menselijke lezingen optioneel zijn. Online belastinginterpretaties worden geregistreerd als niet-geautoriseerde corroboratie onder research/secondary/; deze verdienen geen scorebord-credit en blijven gescheiden van blinde, alleen op bronen gebaseerde model-aanvragen.

De IRS-formulieren en instructies zijn niet de wet. Ze bevatten oordelen over de Internal Revenue Code die niet worden aangekondigd, en dit project codeert de gepubliceerde procedure, inclusief deze oordelen; waar de tekst ambigu is of zwijgt, is de gekozen lezing vastgelegd in ambiguities/<year>.yaml en wordt deze aan de gebruiker getoond wanneer dit hun aangifte beïnvloedt. Geen enkele advocaat heeft de juridische positie waaronder het project opereert beoordeeld (spec/spec.md sectie 9).

Reikwijdte en dekking

De formulieren en regels die worden berekend zijn vermeld in spec/spec.md sectie 2.1, de situaties die worden geweigerd met een geciteerde uitleg in sectie 2.2, en de volgorde van de overige toevoegingen in sectie 2.4; de tool weigert nooit stilzwijgend. Dekking wordt gemeten over volledige aangiften (een aangifte telt alleen wanneer niets erop wordt geweigerd) door tools/coverage/estimate.py in reports/2025/filer_coverage.md, wat vandaag 68,6% van de individuele aangiften aangeeft. Kanttekening: 148 van de 157 weigeringspoorten worden niet gemeten (geen IRS-telling of microdata-variabele), dus het cijfer geldt alleen voor de gemeten situaties en de werkelijke dekking is lager door het aandeel van de ongemeten poorten.

Hoe alles uit te voeren

Eén commando bouwt de data opnieuw op, voert elke controle uit en registreert de geteste tree:

npm install
npm run check-all

Voorvereisten (gecontroleerd bij de eerste inspectie van de toolchain in tools/README.md):

• Node en npm
• Lean 4 via elan (lean/lean-toolchain pinnt de versie) met Lake
• Poppler's pdftotext
• Python 3 met PyYAML
• curl
• Voor de extractie-controle van de PDF's (tools/extraction/pdfkit_text.swift): macOS met de Swift toolchain.

De check draait offline op een verse clone. De engine-differentiaal (tools/engines/README.md) vereist dat de twee externe engines zijn geïnstalleerd met tools/engines/setup.sh (de enige netwerkstap); zonder deze wordt deze stap zichtbaar overgeslagen en wordt de check niet geclaimd. De commit-bewaker is een git-hook, geactiveerd met git config core.hooksPath tools/hooks.

Permanente mededelingen

Getoond bij de eerste run en op elke output (spec/spec.md sectie 8):

• Dit is geen belasting- of juridisch advies.
• De gebruiker is verantwoordelijk voor de aangifte.
• De tool implementeert gepubliceerde IRS-formulieren en instructies, die niet de wet zelf zijn.
• Het is niet gelieerd aan of goedgekeurd door de IRS.
• De lijst van wat het wel en niet dekt (zie boven).

Waar zaken zich bevinden

PROJECT_INDEX.md somt elke directory op, wat deze bevat en de naamconventies. HANDOFF.md en de huidige HANDOFF-STAGE-*.md zijn de leesvolgorde voor een sessie die de build voortzet.

Licenties

Code is gelicenseerd onder de Apache License, Version 2.0 (LICENSE). De data is publiek domein onder CC0 1.0 Universal (LICENSE-DATA): forms/, params/, tables/, fixtures/, ambiguities/ en interview/. De gearchiveerde IRS-bronnen onder sources/ zijn IRS-publicaties.