The availability of big data, combined with rapid progress in training AI agents, has enabled us to deploy software solutions that effectively address the increasing complexity and continual evolution of socio-economic and legal landscapes. Consequently, modern society is becoming increasingly reliant on software to resolve issues with legal, social, and economic implications. A case in point is tax preparation software, which now assists over 72 million Americans annually in filing their returns, significantly easing the collective burden of navigating the ever-growing complexity of U.S. tax laws. Given their socio-economic and legally critical implications, ensuring software accountability—encompassing qualities such as legal compliance, explainability, perceptions of procedural justice, fairness of outcomes, and confidentiality/privacy—is of paramount social importance. Moreover, software that accurately interprets its requirements, complies with legal standards, and upholds social fairness can serve as a surrogate for legal and social norms, enabling policymakers to inquire about the law as seamlessly as a software engineer conducts a test.

Over forty years of research within the formal methods and software engineering communities have produced a range of principled approaches and powerful tools—such as formal property testing, automated fuzzing and debugging, program analysis, and satisfiability/constraint solving—that aid developers in enhancing the trustworthiness of critical software. Can we leverage this infrastructure to develop a computational framework that uncovers and explains accountability bugs in critical socio-legal software? Unfortunately, finding and explaining these accountability bugs in software implementations is remarkably difficult. A key obstacle stems from the challenge of reifying actual requirements in a formal, unambiguous language. The second challenge is the so-called oracle problem, where the ideal expected output for a given input is unavailable, often requiring potentially adversarial deliberation by experts. Finally, due to evident privacy and legal concerns, trustworthy datasets are difficult to access.

Drawing from our experience in debugging U.S. tax preparation software, we propose that these challenges can be tackled by focusing on relational specifications. While the exact output for a given input may be unknown, the relationship between the outputs of two related inputs may be easier to express. We demonstrate the applicability of metamorphic debugging over an open-source US tax preparation and a poverty management software. We show that challenging requirements from various US IRS publications — including Form 1040, Publication 596, Schedule 8812, and Form 8863 — as well as Pennsylvania benefits eligibility handbooks can be expressed as metamorphic relations. We also report critical accountability bugs found by two metamorphic debugging tools.