1 Introduction↩︎

Formal specifications for modular code, in terms of contracts or postcondition assertions, have been a cornerstone in enabling robust and effective software development. Formal specifications realized as runtime checks enable testing code at the unit level, enable formal verification efforts, and enable evolution of software where modules can be swapped with others that satisfy the same specifications. The paradigm of Design by Contract [1] concretizes this approach to development of software, and several specification languages for contracts have been developed over decades, ranging from Eiffel [2], JML [3], Spec# [4], and Code Contracts [5], the latter two at Microsoft. However, despite the advantages, we have always struggled in getting programmers to write formal specifications, primarily due to it being perceived as a “burden” that slows the time to ship out software.

The advent of AI opens up two avenues that transform the framework of writing code with contracts. First, AI opens up the exciting possibility of natural language specifications that are then autoformalized into formal and executable contracts (executable logics). This considerably lowers the burden of writing formal specifications, and is akin to current documentation that is used for understanding code between human software developers. Second, AI-based automated coding/programming has made great advances in recent years, allowing programmers to simply state the intent of their programming task. This however creates a large gap between the intent of the programmer and the code [6]. Formal specifications can help bridge this gap— we can have developers write natural-language specifications at the level of modules, and have autoformalization of these assertions used to check the AI-written code using testing, or even formally prove the code correct against derived formal specifications. This general framework sits well in specification-driven development using AI [7], [8], where structured, human-readable specifications are authored and maintained during AI-written code development.

The key problem that enables both the above applications is the problem of reliable autoformalization of assertions. Reliability is important— when the tool succeeds, we need to be able to trust that the formalizations are faithful translations of the natural-language specifications. More formally, in addition to the usual accuracy metric, we are interested in high precision of the translation framework, i.e., in reducing the number of incorrect translations. We identify and address two key challenges for autoformalizing assertions: (a) how do we effectively assess the faithfulness of the formalization, (b) how do we resolve the inherent ambiguity in specifications written in natural language?

While the former problem is a general problem in autoformalization, the latter has unique aspects in the setting of translating assertions. In particular, ambiguities in natural-language assertions are particularly troublesome when they interpret a valid assertion as an invalid one (raising false positives that lead to doubting the code is correct) or interpret invalid assertions as valid assertions (leading to the assertion not checking the user intent, and hence passing buggy code). Consequently, in our work, we propose to return both the most likely valid and invalid formalizations of the natural-language assertion. Furthermore, when reasonably likely valid and invalid formalizations exist, we propose active learning algorithms to query the user further in order to disambiguate the assertion.

In contrast, several existing works on autoformalization of specifications in the literature instead make the implicit assumption that the assertion is expected to be valid [9]–[11]. While it is tempting to make this assumption in order to disambiguate the meaning of an assertion, these techniques are not useful in a context where there is no such expectation on the assertion being valid. For example, when the programmer is writing assertions to test the code, clearly such an assumption of validity is counterproductive. Also, in the context of using assertions to validate AI-written code, it is crucial to not assume the assertion is valid on that code!

We need a technique to check whether assertions are valid or invalid, and a key idea in this paper is to analyze the code to vet the autoformalization. More precisely, we analyze the behavior of the program on automatically generated test inputs to determine the validity/invalidity of assertions.

In this paper, we propose a framework of autoformalization using a combination of LLMs and program testing that (a) evaluates the confidence of various formalizations of assertions using a novel technique called clausal coverage, (b) generates both the most likely valid formalization and the most likely invalid formalization, using metrics that include the clausal coverage metric, and (c) if necessary, disambiguates between the most likely valid and invalid formalizations using active learning by querying the programmer.

The clausal coverage technique is a key technical contribution of our work. We translate the formal specification back to natural language, and then ask LLMs whether every clause in this NL specification is matched by a clause of the original specification, and vice versa. We ask the LLM to provide a conformance score that captures how well the clauses match, and utilize it to estimate how robust the formalization is.

We emphasize that our work caters to autoformalizing assertions written at the level of modules/code. In the context of AI-written code, our proposed tool helps programmers write module-level specifications (in addition to overall intent) that are then vetted against the code using autoformalization and testing. We do not attempt to solve several closely related problems studied in the literature such as (a) formalizing higher application-level intent of a programmer [6], or (b) mining formal specifications from documentation in natural language [12], [13]. Our solutions, in particular the clausal coverage technique and active learning, rely on the fact that localized natural-language assertions are being formalized.

We target formalizing contracts/assertions for a rich class of specifications of object-oriented code that encapsulates data and provides interface methods. The methods include those that have effects as well as those that are pure observer methods that return information of the underlying object. Our formal specifications are based on writing logical assertions involving the rich class of observer methods on objects. The logics we target are expressive, involving Boolean combinations, bounded quantification, and multiple sorts (objects, integers, etc.). We target realistic specifications of such modules.

Benchmarking, Implementation, and Evaluation

We curate several benchmark suites containing NL specifications and corresponding ground-truth formal specifications. The datasets span both synthetically generated NL specifications and manually written ones, and contain both valid and invalid assertions. Together, the datasets contain a total of 541 (NL spec, formal spec) pairs across 22 Java classes that represent collection-like data structures. We implement our approach in a tool called Monty and evaluate different research questions.

Our experiments show that Monty is effective at autoformalizing NL specifications. In particular, our approach significantly improves the precision of autoformalization beyond simply using an LLM, i.e., how likely is it that a generated response is correct? As may be expected, the effect is more pronounced with smaller models, and Monty used with Qwen2.5-Coder (a 32B parameter model, considered relatively small) improves the precision from 75% to 91.6% on one dataset, and from 64% to 85% on another dataset. We also show that the improvement in precision is obtained while still maintaining a high recall, which shows that Monty improves the reliability of autoformalization without affecting the availability of correct responses from raw LLM translations. Finally, we also perform several ablations relating to the choice of backbone model, the conformance checking approach we contribute, and the active learning. The most interesting observation among these is that our clausal coverage method appears to be the best approach for conformance checking, outperforming baseline approaches similar to those found in related literature.

2 Illustrative Example↩︎

We illustrate our pipeline with an assertion for a method in the standard ArrayList Java class [14]. The add(int index, E element) method inserts an element at a specified position, shifts the existing suffix to the right, and then increments the size of the list. One natural-language specification for this method is:

“If the index is valid, the value at the index after insertion will be the inserted element.”

Figure 1 shows the skeleton of the ArrayList class that we provide as an input to our pipeline. Notice that the skeleton also contains the stubs of methods other than add. These are observer methods, which are side effect-free functions that serve as atoms for the formal specification vocabulary (see Section 3 for a more formal presentation). In this case, the observer methods are get, which returns the value at a given index, and size, which returns the size of the array list. The skeleton includes documentation strings and method signatures for the observer methods as well as the target method signature. The comment marked with @@@ denotes the natural-language assertion to be formalized.

Although the NL assertion appears straightforward, a faithful formalization must avoid many pitfalls, both in terms of natural language understanding and writing semantically correct assertions for the underlying programming language. We illustrate these challenges by walking through the different stages of our solution architecture below.

4pt

Generating Candidate Formalizations using LLMs↩︎

Given the NL specification and the code skeleton above, we first use an LLM to generate candidate formal specifications in JML (Java Modeling Language)[3]¹. Let us say that the LLM produces the five candidate formalizations shown in Table 1. These assertions are in fact representative of the different scenarios we encountered in our experiments.

These candidates can suffer from a variety of errors. Most importantly, as explained in Section 1, we do not know if a given candidate conforms to the original natural-language assertion. Second, although it is true in this case, our solution approach also does not presume that the given assertion was valid for the method, and therefore we cannot simply filter for the valid formalizations (say, via testing).

