Lean, el verificador de pruebas, halla 138 fallos fiscales

¿Qué hizo Lexifina con el código fiscal de Estados Unidos?

138 errores de redacción en el código fiscal de Estados Unidos, detectados por una máquina en dos minutos y medio. Eso es lo que reporta Lexifina, un proyecto de investigación legal que tradujo el Internal Revenue Code al lenguaje Lean, cuyo verificador de tipos también comprueba demostraciones matemáticas: si Lean acepta una prueba, cada paso se sigue de las definiciones y no se acepta nada por confianza.

Para un founder que construye sobre reglas —impuestos, compliance, seguros, contratos— el mensaje es directo: si la ley se puede escribir como código, también se puede testear como código. Y eso cambia el costo de encontrar el error antes de que lo encuentre un cliente, un regulador o un tribunal.

El texto oficial del Título 26 lo publica como datos estructurados la Office of the Law Revision Counsel, la oficina de la Cámara de Representantes que compila el Código. Lexifina usó la versión vigente al 3 de noviembre de 2026. Un parser lee cada referencia cruzada —incluidas las escritas con palabras, como «paragraph (2) of subsection (b)» o «sections 922 through 927», que no llevan hipervínculo— y Lean verifica una por una: ¿existe la disposición citada? ¿sigue vigente?

¿Y esto cómo se aplica en tu negocio?

Dueños de negocio de Latinoamérica y España usan un agente de IA para ganar más y recuperar su tiempo. El Kit «tu mano derecha con IA» te muestra cómo en un video de 11 minutos, con una ficha para armar el tuyo. CAR está cerrada por ahora; al anotarte, te avisamos cuando abra.

👥 Quiero el Kit →

El trabajo continúa una entrada previa del mismo blog, donde una búsqueda ciega redescubrió el backdoor Roth partiendo solo de las reglas de cuentas de retiro.

138 errores de redacción que nadie había detectado

El test suite reporta 257 hallazgos. Tras revisarlos contra el texto oficial y sus notas editoriales, quedaron 98 intencionados (reglas para periodos pasados y disposiciones aprobadas que aún no entran en vigor), 21 falsas alarmas en los hipervínculos de los propios editores y 138 fallos reales:

67 referencias a algo derogado, movido o reescrito sin el ajuste correspondiente.
24 erratas, subdivisiones equivocadas o leyes sin nombrar.
9 disposiciones que comparten el mismo número.
8 palabras de nivel jerárquico incorrectas (llamar «paragraph» a un «subsection»).
30 paréntesis que nunca cierran.

Cada fallo lleva un certificado: una declaración corta en Lean que arrastra su evidencia desde el XML oficial y demuestra el error. Lean reverifica los 138 en unos dos minutos y medio. Y como el registro del Código es un historial de git con un commit por ley pública, cada error se rastrea hasta la ley que lo escribió; para el Título 26 el historial llega hasta la edición de 1994.

Lo relevante para un equipo de producto es que el chequeo es barato de repetir: correrlo contra cada nueva versión del Código marca un error apenas aparece y nombra la ley responsable.

Los cinco hallazgos del modelo fiscal de 2025

Después, Lexifina escribió lo que la ley calcula: el impuesto federal sobre la renta de 2025 para un hogar, los números del Form 1040, incluidos los cambios del One Big Beautiful Bill Act de julio de 2025. El modelo se armó en cuatro partes —ingresos hasta el AGI, deducciones, el impuesto con el AMT y los créditos— y se validó contra las tablas que publica el IRS y contra tres programas fiscales independientes sobre 5.000 hogares.

Al escribirlo aparecieron cinco cosas:

