Tax rule changes at AWS's scale are risky to ship: a bad configuration in a tax rule engine has direct monetary consequences, but there was no automated way to verify that a proposed rule change behaved consistently with the existing rule set before it reached production.
I designed and built a rule evaluator using Satisfiability Modulo Theories (SMT) solvers to formally verify tax rule engine updates before deployment — processing roughly 2.25M rule evaluations per configuration deployment. Rather than spot-checking a handful of test cases, the SMT-based approach let us reason about rule behavior across the space of possible inputs.
On top of the core evaluator (Java, AWS Lambda, SQS, DynamoDB, S3), I built comparison and reporting logic that surfaced behavioral inconsistencies as actionable reports, so engineers could see exactly what changed and why it mattered — not just that something did.
I integrated the tool into pre-production verification pipelines used by multiple teams, so the check happened automatically before a rule change could reach customers, rather than depending on someone remembering to run it.