Choosing Likely and Faithful Formalizations↩︎

The second stage of our approach ranks and filters candidate formalizations using two complementary signals. First, we use a test generator to compute a validity score that captures whether an assertion is well-formed, and whether it is valid for the given method with respect to a set of tests generated by a test generator. Second, we compute a conformance score that estimates how well a candidate formalization covers the intent of the original NL specification.

The validity score is computed through a sequence of checks:

• Syntactic check: checks whether the candidate is syntactically and semantically well-formed, i.e., whether the formal assertion can compile without error

• Fuzz-Safety check: checks (using a fuzzer) whether the assertion is itself safe, i.e., that evaluating the assertion does not raise a runtime exception.

• Fuzz-Semantic check: checks (again, using a fuzzer) whether the candidate is test-valid or test-invalid for the given method.

Note that our candidate assertions can use the \old(e) operator to denote the value of the expression \(e\) in the pre-state of the method. These are computed simply by memoizing the corresponding values in the pre-state.

In the context of our example, the validity checks eliminate Candidate #4 in Table 1 because it has an extra parenthesis, making it syntactically invalid. Additionally, note that Candidate #1 fails the fuzz-safety check since it does not use a null-safe interpretation of equality.

The conformance score provides a complementary signal. To determine this score, we ask an LLM to describe the given formal assertion in natural language. We then ask an LLM to compare the clausal structure of this description against the original NL assertion and provide a measure of conformance between them (with \(1\) being the best possible score). At a high level, candidates whose semantic content overlaps better with the original NL assertion receive higher scores, whereas those with missing, irrelevant, or conflicting content receive lower scores. This mechanism of using LLMs to provide numerical scores is known as LLM-as-a-Judge in the machine learning literature [15]. In our example, the LLM provides the following NL description for Candidate #1:

“If the index is at least 0 and at most the size of the list before the insertion, then after the add operation the element at that index equals the inserted element.”

This sentence is compared with the original specification for bidirectional clausal coverage, i.e., whether each substantive clause in one is represented in the other. In this case, the LLM judge assigns a perfect score of 1.0, because it does not find any differences. In contrast, the description for Candidate #3 begins as follows: “If the index is greater than or equal to 0 and less than the list size before the insertion...”. The LLM judge then correctly identifies that “less than the size” misses an edge case compared to the original NL assertion, and therefore provides a lower score.

We repeat the scoring process several times and average the LLM judge’s scores. We set a threshold for the average conformance score and eliminate the candidates that do not meet this threshold. In our experiments we set the threshold to \(0.6\), which eliminates Candidate #3 in this example.

4pt

Table 2 summarizes the validity and conformance results for the candidates.

One of the key challenges in autoformalization is the inherent ambiguity in natural language. The ambiguity arises from several sources, among which is the fact that we do not know whether the original NL assertion is meant to be valid for the method. For example, when writing formal documentation, one may wish to always choose the formalization that is valid, whereas when attempting to find bugs in human or AI-written code, the more appropriate choice could be the formalization that reveals an assertion failure.

Therefore, among the remaining candidates we choose the candidate with the highest conformance score among those that passed the fuzz checks, and similarly one from those that failed the fuzz checks. In this case, that decision returns Candidate #0 and Candidate #1 as the most likely and faithful formalizations.

Final Disambiguation using Active Learning↩︎

The final stage of our pipeline disambiguates between the likely and faithful autoformalizations using active learning. The idea is that the programmer can look at the distinction between the two candidates and determine the better formalization of the intended specification. In our work we utilize the modality of active learning where we produce a concrete valuation that distinguishes the two candidate formalizations. The user (or an automatic oracle) then determines whether the intended specification would satisfy this valuation, and we pick the corresponding formalization.

In this example, Candidate #0 and Candidate #1 are distinguished by the case where the inserted element is null. We use the test generator to come up with the distinguishing valuation. In our experiments, we simulate the user using an automatic oracle that is given the ground-truth, and answers using this ground truth. In this example, our framework ends up selects Candidate #0.

3 Preliminaries↩︎

In this work we study the autoformalization of specifications in the realm of object-oriented programming. We now provide some background to formalize the vocabulary we employ in the paper.

Specification Language

Our specifications are written at the method level for methods in a class. We identify for each class a set of observer methods, which are essentially side-effect-free methods (mathematical functions) that compute useful attributes of an object at a given state. For example, in our illustrative example in Section 2 we utilized the observer method size in the ArrayList class. Observer functions are a standard feature in specification languages for object-oriented programs, especially in paradigms inspired from Design-by-Contract [1]. Observer functions are the only methods in a class that can be utilized in specifications. Specifications can also, of course, express properties of input parameters to a method and their return value.

At a high level, our assertion language is essentially the same as the Java Modeling Language (JML) [3]. Given a function with input variables \(\overline{in}\) and output variables \(\overline{out}\) (represented as \(\mathit{\backslash result}\)), our assertions can use the input and output variables, observer methods, implications, equality, Boolean operations, and certain basic operations for the various datatypes involved, e.g., inequalities and arithmetic operations for integer-typed values or specialized .equals functions for object types. We denote the values of observer functions \(f(\mathit{args})\) on object variables \(o\) by \(o.f(\mathit{args})\). The special variable \(\mathit{this}\) denotes the default current object for the class under consideration.

We also allow bounded quantification in assertions, e.g., \(\forall i\) ranging over \(0 \leq i < o.\mathit{size}()\) for an array \(o\). Finally, we use the operator \(\mathit{\backslash old}(e)\), which takes an expression \(e\) and evaluates it in the pre-state of the method. For example, to say that the size of the object increases by \(1\) compared to the pre-state, we would write \(\mathit{this}.\mathit{size}() == \mathit{\backslash old}(\mathit{this}.\mathit{size}()) + 1\).

Test Generators

In this work we use test generators as verification oracles to judge the validity of assertions on methods. The test generator constructs a collection of well-formed inputs and checks the method under test for assertion violations within a given resource budget. In particular, it only constructs valid and reachable program states, by using constructors and other factory methods to construct valid objects and then calls the method under test. In our experiments we use Randoop [16].

4 Problem Statement and Methodology↩︎

Problem Statement↩︎

We begin by stating our problem of study. We fix a logic \(\mathcal{L}\) over which our framework is parameterized. In this work, the logic \(\mathcal{L}\) is always “executable”, that is, given a method and a formula in \(\mathcal{L}\), it is possible to evaluate whether a given behavior of the method (inputs and outputs) satisfies the formula. Examples of such executable logics include the assertion libraries or sub-languages supported by any number of programming languages. In our experiments, we use an executable sublanguage of JML [3] as our logic for formalizing specifications.

Let us fix a module \(M\) (we use class and module interchangeably) consisting of several methods \(m\), each over a set of input variables \(\overline{in}\) and output variables \(\overline{out}\). The module may also optionally contain documentation strings \(d_m\) for each method \(m\). As explained in Section 3, in this work we consider specifications in the setting of object-oriented programs, so we also fix a formal object variable \(o\) of the class \(M\) to denote the calling object.

Note that techniques for solving the above problem are of course allowed to use all the information in \(M\), including the signatures, documentation, and code for any of the methods. The above definition captures the minimal set of entities needed to define the problem.

Our definition above contains a couple of curiosities. First, we use the term faithful to refer to the intuitive notion of a correct translation of a natural-language specification. Second, we do not ask for the authoritative faithful formal translation, since natural language is inherently ambiguous. We discuss these challenges in detail below. We note here that in general the problem in Definition 1 is under-specified, and we therefore utilize the standard practice of evaluating the performance of solutions to the problem on datasets containing ground-truth formal assertions.