El Código publicado mezcla derecho de 2025 y de 2026. En seis lugares el texto consolidado ya muestra enmiendas de la ley de 2025 que empiezan a regir en 2026. Leído sin las notas de vigencia, da un impuesto de 2025 equivocado: el desfase del AMT al 50% en lugar del 25%, y un piso de donaciones y un tope de deducciones que todavía no aplican.
La misma ley redondea en direcciones opuestas. Las nuevas deducciones por propinas y horas extra se reducen US$100 por cada US$1.000 completos de ingreso por encima del límite, así que un dólar más de ingreso puede costar US$100 de deducción. La deducción por intereses de crédito automotriz se reduce US$200 por cada US$1.000 «o fracción», que redondea al revés: se agota US$999 antes de lo que sugieren los números redondos.
Una pareja puede deducir más SALT declarando por separado. El tope de deducción de impuestos estatales y locales se reduce 30 centavos por cada dólar sobre US$500.000 en una declaración conjunta. En una separada, la ley reduce el tope a la mitad antes de aplicarlo, así que baja solo 15 centavos por dólar. Una pareja que gana US$300.000 cada uno puede deducir hasta US$25.000 en dos declaraciones separadas, pero solo US$10.000 en una conjunta.
La Tax Table no es la fórmula. La tabla del IRS difiere de la fórmula legal entre −US$5 y +US$6, y Lean demuestra ese rango para todo ingreso bajo US$100.000 y cualquier estado civil.
Un dólar puede costar US$8.046. Una familia con tres hijos puede perder todo su EITC por tener un dólar de ingreso por inversiones por encima de US$11.950. El crédito del ahorrador funciona igual: una pareja que aporta US$2.000 cada uno recibe US$2.000 con un ingreso de US$47.500 y US$800 con US$47.501.

¿Qué pasó al compararlo con el software fiscal que ya se usa?

Un modelo solo sirve si da las respuestas correctas. Lexifina construyó 5.000 hogares de muestra y calculó el impuesto de 2025 de cuatro maneras: con su modelo y con PolicyEngine-US, Tax-Calculator y UsTaxes, tres herramientas de código abierto hechas por equipos independientes entre sí y del suyo. Dos mil hogares eran ordinarios; los otros 3.000, deliberadamente incómodos: parejas que declaran por separado, viudos, estudiantes, gente con propinas u horas extra, IRAs y cuentas de salud, créditos educativos y por ahorro, e ingresos sobre US$1 millón con grandes ganancias de inversión.

El modelo de Lexifina y PolicyEngine-US coincidieron en 4.993 de los 5.000 hogares; los siete restantes difieren en US$11 como máximo, todos en el EITC. La comparación también expuso errores ajenos: Tax-Calculator otorga el EITC y el crédito por cuidado de hijos a parejas que declaran por separado sin comprobar que vivan separadas, y no calculó AMT para un declarante separado de altos ingresos donde otras dos calculadoras llegaron a US$14.881. UsTaxes acumuló 14 bugs que afectan a cerca de uno de cada seis hogares ordinarios, entre ellos que su declaración de 2025 nunca adjunta el Schedule C, con lo que la renta por cuenta propia desaparece sin aviso.

Y sirvió para lo más incómodo: encontrar dos errores propios. Lexifina no contaba la ganancia por cuenta propia para la deducción del 20% a pequeñas empresas, y siempre tomaba la mayor entre deducción estándar y detallada, aunque la ley permite detallar una cantidad menor. Con eso corregido, un hogar pagó US$2.070 menos.

Tres estrategias fiscales que no estaban documentadas

Con un modelo que coincide con el software de referencia, Lexifina lo usó como oráculo de una búsqueda que no sabe nada de planificación fiscal: primero 195.787 declaraciones con opciones ordinarias, después unos 30.000 planes para cuatro familias a lo largo de 34 a 47 años. Casi todo lo grande que encontró ya estaba en la literatura de asesores. Tres resultados no:

Declarar por separado puede bajar el impuesto sobre el Seguro Social, incluso para una pareja que vive junta. Con US$48.000 de beneficios y un salario de US$60.000, la pareja debe US$7.050 en conjunto y US$5.568 por separado: US$1.482 menos. Con un salario de US$100.000 el resultado se invierte, así que la ventana existe pero es estrecha.
Salarios en una declaración, inversiones en la otra. El impuesto del 3,8% sobre renta por inversiones aplica al menor entre esa renta y el exceso sobre US$250.000 en conjunto o US$125.000 por separado. Con unos US$200.000 de cada lado, el ahorro es de US$1.621.
El Schedule 8812 paga más de lo que permite la ley. No es una estrategia, es una brecha entre el formulario y el estatuto: con un hijo y otro dependiente, US$240.000 de ingreso y sin impuesto por absorber, la ley da US$200 y el formulario US$700.

