As model-driven code generators have increased in capability and in performance, so too has their use in mission-critical software development. One benefit of auto-generated code over handcrafted, individually created source code is that it is simpler to verify the code for mathematically specified requirements and for the absence of safety violations. Automatic theorem provers (ATPs) used to verify the program depend on user-provided axioms that encode domain-specific model information and knowledge used by the prover. The auto-generated code can be verified by the ATP, while the proofs provided by the ATP can be checked in a proof checker, which leaves the axioms as a potential source of unchecked errors and ultimately the potential cause of software failure.

In this paper, the authors propose an axiom verification framework to check that the axioms are correct and not unsound due to some implicit but incompatible interpretation. Within this framework, the tester is required to provide a computational model of the axiom logic by providing interpretations for function symbols within the Haskell programming language. The axioms are thus converted into executable functions within Haskell, and existing tools are used to both construct test data and evaluate the axioms for correctness. Failing axioms are provided with counterexamples from the framework.

After writing code for over two decades, I require no convincing of the benefits of early-stage testing. Any endeavors to improve testing and reduce software failure rates need to be applauded. My one criticism is that much of this paper may prove difficult to penetrate for readers outside the Haskell developer community.