Challenges↩︎

In this work we combine the powerful formalization abilities of LLMs and other tools such as fuzz testing and active learning to build techniques for autoformalizing natural-language assertions. We identify two key technical challenges in this process.

Challenge 1: Identifying equivalence between natural language and formal language statements.  The concept of “equivalence” between a natural language statement and a formula is intuitive to humans who are familiar with expressing formal logic. For example, \(x > 0\) is a faithful translation of the statement “\(x\) is positive”, but \(x <0\) is not. However, since the semantic content of an assertion can itself be complex and expressing formulas involves dealing with intricate logical operators, it can happen that LLMs do not faithfully translate natural-language assertions. They can suffer from a variety of issues, including specification language misuse, semantic overreach or overfitting to common cases, and depending on the model they may just plainly forget to formalize certain parts of a natural-language assertion [17]. One way of addressing this problem without performing post-training is to utilize a mechanizable definition of equivalence between a natural language utterance \(s\) and a formula \(\psi\) that approximates the intuitive equivalence as well as possible. One can then sample many outputs from an LLM, and filter out the candidates that do not pass the equivalence check. In this work we tackle the issue of identifying equivalence by introducing a technique called clausal coverage conformance checking. Challenge 2: Tackling inherent ambiguity in natural language.  The above challenge concerns the issue of tracking the semantic content that is explicitly present in an NL assertion. However, natural language is inherently ambiguous, and it is not always possible to identify a single formal concept that corresponds to a natural language utterance. For example, people use the word “positive” in an informal sense to mean both strictly positive and non-negative, depending on the context. Another example documented in prior work on human understanding of LTL [18] is phrases like “the red light is on until the blue light comes on”, which does not clearly specify whether the red light continues to be on or if it turns off when the blue light turns on. Note that both of these translations would be faithful to the original utterance, and are therefore not resolved by our solution to Challenge 1.

Monty Architecture↩︎

We now describe Monty, our methodology for faithful autoformalization of specifications. Our overall pipeline is depicted in Figure 2.

We first prompt an LLM with the module and method under consideration, as well as the NL specification \(s\). We also provide information about the target logic in the prompt, and a few in-context examples. (see Appendix 10 for the full prompt.) We then obtain candidate formalizations \(\psi_1, \psi_2,\ldots \psi_n\). The first stage of our architecture then calls, for each candidate formalization \(\psi_i\), (a) a test generator that evaluates whether \(\psi_i\) is test-valid for the given method, and (b) a conformance measurement module that measures the overlap in the semantic content between \(\psi_i\) and the original NL assertion \(s\). During this process we also eliminate syntactically malformed generations, or generations that do not compile without errors.

The second stage of our architecture is a decision matrix that takes the scores from the test generator and the conformance checker for all the candidates and returns the subset of them that are the most likely faithful formalizations. One of the key insights of our work is that inductive biases (e.g., presumption of validity) can be used to combat some of the inherent ambiguity in natural-language specifications.

The final stage of our system is an active learning loop that disambiguates between the remaining candidates. We detail the construction of the nontrivial modules in our architecture below.

Clausal Coverage Conformance Checker.  One of the key contributions of our work is the construction of a conformance checker to address Challenge 1 above, namely the judgment of semantic equivalence between an NL assertion and a formal assertion. Since natural language is inherently ambiguous, we would not want the conformance checker to pick up on details in the formal assertion that were not specified clearly in the NL assertion. Our key insight here is that inherent ambiguity typically manifests locally in the formal assertions, and it is therefore possible to rule out many bad formalizations by looking at the broad structure of the two assertions.

We call the resulting technique clausal coverage. We first ask an LLM to describe the given formalization in natural language. We then prompt the LLM to identify all the substantive clauses in the original NL assertion as well as the description, and ask whether the description is both (a) Sound: the description contains all the clauses in the NL assertion and (b) Complete: the description does not contain any information beyond what is given by the clauses in the NL assertion. We ask the LLM to provide a score in the interval \([-1,1]\) along with the following rubric: Positive scores indicate that the clauses in the original assertion were covered, with \(+1\) indicating perfect conformance. Negative scores indicate that parts of the formalization conflict with the original assertion, with greater negative scores indicating more serious contradictions between the two assertions. A zero score is a neutral judgment that encompasses many cases like unrelated content in the formalization, or a failure to clearly detect either conformance or contradiction. This method of using an LLM as a scoring function is known as LLM-as-a-Judge in the Machine Learning literature [15]. We repeat this evaluation multiple times and average the scores, accepting a formalization as faithful only if it exceeds a certain threshold. In our experiments we repeat the check \(8\) times and set the threshold to be \(0.6\). We provide the prompt that we use for conformance checking in Appendix 10. Though the above technique is intuitive, to our knowledge we are the first to utilize this approach for conformance checking. In fact, in our initial version of the architecture we used a conformance checking method based on Natural Language Inference (NLI) [19], similar to the recommendations found in contemporary works that mention conformance checking [20]. These contemporary techniques also recommend doing a “reverse translation”, and ask whether it is equivalent to the original input. However, we found that this only amplified the inherent ambiguity problem, and LLMs turned out to be overly sensitive to differences in phrasing. We evaluate ablations of our conformance checking technique in Section 6.

Decision Matrix and Inductive Biases.  The second insight of our work is that the inherent ambiguity in natural language can be addressed in part by incorporating inductive biases specific to the application domain. For example, if the statement “\(x\) is positive” yields both \(x > 0\) and \(x \geq 0\) as faithful candidate formalizations where only one of them is test-valid for the given method, we may be able to pick the valid one if we assume that the application demands a presumption of validity of the assertion on the part of the user writing the NL specification. This is often the case in documentation of code, and has been the default incorporated by other related works on specification mining (see Section 7). In contrast, if the user is writing assertions to identify edge cases and finding bugs, we may in fact want to choose the formalization that is not test-valid for the given method, and return the inputs that raise the assertion violation.

In our work we assume a more general setting with no presumptions about the validity of the assertions. Instead, we separate the generated assertions into test-valid and test-invalid ones, and choose the candidates with the highest conformance score from each category. Of course, we do not pick any candidates whose conformance score is below the acceptable threshold. The intuition behind our approach is that the best test-valid and test-invalid formalizations together capture the range of ambiguity in the original natural-language assertion. This is similar to the idea of a version space bounded by a general hypothesis and a specific hypothesis in traditional work on learning theory [21].

Active Learning Loop.  The final stage of our pipeline utilizes active learning to disambiguate between faithful candidate formalizations. The intuition is that the remaining candidates at this stage are the likely and faithful formalizations, and indicate the range of inherent ambiguity or under-specification in the original NL assertion. In this work we use the active learning paradigm that utilizes a teacher (typically the user) who can say whether a given data point satisfies the intended assertion. A data point here is a valuation over the entities/variables involved in the assertion. So, for example, if the original assertion is “If the inserted element is positive then the size of the array increases by 1”, the valuation would provide values for the inserted element, as well as pre- and post-state values for the size of the array object.

In this work the active learning only distinguishes between the two candidates that are returned by the decision matrix. We compare them using the test generator to produce a valuation (\(\overline{v}\) in Figure 2) that distinguishes them. In Section 2 this valuation was setting the inserted element to null. In particular, we ensure that the valuation is realizable, i.e., one that can actually be produced by the method’s transformation. For example, if the valuation involves both the old and new sizes of an object, we only ask the test generator to search over values for the old size, and execute the program to yield the size in the post-state. We then query the user to gather whether the intended formal assertion satisfies the distinguishing point, and pick the appropriate candidate. In our experiments we utilize datasets with ground-truth formal assertions and simulate the user by executing the ground-truth assertion on the distinguishing valuation.