¿Qué significa esto para tu startup?

Si tu producto depende de reglas —fiscales, regulatorias, contractuales o de seguros—, este caso deja tres lecciones operativas que puedes aplicar esta semana:

Separa la regla del cálculo y testéala como código. Lexifina no confió en su traducción del estatuto: la comparó contra tablas oficiales y contra tres implementaciones independientes. Si tu motor de reglas solo se prueba con casos que tú mismo escribiste, estás midiendo tu propia lectura, no la norma.
Versiona la ley como versionas el software. Un commit por norma permite responder la única pregunta que importa cuando algo se rompe: qué cambio lo rompió y cuándo entró en vigor. Sin ese historial, cada actualización regulatoria es un salto de fe.
Desconfía del consenso entre herramientas. Lexifina encontró dos errores propios justamente porque dos programas ajenos coincidían entre sí y no con su modelo. Si cuatro calculadoras dan lo mismo, pueden compartir la misma mala lectura.

El mercado ya se está moviendo en esa dirección. Pramaana Labs, una startup de San Francisco, levantó US$27M en una ronda semilla liderada por Khosla Ventures con participación de Accel, Boldcap, Nexus Venture Partners, Premji Invest y Unbound, según reportó TechTimes, para construir verificación formal en derecho, preparación de impuestos y descubrimiento de fármacos. Su equipo asesor en materia fiscal incluye a Danny Werfel, comisionado del IRS entre marzo de 2023 y enero de 2025. La misma nota de TechTimes señala que la base de datos del investigador Damien Charlotin había catalogado más de 1.353 casos de alucinación de IA en procesos judiciales en todo el mundo hacia abril de 2026, y que solo en el primer trimestre de ese año los tribunales de EE.UU. impusieron más de US$145.000 en sanciones a abogados que presentaron citas fabricadas por IA.

Los límites: una prueba no es la verdad

Lexifina es explícita sobre lo que su trabajo no cubre, y esa honestidad es parte del valor:

Cobertura. El modelo cubre el impuesto individual de 2025 para un hogar. Deja fuera el kiddie tax en la declaración de un año, las ganancias del 28% y del §1250, la renta extranjera, las reglas de actividad pasiva y la mayoría de las preferencias del AMT.
Quién revisó qué. La clasificación de errores de redacción y las revisiones las hicieron agentes de IA contra el texto oficial, y no las ha validado un abogado ni un contador.
Coincidir no es acertar. Donde las cuatro calculadoras coinciden, pueden compartir la misma mala lectura. La prueba real son los teoremas y los ejemplos que publica el IRS.

Existe además un límite estructural que TechTimes describe con claridad al analizar a Pramaana: un sistema de pruebas demuestra que una respuesta es correcta respecto de una especificación formal. Si esa especificación está mal escrita, omite una excepción o no refleja una enmienda, la prueba es válida dentro del sistema equivocado. La respuesta verificada sigue siendo incorrecta. Por eso el cuello de botella no es el motor de pruebas, sino las personas capaces de traducir la norma con fidelidad.

Conclusión

Lexifina demuestra que el código fiscal de EE.UU. se puede tratar como software: con tests, con historial de versiones y con errores rastreables hasta la ley que los introdujo. Los 138 fallos de redacción no son anécdotas: son el tipo de defecto que un equipo de producto descubre cuando un cliente lo reporta.

Para un founder hispanohablante que construye en legal tech, fintech o compliance, la ventana es concreta. La formalización de normas es trabajo intensivo en conocimiento experto y todavía poco automatizado, y quien logre combinar dominio legal con ingeniería de pruebas tendrá una ventaja difícil de copiar. El aviso también es claro: la verificación no sustituye el criterio. Prueba que tu sistema hace lo que dijiste que debía hacer; asegúrate, por separado, de que lo que dijiste es lo que la ley realmente exige.