Abstract Large Language Models perform well at natural language interpretation and reasoning, but their lack of formal correctness guarantees limits their adoption in regulated industries like finance and healthcare that operate under strict policies. To address this limitation, we launched Automated Reasoning checks (ARc) : a public service that (1) uses LLMs with optional human guidance to formalize natural language policies, allowing fine-grained control of the formalization process, and (2) uses inference-time autoformalization to validate logical correctness of natural language statements against those policies. ARc performs multiple redundant formalization steps at inference time, checking the formalizations for semantic equivalence. Our benchmarks show that ARc exceeds 99% soundness and achieves a near-zero false positive rate in identifying logical validity. Our approach produces auditable artifacts that substantiate the verification outcomes and can be used to improve the original text. ARc is the first commercial offering from a major cloud provider to integrate automated reasoning into a generative AI guardrail.

It is so inconceivable to debug a program without testing it that these two words are used nearly interchangeably. Yet we argue that using the concept of relative correctness we can indeed remove a fault from a program and prove that the fault has been removed, by proving that the new program is more correct than the original. This is a departure from the traditional roles of proving and testing methods, whereby static proof methods are applied to a correct program to prove its correctness, and dynamic testing methods are applied to an incorrect program to expose its faults.

Relative correctness is the property of a program to be more-correct than another with respect to a specification; this property enables us to rank candidate programs in a partial ordering structure whose maximal elements are the correct programs.Whereas traditionally we think of program derivation as a process of successive correctnesspreserving transformations (using refinement) starting from the specification, we argue that it is possible to derive programs by successive correctness-enhancing transformations (using relative correctness) starting from abort.One of the attributes of our approach is that it captures in the same mathematical model, not only the derivation of programs from scratch, but also most (if not all) of the activities that arise in software evolution.Given that most software is developed nowadays by evolving existing products rather than from scratch, any advance in the technology of program transformation by correctness enhancement stands to yield significant practical benefits.

In the process of trying to define what is a software fault, we have foundthat to formally define software faults we need to introduce the conceptof relative correctness, i.e. the property of a program to be more-correctthan another with respect to a given specification. A feature of a programis a fault (for a given specification)only because there exists an alternative to it that would makethe program more-correct with respect to the specification.In this paper, we explore applications of the concept of relative correctness in programtesting, program repair, and program design.Specifically, we argue that in many situations of software testing,fault removal and program repair, testing for relative correctnessrather than absolute correctness leads to clearer conclusions andbetter outcomes. Also, we find that designing programs by stepwisecorrectness-enhancing transformations rather than by stepwise correctness-preserving refinements leads to simpler programs and is more tolerant of designer mistakes.