Of course, it can happen that the decision matrix only produces one candidate that exceeds the conformance threshold, and we simply return that candidate in this case. One interesting scenario is when there are more than two candidates with sufficiently high conformance scores. One can then consider distinguishing between these using active learning. We do not entertain this scenario in this work, but it would be simple to make a sufficient number of pairwise comparisons (either all pairs or perhaps sequentially) and find distinguishing inputs as we currently do. We can also consider minimizing the number of distinguishing points to reduce user involvement, and there has been some recent work on this problem [22].

5 Benchmarking↩︎

We curate a suite of benchmarks for evaluating our approach from existing datasets. In particular, as we discuss in Section 7, existing benchmarks are not precisely aligned with our task of formalizing assertions, and hence we need some adaptation/curation. As such, the datasets we develop are one of the contributions of this work.

Our datasets are all centered around the formal assertions in the prior work of Zhai et al. called C2S [17]. The dataset published in this work contained a set of Java collection-style classes and formal specifications for the methods in those classes. We adapted this dataset, manually resolved errors in some of the formal assertions, and augmented it with more collection-style classes and formal specifications.

C2S-Augmented Synthetic Dataset. The first benchmark suite we develop is one where the NL specifications are synthetically generated from the formal assertions in the augmented C2S suite we describe above. We prompt Claude-Sonnet-4.6 to describe the formal specifications with concise and natural-sounding English statements. We obtain a suite of 416 (NL specification, ground-truth formal specification) pairs across 19 classes as a result. Buggy Dataset. The specifications in the augmented C2S suite are valid assertions. We therefore construct a Buggy assertion dataset to evaluate translation of natural-language specifications when specifications are incorrect or program contexts are inconsistent. This dataset is derived from a subset of the 19 classes described above. We create two variants: a buggy-code variant where we perturbed the code for the target method, and a buggy-assertion variant where we perturbed the specifications into incorrect or misleading assertions. Once again, we use Claude Sonnet 4.6 to produce the NL specifications for the buggy assertions.

Manual NL Specs Dataset. We also create a smaller dataset where we write the natural-language specifications manually. We choose three additional Java classes not included in the above set along with formal specifications. We then asked one of the authors to write specifications, with the only instruction being that they could look at the code and the documentation and needed to write an NL specification that would essentially capture the given formal specification. This author was not involved in the identification of the three additional classes or the formal specifications, and was also not shown any of the synthetically generated NL specifications from the above datasets. The author was, however, aware of the solution approach in the paper. This dataset contains 39 (NL, formal) specification pairs.

We provide a detailed account of the dataset statistics in Appendix 9.

6 Evaluation↩︎

3pt

We follow a routine experimental setup described in Appendix 12 and evaluate our implementation of Monty on the following research questions:

• RQ1: How effective is our approach at autoformalizing natural-language specifications?

• RQ2: What, if any, are the improvements our approach provides over purely calling an LLM to solve the task?

• RQ3: What is the effectiveness of our approach on manually written NL specifications?

• RQ4: How does the choice of backbone LLM affect autoformalization performance?

• RQ5: How effective is conformance checking in improving the faithfulness of formalizations? How does our approach compare to baselines?

• RQ6: How effective is active learning in the architecture?

We use the following task-level metrics throughout the evaluation (see e.g., Table 3). Any-Equiv measures the generation potential of the backbone LLM: it reports whether the candidate pool contains at least one assertion equivalent to the ground truth. This is essentially the Pass@5 metric. Oneshot is the Pass@1 metric: it measures whether the first generated candidate from the LLM is equivalent to the ground-truth assertion. This provides the baseline comparison of plainly calling an LLM to solve the task at hand. Monty-Acc measures the end-to-end accuracy of our approach: the final assertion selected by the full pipeline (and hence passing the conformance threshold 0.6) is logically equivalent to the ground truth. Monty-Prec measures the reliability of Monty outputs: among all tasks for which Monty returns a high-conformance (\(\ge0.6\)) final assertion, it reports the fraction whose final assertion is equivalent. This is a precision metric for the tool. In other words, when Monty returns a formal assertion, how likely is it to be correct? This is one of the most important metrics as it measures how accurate the tool is when it reports a formalization. Finally, Monty-Rec measures recall, i.e., how often Monty recovers a correct assertion when one is available: among tasks whose candidate pool contains at least one equivalent assertion, it reports the fraction for which Monty selects a logically equivalent high-conformance (score\(\ge0.6\)) final assertion.

We note here that Section 7 discusses several works on the related problem of mining formal specifications from natural language documentation using LLMs. To our knowledge, all these works either (a) plainly use an LLM, or (b) use an LLM to generate formal assertions and then weed out invalid ones using a fixed set of tests/test generator and a presumption of correctness. Our experiments essentially capture (a) using the Oneshot metric, and (b) via our evaluation ablating the conformance check (but only on benchmarks that have valid assertions). Another technique in the literature is the use of an LLM to ‘repair’ test-invalid assertions. We do not adopt this since we do not have a presumption of validity.

RQ1: How effective is our approach at autoformalizing natural-language specifications?↩︎

Table 3 summarizes the overall effectiveness of Monty across datasets and open-source backbone models. The results show two complementary effects. First, the LLMs are often able to generate at least one suitable candidate formalization, as reflected by the Any-Equiv metric. Second, given the generated candidate pool, our decision matrix and active-learning resolver effectively select a final candidate with high precision and recall. On the main C2S-Augmented dataset, GPT-oss achieves an overall success rate of 89.7%, while Qwen2.5-Coder achieves 75.7%.

The same trend holds across the additional datasets. On Buggy Code, Monty maintains high recall for both models. Performance is lower on Buggy Assertion, especially for Qwen2.5-Coder, reflecting the difficulty of formalizing misleading or incorrect specifications. This also suggests that LLMs have a noticeable bias toward producing valid-looking assertions or specifications, making it harder for them to synthesize intentionally invalid assertions from natural-language descriptions if one were to use them for, say, bug finding. Overall, these results indicate that Monty is effective across the evaluated datasets.

We also evaluated our pipeline on a variant of the above dataset where the NL specifications were generated by GPT-5, and we found that the results were materially no different from the ones presented in Table 3.

RQ2: What, if any, are the improvements our approach provides over purely calling an LLM to solve the task?↩︎

This is the main research question of this paper. With any methodologies that augment LLMs, the main baseline for comparison is the one that a naive user would resort to, namely simply calling an LLM with the task description and choosing the first response. While we do not use a naive prompt, we do capture this approach using the Oneshot metric.

Table 3 shows that our approach (Monty-Acc) generally performs improves over the Oneshot metric. On the main C2S-Augmented dataset, GPT-oss improves from an Oneshot accuracy of 85.3% to a Monty-Acc accuracy of 89.7%, while Qwen2.5-Coder improves slightly from 75.0% to 75.7%. The improvement is consistent on other datasets, especially for Buggy Code, where GPT-oss increases from 60.0% to 70.0%.

The more interesting results lie in the Monty-Prec scores. Note that since LLMs always provide a response, the Oneshot metric is also the same as the precision metric for plainly using an LLM. Table 3 shows that our approach significantly improves precision. The effect is more pronounced for smaller models: for Qwen2.5-Coder the precision improves from 75% to 91.6% on C2S-Aug, and from 64.1% to 85.2% on the manual specs dataset. Even on GPT-oss, which is a larger model, the precision increases from 80% to 88% on average. This is a significant difference and a promising observation, since practical adoption typically requires more than 90% precision (and more than 95% in many cases).

