Exhaustive Differential Verification of Rule Execution in Building Compliance Software: A Method and Its Application to Seismic Provisions for Earthen Buildings

Digital compliance tools increasingly stand between building regulations and the people who apply them, yet research on automated compliance checking has concentrated on whether a rule can be extracted from regulatory text rather than on whether the extracted rule is then executed correctly, so tools issuing compliance verdicts circulate without evidence of computational fidelity. This study proposes a verification method for the large class of provisions stating their requirements as algebraic inequalities over measurable building dimensions. The method combines division-free formalisation, cross-validation against an exact rational oracle, exhaustive enumeration of the discretised design space, differential comparison using asymmetric error classes, and a boundary coverage test suite. It was applied to the wall geometry provisions governing earthen buildings in Peru and Ecuador and to a mobile tool in free circulation. Exhaustive enumeration at the full input resolution of the tool, over 292,364,966,481 configurations, indicates that 7.93 percent of the baseline domain is admissible and that 72.1 percent of inadmissible configurations violate two or more requirements at once. The audit identified three execution defects; the rule sets disagree over 8.26 percent of the domain, and 55.9 percent of the verdicts issued lack normative support. A corrected version reproduced the reference verdict in all 32 device-executed test cases against 24 of 32 for the original, and agrees with the reference on every one of the 292,364,966,481 enumerated configurations. Applying the method to a second provision, the slenderness limit of EN 1996-1-1, reproduces the same defect signature in an unrelated code. Verification of rule execution is therefore inexpensive and necessary before compliance tools can be relied upon on site. The conditions under which the method applies are stated explicitly and are met by provisions in several codes, although transferability beyond the two cases examined remains to be demonstrated empirically.