Table 3 also shows that the precision is improved without hurting recall. On C2S-Augmented, while the precision reaches 92.8% for GPT-oss and 91.6% for Qwen2.5-Coder, recall reaches 97.6% and 93.2%, respectively. Recall captures the complementary property to precision: when the candidate pool contains a correct formalization, a high recall indicates that the filtering process usually preserves it rather than discarding it. Together, these results suggest that the decision matrix improves reliability without substantially reducing the availability of useful outputs.

RQ3: What is the effectiveness of our approach on manually written NL specifications?↩︎

Machine-generated natural-language specifications can be more regular and templated compared to human-written specifications written by real developers. This raises the concern that evaluation on such data may overestimate performance if autoformalizing models exploit machine-generated phrasing patterns. To address this concern, we evaluate Monty on the Manual NL Specs dataset, where the natural-language specifications are written manually. As shown in Table 3, our tool still achieves meaningful end-to-end performance on these specifications: GPT-oss obtains an accuracy of 84.6%, while Qwen2.5-Coder obtains 59.0%. This suggests that the performance of Monty may be generalizable to real-world use cases with human users.

The precision and recall results further clarify how Monty behaves in this setting. For GPT-oss, the reported outputs have a precision of 86.8%, and the tool also recovers 97.1% of cases where an equivalent candidate is available. Qwen2.5-Coder is weaker on this dataset, but its reported outputs still have relatively high precision, 85.2%, with a recall of 85.2%.

RQ4: How does the choice of backbone LLM affect autoformalization performance?↩︎

10pt

Table 4 compares different backbone models on a randomly chosen subset of the C2S-Augmented dataset. We choose a subset owing to resource constraints. In addition to the two main open-source models, we evaluate three stronger backbones: Qwen3-235B-A22B-Instruct-2507 [23], GPT-5.5 [24], and Claude-Opus-4.8 [25]. Qwen3-235B is a larger model from the Qwen family, while GPT-5.5 and Claude-Opus-4.8 represent closed-source frontier models. For GPT-5.5, we use the medium effort. The results show that backbone quality has a clear effect on candidate generation. The smaller Qwen2.5-Coder model obtains an Any-Equiv score of 81.2%, whereas the larger or stronger models all exceed 90%, indicating that they are more likely to generate at least one equivalent formalization in the candidate pool. The Oneshot results vary even more substantially: Claude-Opus-4.8 and GPT-5.5 achieve the strongest first-candidate accuracy, 90.6% and 88.5%, respectively, while GPT-oss and the Qwen models are lower. At the same time, the precision remains high across all models, suggesting that the decision matrix can still select reliable outputs even when the first generated candidate is not consistently correct. Overall, stronger backbones improve raw generation quality, while Monty improves the reliability of the final reported formalizations across model families.

RQ5: How effective is conformance checking in improving the faithfulness of formalizations? How does our approach compare to baselines?↩︎

10pt

To isolate the effect of conformance checking, we evaluate it as a classifier: a candidate is predicted correct when its conformance score is at least \(\tau\), and the label is logically equivalent to the ground-truth specification. Figure 3 shows the ROC curve obtained by sweeping the conformance threshold \(\tau\); based on this tradeoff, we set \(\tau=0.6\), because it favors high recall while still filtering low-conformance candidates.

Table 5 reports performance at this threshold. On C2S-Augmented, conformance achieves strong F1 scores for GPT-oss and Qwen2.5-Coder, 93.3% and 85.4%, respectively. Recall is consistently high, showing that the filter rarely removes correct candidates. Precision is lower, confirming that conformance is not a correctness oracle, but still provides a useful signal for ranking and filtering. Qwen2.5-Coder performs poorly on Buggy Assertion, suggesting that smaller models struggle when many candidates look valid but do not match the intended specification.

Table 6 compares conformance implementations using AUC. Detailed explanation and visualization can be found in Appendix 13. Our full method achieves the best aggregate AUC, 0.659, outperforming other methods. The gap between Ours and Ours-noCtx shows that contextual information improves ranking quality. Although NLI performs well on Manual NL, its overall AUC and fixed-threshold behavior are weaker. These results support the use of a contextual, roundtrip-based bidirectional clausal conformance check.

5pt

RQ6: How effective is active learning in the architecture?↩︎

We evaluate the effectiveness of active learning across datasets. The learner is only invoked when the decision matrix identifies both a valid candidate and an invalid candidate. We find in our experiments that active learning only applies in a few cases in our datasets. In Table 5, Cases counts eligible active-learning tasks: tasks where the learner is invoked and at least one of the two competing candidates is equivalent to the ground truth. Accuracy measures whether the learner selects an equivalent candidate among these eligible cases. Although in practice it is useful to have active learning interactions be minimal to prevent user fatigue, we believe that a larger study may be needed to showcase a more complete picture of the prevalence of cases where active learning would be required.

7 Related Work↩︎

Traditional Specification Mining and Contract Inference↩︎

Traditional specification mining and contract inference aim to recover program properties automatically. Early passive techniques infer invariants or API protocols from observed executions and traces, such as Daikon-style dynamic invariant detection and trace-based protocol mining [26]–[31]. These methods are grounded in program behavior, but can only infer properties exposed by the observed executions and generally do not capture developer intent directly.

Later work combines dynamic analysis with testing, symbolic reasoning, predicate synthesis, and learning. For example, Sankaranarayanan et al. [32] combine dynamic and symbolic techniques for invariant inference, Padhi et al. [33] synthesize preconditions from execution data, and Astorga et al. [34], [35] learn stateful and object-oriented contracts with guarantees defined relative to a test generator. More recent work also mines specifications from natural-language API documentation and comments [13], [17]. Our work is complementary: we start from a natural-language assertion and study whether LLMs can autoformalize it to an executable assertion while preserving intent. Unlike prior mining approaches, Monty explicitly evaluates generated candidates along two dimensions: their execution-level validity and their semantic alignment with the user’s intended specification.

LLM-Based Specification Generation and Autoformalization↩︎

LLM-based specification generation has emerged along two main directions. The first translates natural-language requirements, documentation, or informal descriptions into formal artifacts such as regular expressions, first-order logic, temporal logic, contracts, and hardware assertions [9], [36]–[39]. These systems show that learned models can recover useful semantic structure from natural language, often with grammars, templates, interaction, or refinement to improve syntactic validity and reduce ambiguity.

The second direction generates specifications directly from code or program context. SpecGen [10] synthesizes formal specifications with LLMs and improves them through mutation-based refinement and verification-guided selection. SpecSyn [40] targets real-world program verification by decomposing programs and refining generated specifications based on semantic strength. SLD-Spec [41] focuses on complex loop functions, using program slicing and LLM-based logical deletion to remove irrelevant or incorrect specifications. AutoReSpec [42] further explores validator-guided collaborative LLM generation for improving verifiable specifications. Recent work has also used LLM-based extraction of specifications for libraries to prove a client correct [43].

Our work differs in that it targets module-level code contexts and explicitly starts from natural-language specifications, with the goal of formalizing them into executable assertions while preserving the user’s intended meaning.

Round-Trip Techniques for Specification and Verification↩︎

Round-trip techniques translate artifacts back into the original representation to expose information loss or semantic mismatch. In NL-to-formal-specification settings, prior systems use back-translation or subformula-to-text mappings to inspect, debug, or refine generated specifications [36]. Clover checks consistency among code, docstrings, and formal annotations through reconstruction tests [44], while Claimcheck back-translates verified Dafny lemmas to detect proof–intent mismatches [45]. Round-trip translation has been used for quality control in machine translation and software traceability, but is not always a reliable proxy for forward-translation correctness [46].

Our conformance check adapts this idea to assertion autoformalization. Rather than simply prompting an LLM to judge equivalence, it evaluates bidirectional clause-level coverage with relevant code context, including method signatures, arguments, return values, and documentation.

8 Conclusions↩︎

We present Monty, a pipeline for autoformalizing natural-language specifications into executable assertions by combining LLM-based candidate generation with a decision matrix based on execution-level validity and semantic-level conformance, together with an active-learning loop for disambiguation. Rather than relying on a single raw LLM output, Monty generates multiple candidate formalizations, checks their executable behavior, estimates their alignment with the intended specification, and selects a reliable final formalization when possible. Across multiple datasets and backbone models, our results show that Monty improves the reliability of the formalizations it reports. The ablation studies further show that contextual, roundtrip-based bidirectional clausal coverage provides an effective conformance signal for candidate selection.

9 Detailed Statistics of Datasets↩︎

Table 7 reports the detailed composition of the datasets used in our evaluation. Each entry counts the number of assertion-generation data points for a given class, where one data point consists of a code context, a natural-language specification, and the corresponding ground-truth formal assertion. The C2S-Augmented dataset is our main benchmark and contains 416 data points across 19 Java collection-style classes. C2S-Augmented Sub is a 96-data-point subset used for more expensive ablation and comparison experiments. Manual NL contains 39 human-written natural-language specifications over three additional classes. The Buggy Code and Buggy Assertion datasets are derived from selected C2S-Augmented classes and are used to evaluate robustness under perturbed implementations and incorrect assertions, respectively.

6pt

10 Prompt Design↩︎

Candidate-generation prompt↩︎

The candidate-generation prompt asks the LLM to translate the natural-language assertion marked by @@@ into exactly one executable assertion. The prompt includes a small number of in-context examples and explicitly describes the supported logic syntax, including \old(...) for pre-state values, \result for return values, => for implication, and \forall for universal quantification.

Your task is to read java code and output exactly one assert statement (specification) corresponding to the comment that starts with "@@@". 
Your statement should accurately reflect the natural language assertion. Make sure to include all relevant details (such as premises, bounds, or branch cases), and avoid leaving out information or adding anything extraneous.
You can think step by step before coming up with the final answer, but please make sure that your final answer (the java code of the assert statement) is displayed in a <code></code> block.

Here are some rules and tips:
1. If the assert statement needs to access the value of an expression at the beginning of the function, you can use the `\old(expression)` syntax.
2. To refer to the return value of the method in the assert statement, you can use the `\result` variable.
3. To write A implies B or B happens if A holds, you may use the `A => B` syntax. Keep in mind that `=>` is binary with exactly two operands, and `=>` has lower priority than operator `&&` and `||` so use parentheses to ensure correct grouping.
4. If the assert statement needs to express that the `spec` should hold for each int variable `i` where `cond` holds, you may use `\forall int i; cond; spec` syntax.
5. Use only publicly accessible observer methods provided in the test function. (Use `\result` instead of calling the observer method that is being tested.) All function calls in the test function should be of the format `this.func_name(args_list)`.

[Few-shot Java examples]

Now, read the following java code and output an assert statement corresponding to the comment that starts with "@@@".

{TARGET_CODE}

Roundtrip translation prompt↩︎

For roundtrip checking, we first translate a generated formal assertion back into natural language. We use the precise mode so that the roundtripped description preserves premises, bounds, old-state references, return-value references, null cases, equality conditions, and logical connectives.

Your task is to read java code and write a natural language assertion that describes a specific logical specification in the code.

Here are descriptions for some syntactic symbols in JML logic:
1. If the assertion uses "=>" or "==>", such as "A => B", that means "A" implies "B".
2. \old(expression) means the value of expression before the method is executed.
3. \result means the return value of the method.
4. "\forall var i; cond; spec" means that the "spec" should hold for all the "i" such that "cond" holds.

Please try to make your translation as consistent as possible. Your translation should be equivalent to the original assertion. Do not include anything extra, and also do not leave anything out, especially premises.
Also write the translation as if you were a careful human engineer writing contract specifications for this code in plain English: follow the logic of the code naturally, make the statement fluent, clear, and easy to read, and prefer ordinary human phrasing over formal logical wording.

Translate the formal assertion as accurately and completely as possible: preserve every premise, bound, quantified condition, old-state reference, return-value reference, null case, equality condition, and logical connective in the natural language assertion.
Do not summarize away implementation-level details when they affect the exact meaning. Include all details from the formal formula in natural language, even if the resulting sentence is longer.
For example, if an assertion says something like "index>=0 && index<=size", explicitly state that the index is greater than or equal to 0 and less than or equal to size. Likewise, if an assertion uses a null-safe equality pattern like "a==null && b==null || a.equals(b)", explicitly mention both the case where both values are null and the case where one value equals the other.

Your output should be one single line starting with "// @@@ "
Here are several examples for your reference:

[Few-shot Java examples]

Now, read the following java code:

{TARGET_CODE}

Write a natural language assertion that describes the assertion code: {TARGET_ASSERTION}.
Please directly output your answer without any other information.

Conformance-scoring prompt↩︎

After roundtrip translation, we compare the original natural-language assertion with the roundtripped natural-language assertion. Our main conformance checker uses a contextual, component-level prompt. It asks the model to score how well the hypothesis preserves the premise, where the premise is the original specification and the hypothesis is the roundtripped specification.

You are performing a **roundtrip conformance check** between:
(1) a natural-language post-condition (the "premise"), and
(2) a second natural-language statement (the "hypothesis") that is a natural-language translation of a generated post-condition formula.

Your job is to judge how well the hypothesis conforms to the premise under the following responsibility:

Conformance responsibility
1) Completeness: The hypothesis must not omit any component that the premise intends.
   - Every component mentioned or implied as an intended constraint in the premise should be present in, or entailed by, the hypothesis.
2) Soundness: The hypothesis should not introduce unrelated or unjustified components.
   - Ideally, every component in the hypothesis should be traceable to the premise's intention.
   - In practice, *minor reasonable supplementation* is allowed (e.g., explicit bounds/ranges, type conversions, edge-case handling) as long as it does not change the intended structure or meaning.

What counts as a "component" (treat these as the primary comparison units)
- Entities / terms: the return value or result, method parameters, object fields, collection elements, indices, sizes, old/pre-state values, and new/post-state values
- Quantification / scope: statements about all items, any item, no item, a particular item, or a restricted subset of items
- Bounds / ranges: valid index ranges, quantified ranges, numeric limits, and whether endpoints are included or excluded
- Predicate relations: equality, inequality, ordering/comparison, containment/membership, nullness, type/compatibility requirements, and method-call properties
- Logical structure: conditions ("if/when/only if"), conjunctions ("and"), alternatives ("or/either"), negation ("not/no"), implications, case splits, and grouping/precedence implied by the sentence

Evaluation principle
- This is a *structure- and alignment-focused* check: prioritize whether the hypothesis preserves the overall logical skeleton and aligns each segment/component to the premise.
- Ignore superficial wording differences and synonyms of technical terms.
- Ignore fine-grained details; focus on whether the same structural components are present and aligned, and whether their logical relationships (quantifiers, bounds, predicates, connectives) match.
- The hypothesis may be imperfectly phrased or not fully "compilable" as a formula; still score based on whether the intended components/structure match.
- Do not purely evaluate on literal text similarity; instead, reason about semantics and structure in the context of target code behavior. (The context information is given below.)

Scoring (real value in [-1.0, 1.0])
Interpret the score as a combined measure of:
- Completeness (missing components/segments -> lower score)
- Soundness (unjustified extra components/segments -> lower score)
- Logical compatibility (contradictions/incompatible constraints -> negative score)

Use these anchor points (you may output intermediate values like 0.8, 0.2, -0.3):
+1.0 Perfect Conformance:
  - Hypothesis preserves all components and the logical structure of the premise (may rephrase wording).
  - Hypothesis may add minor, clearly reasonable supplementation (e.g., explicit bounds/ranges, type conversions, edge-case handling) as long as it does not change the intended structure or meaning.
+0.5 Mostly Conformant / Minor Loss:
  - Hypothesis is consistent with the premise but omits some non-trivial components, weakens constraints, or only covers a subset of cases.
  - Or adds some unrelated or unjustified content while the core structure still mostly aligns with the premise.
0.0 Neutral / Not Established:
  - The hypothesis is largely unrelated to the premise's components/structure, OR
  - The hypothesis introduces new requirements not supported by the premise, OR
  - The hypothesis omits essential segments such that conformance cannot be verified from it.
-0.5 Partially Conflicting:
  - Some aligned components exist, but at least one important segment contradicts the premise (e.g., flipped inequality, negation, wrong old/pre-state reference, implication reversed, incompatible bound).
-1.0 Completely Conflicting:
  - The core structure/meaning contradicts the premise and cannot hold simultaneously.

For instance,
[Few-shot examples]

Here is the context information to help understand the sentences:
The sentences are assertions in natural language form describing the expected behavior or properties of a piece of java code, such as a function or method.
More specifically, you are given the implementation of a class [Class name]. Inside this class, there is a method [Method name]. The following two assertions are both written about the behavior of the method. To help you reason about their relationship, here is some context:
- The method takes in ([Parameters]) as parameters.
- [Return information]
- The functionality of the method is documented below:
[Method documentation]

Output format:
- First, briefly explain your reasoning process in 1-3 concise sentences.
- Then, output only your decision as real-valued score wrapped in <ans> </ans> tags.
- Place exactly one score inside the tags. Do not include anything else inside the tags.

Here are the two assertions to evaluate:
The premise is: [Premise]
The hypothesis is: [Hypothesis]

11 Details on Test Harness Construction↩︎

For each generated assertion, our implementation constructs an executable Java test harness that checks the assertion over inputs generated by Randoop. The construction has four main steps: parsing the target context, translating the assertion formula, composing the target-method call, and embedding the translated formula into a test method.

11.0.0.1 Parsing the target context

Given the code skeleton for a data point, the implementation first extracts the class name, import declarations, method signatures, method arguments, return type, documentation string, and whether the target method is a constructor. We treat the last method in the skeleton as the target method to be checked. The remaining public observer methods, such as size(), get(), contains(), indexOf(), and isEmpty(), are available to generated assertions and to the generated test code. The generated test method takes an instance of the target class, named fuzzobj, together with the original target-method arguments. For example, for ArrayList.add(int index, E element), the test method receives ArrayList<E> fuzzobj, int index, and E element.

11.0.0.2 Extracting the assertion formula

The checker expects each candidate to contain exactly one assertion of the form assert formula;. The implementation extracts the inner formula and normalizes implication operators such as ==>, ->, and => into a single implication operator =>. It then rewrites references to the receiver and return value: this is replaced with the generated receiver variable fuzzobj, and \result is replaced with the generated return variable New_Ret. The resulting formula is the basis for all later code generation.

11.0.0.3 Handling pre-state expressions

Assertions may refer to pre-state values using \old(e). For each such expression, the implementation creates a fresh variable, such as OLD_var0, and emits code that evaluates the expression before the target method is executed:

var OLD_var0 = exec(() -> fuzzobj.size());

The occurrence of \old(fuzzobj.size()) in the assertion is then replaced by OLD_var0. Nested \old expressions are handled recursively, so that all required pre-state values are saved before any mutation performed by the target method.

11.0.0.4 Handling quantified assertions

The simplified assertion language supports integer universal quantification of the form:

\forall int i; condition; specification

The implementation extracts the quantified variable, the range condition, and the quantified body. It then infers loop bounds from simple inequalities in the condition. For example, a condition such as 0 <= i && i < oldSize is converted into a loop over the corresponding integer range. The quantified formula is translated into a Boolean accumulator:

Boolean forall_holds = Boolean.TRUE.equals(exec(() -> {
  boolean ret = true;
  for (int i = lo; i <= hi; i++) {
    if (condition) {
      ret &= Boolean.TRUE.equals(exec(() -> specification));
    }
  }
  return ret;
}));

The original \forall expression is then replaced by the generated Boolean variable. If the quantified body contains \old expressions that depend on the quantified variable, the implementation snapshots the corresponding pre-state values into an array before the method call and retrieves them during the loop.

11.0.0.5 Splitting compound formulas

To make assertion evaluation robust and to localize failures, compound formulas are split into intermediate expressions. The implementation recursively decomposes formulas at top-level logical operators, including implication, disjunction, conjunction, and equality. Implication A => B is translated into !A || B. Equality between non-null expressions is translated using Objects.equals, while equality against null is translated using Java reference equality. Each intermediate expression is evaluated through exec, which catches runtime exceptions and converts them to null. Boolean subformulas are then normalized with Boolean.TRUE.equals(...) so that exceptions and non-true results are treated as failures.

11.0.0.6 Composing the target-method call

After all pre-state values have been copied, the test harness executes the target method. Void methods are invoked through a Runnable wrapper:

String exceptionType =
  func_call_runnable(() -> fuzzobj.add(index, element));

Methods with return values are invoked through a Supplier wrapper, which stores both the return value and any thrown exception:

var paired_ret =
  func_call_supplier(() -> fuzzobj.method(args));
var New_Ret = paired_ret.first;
String exceptionType = paired_ret.second;

Constructors are handled similarly, except that the constructed object is stored as the post-state receiver. This uniform wrapping lets the generated test distinguish exceptions raised by the target method from exceptions raised while evaluating the generated assertion.

11.0.0.7 Checking the postcondition

After the target method has executed, the generated code evaluates the translated assertion formula. The normal postcondition is checked as follows:

Boolean normalpost = exec(() -> translatedFormula);
if (normalpost == null || !normalpost) {
  throw new RuntimeException("Normal Postcondition Violated");
}

Thus, a candidate fails if the assertion evaluates to false or if evaluating the assertion raises an exception. The latter is important because many incorrect generated assertions are syntactically plausible but unsafe, for example by calling equals on a value that may be null. Exceptional postconditions are currently represented by a default true condition unless the checker is configured with additional exception-specific constraints.

Figure 4 shows a simplified fuzz test generated from the example in Section 2. The test first saves the pre-state value needed by the assertion, namely list.size(), to implement \old(this.size()). It then executes the target method, list.add(index, element), on inputs generated by the test generator. After the method call, the candidate assertion is evaluated in two parts: the precondition checks whether index is within the valid insertion range in the pre-state, and the postcondition checks whether list.get(index).equals(element) holds. The implication is encoded as !pre || post. If this expression evaluates to false, or if evaluating it raises an exception and therefore returns null, the test throws a runtime exception, causing the generated input to be reported as a counterexample. The helper function exec safely evaluates expressions that may throw exceptions during assertion checking. Similarly, funcCall executes the target method while recording whether the method itself throws an exception. In this way, the fuzz test distinguishes exceptions caused by the program under test from exceptions caused by an invalid or unsafe generated assertion.

11.0.0.8 Helper functions

The generated harness includes a small set of helper functions to make assertion evaluation robust. We describe them below.

Pair. For target methods with return values, the harness needs to record both the returned value and whether the method itself throws an exception. We use a lightweight Pair container for this purpose.

private static class Pair<A, B> {
  private final A first;
  private final B second;

  private Pair(A first, B second) {
    this.first = first;
    this.second = second;
  }
}

Safe expression evaluation. Generated assertions may be unsafe even when they are syntactically valid; for example, they may call equals on a null value. The exec helper evaluates an assertion subexpression and converts any runtime exception into null. The checker then treats null as a failed assertion evaluation.

private static <T> T exec(Supplier<T> supplier) {
  try {
    return supplier.get();
  } catch (Exception fuzzexception) {
    return null;
  }
}

Method execution. The harness separates execution of the target method from evaluation of the generated assertion. For target methods with return values, func_call_supplier stores both the returned value and any exception tag. For void methods, func_call_runnable records only whether the method throws. This separation allows the checker to distinguish exceptions raised by the program under test from exceptions raised later during assertion evaluation.

private static <T> Pair<T, String> func_call_supplier(Supplier<T> supplier) {
  try {
    return new Pair<>(supplier.get(), null);
  } catch (Exception fuzzexception) {
    String exceptionType = fuzzexception.getClass().getSimpleName();
    return new Pair<>(null, exceptionType);
  }
}

private static String func_call_runnable(Runnable runnable) {
  try {
    runnable.run();
    return null;
  } catch (Exception fuzzexception) {
    return fuzzexception.getClass().getSimpleName();
  }
}

Retrieving saved pre-state values. For quantified assertions, a \old expression may depend on the quantified variable. In such cases, the harness snapshots the relevant pre-state values into an array before executing the target method. During assertion evaluation, get_from_array retrieves the saved value at the current quantified index and casts it back to the expected target type.

@SuppressWarnings("unchecked")
private static <T> T get_from_array(Object arr, int index, T ex_val) {
  try {
    return (T) Array.get(arr, index);
  } catch (Exception fuzzexception) {
    return null;
  }
}

11.0.0.9 Compilation and fuzzing

The composed test harness is written into a temporary fuzztests.FuzzTest class and compiled together with the target class and required third-party libraries. The compile check succeeds only if this generated harness compiles. The fuzz check then invokes Randoop on the generated FuzzTest class. If Randoop reports no error-revealing tests, the candidate passes the fuzz check; otherwise, the candidate is marked invalid. This design allows the same generated harness to serve both as a compilation oracle and as an executable semantic check for generated assertions.

11.0.0.10 Equivalence-Check Harness

The equivalence check reuses the same executable-harness infrastructure described above, but changes what is executed and what property is checked. The fuzz and validity checks are context-dependent: they execute the target method on generated inputs and then evaluate one candidate assertion against the resulting program state. In contrast, the equivalence check is context-independent. It does not call the target method and does not depend on whether a particular receiver object satisfies the original method semantics. Instead, it compares two assertion formulas directly over the same generated valuation of their free variables.

Concretely, given two formulas \(A\) and \(B\), the generated equivalence harness evaluates both formulas under the same generated inputs and checks whether they always agree:

Boolean left = exec(() -> translatedFormulaA);
Boolean right = exec(() -> translatedFormulaB);

Boolean equiv = exec(() -> Objects.equals(left, right));

if (equiv == null || !equiv) {
  throw new RuntimeException("Equivalence Violated");
}

Thus, Randoop is used to search for a valuation that distinguishes the two formulas. The main difference from the fuzz-check harness is therefore the absence of the target-method call. There is no pre-state/post-state transition to execute, and no candidate is checked against the implementation behavior of a method. Instead, both formulas are translated into executable Java expressions and evaluated side by side. This makes the equivalence check a formula-level test: it asks whether two candidate assertions describe the same condition over the generated inputs, independent of the method body or the correctness of the implementation.

12 Experimental Setup↩︎

Our main experiments use two open-source backbone models: Qwen2.5-Coder-32B-Instruct [47], a smaller code-specialized model, and GPT-oss-120B [48], a larger instruction-tuned model. For each natural-language specification, we sample five candidates with a moderately high temperature \(0.6\) to encourage output diversity, and set the maximum generation length large enough (\(65536\)) to avoid truncating formal assertions. The experiments are run on a local server with two NVIDIA L40S GPUs.

13 Detailed Explanation and Visualization for Different Conformance Implementation↩︎

This appendix describes the conformance-checking variants evaluated in Section 6. Each method takes as input the original natural-language specification and a generated formal assertion, and returns a conformance score estimating whether the generated assertion preserves the intended meaning of the specification. The variants differ in whether they use roundtrip translation, whether they decompose the specification into components, whether the comparison is bidirectional, and whether they include contextual examples.

13.0.0.1 Direct

The Direct baseline does not use roundtrip translation. It directly asks the LLM whether the generated formal assertion is equivalent to the original natural-language specification. To make the formal assertion interpretable, the prompt first describes our JML-like assertion syntax, including implication, quantification, \old, \result, and receiver references such as this. It also provides the scoring rule used by the checker and the relevant code context, so that the model can interpret the formula with respect to the target method. The model then receives the natural-language intent and the candidate assertion, and predicts whether they describe the same behavior. Because the model must reason directly over the formal logic formula, this method depends heavily on the LLM’s ability to understand the assertion syntax and map it to the intended semantics.

13.0.0.2 Simple

Simple is a roundtrip-based baseline. It first asks the LLM to translate the generated formal assertion back into natural language. It then asks whether this generated natural-language description is equivalent to the original natural-language specification. This reduces the comparison to a simple natural-language equivalence judgment, but it does not explicitly ask to compare bidirectionally, or decompose the specification into smaller semantic parts.

13.0.0.3 Bi-NLI

Bi-NLI uses roundtrip translation, but frames the comparison as a bidirectional natural-language inference task. After translating the formal assertion back into natural language, the checker asks whether the original specification entails the roundtripped description and whether the roundtripped description entails the original specification. Unlike our full method, this variant does not provide additional code context, examples, or component-level alignment guidance during the equivalence judgment. The candidate is considered conforming only when both entailment directions hold. This formulation makes equivalence explicit, but can be sensitive to conservative entailment judgments and score calibration.

13.0.0.4 Ours-noCtx

Ours-noCtx is a clausal-level roundtrip method without additional context. It decomposes the original specification and the roundtripped description into semantic clauses, then checks whether the clauses align bidirectionally. This lets the checker compare finer-grained pieces of meaning rather than making a single global equivalence judgment. However, because this variant omits contextual examples and surrounding task information, the model has less guidance for interpreting edge cases or domain-specific intent.

13.0.0.5 Ours

Ours is our full conformance implementation. LikeOurs-noCtx, it uses roundtrip translation and bidirectional clause-level alignment. In addition, it provides contextual information, including the target code context and examples of how specifications should be interpreted. This helps the LLM resolve ambiguous terms, align clauses more consistently, and avoid judging candidates only by surface-level textual similarity. This is the method used in the main pipeline unless otherwise stated.

Visualization↩︎

Figure 5 compares the overall ROC curves of all conformance implementations after pooling candidates from all datasets. The curve for Ours dominates the alternatives in aggregate, showing that the contextual bidirectional clausal checker provides the strongest ranking signal for distinguishing equivalent from non-equivalent candidates. Figure 6 breaks the same comparison down by dataset. The per-dataset curves show that no single baseline is uniformly best across all settings, but Ours is the most stable overall and obtains the highest aggregate AUC.

References↩︎