Clover: Closed-Loop Verifiable Code Generation

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number in Tables 1, 2, 4, 5, 6, 7, 8, the Algorithm 1 steps, the template lemmas, page and section references, the quotations, the prompts and the Verus sketch; corrected the soft-evidence quotation (it is about data contamination, not the C2 result), the threat paragraph that said formal equivalence rejected every weakened contract (60/60 in C2 only, 44/60 and 30/60 in C3), the Table 5 page reference, the one-change claim for Verus, the feedback claim (generation experiment, not a Clover edge), the missing termination caveat on the Verus proof-instead-of-tests idea, and seven unmarked inferences.

source: Sun, Sheng, Padon, Barrett (Stanford, VMware Research); arXiv:2310.17807v4 (16 Nov 2024), 59 pages: 18 of body, references, Appendix A.1 to A.10 on pp.26-59. Page numbers below are PDF pages. Where the body cites [61, Appendix …] it means the appendix of this same arXiv version.

the problem Clover attacks

A verifier proves that code meets its annotations. It says nothing about whether the annotations say what the user asked for, and a weak postcondition verifies as happily as a full one. Clover is a filter for that gap. It takes three artifacts for one function, the code, the formal annotations (pre- and postconditions) and a natural-language docstring, and accepts the triple only if six pairwise checks pass. One check is ordinary verification. The other five regenerate one artifact from another with an LLM and test whether the regenerated artifact is equivalent to the original.

proved, measured, trusted

Proved by a tool: that the code satisfies the annotations (Dafny), and, inside the doc2anno check, that two sets of annotations are logically equivalent (Dafny again).

Proved on paper: Theorem 3 (Appendix A.1, p.27-28), a bound on the accept probability of one reconstruction edge under two assumptions about the LLM. It is not a guarantee about the implementation; the authors write that “the combined use of GPT-4 and Dafny may not satisfy our assumptions” and that the parameter u “could be non-negligible” (p.28).

Measured: acceptance of 60 hand-written correct Dafny triples and rejection of 240 hand-mutated incorrect ones (CloverBench), the same on 33 programs of MBPP-DFY-50, acceptance of 41 correct Verus triples, and a small generation study.

Trusted: GPT-4 as the regenerator and as the judge of docstring equivalence; five input/output tests per program as the judge of code equivalence; Dafny and Z3; and the docstring itself as the statement of intent. The input assumption is strict: “Additionally, we expect that each of the three components provides sufficient detail to unambiguously determine a unique result of running the code on any given input.” (Section 3.2, p.5)

technique 1: the six-edge consistency check

What it is. A triangle with code, annotations and docstring at the corners and a directed check on each of the six edges. “For an input instance to pass the verification phase, it must pass all six tests.” (Section 3.2, p.6)

When to use it. Inference: as an acceptance filter after any generator has produced code with a specification, when no human will read the specification. The paper says the second phase is “completely agnostic to the process used in the first phase” (Section 1, p.3).

Steps, from Algorithm 1 (p.7) and Section 3.3 (p.8-10). The number of tries with compiler feedback is m = 3.

1. anno-sound. Run Dafny on the annotated code. Fail means reject.
2. anno-complete. Give the LLM the function signature with an anonymized name and the annotations only (Listing 1.5, p.8, uses the name foo and a // TOFILL body). Ask for code, up to 3 tries with Dafny feedback. Reject if the new code is not equivalent to the original code.
3. doc2code. Give the LLM the docstring and signature only, ask for code, up to 3 tries with feedback from the compiler and not from the verifier. Reject if not equivalent to the original code.
4. code2doc. Ask the LLM for a docstring from the code, 3 times. Reject if none is judged equivalent to the original docstring.
5. doc2anno. Give the LLM the docstring and signature, ask for annotations, compile them against an empty body and feed compiler errors back up to 3 times. Reject if the new annotations are not proved equivalent to the original ones.
6. anno2doc. Ask the LLM for a docstring from the annotations, 3 times. Reject if none is judged equivalent.
7. Accept.

Three details the checks depend on:

• What counts as annotation. Only pre- and postconditions. Loop invariants and assertions are treated as part of the code (Section 4.3, p.12), because they mean nothing without the code they sit in.
• code2doc must see the precondition. “The only difference is that in order to ensure the code provides all the information needed for the docstring generation, we embed the preconditions into the code in the form of assert statements.” (Section 3.3, p.10)
• The whole check can be repeated k times per edge, and an edge passes if any repetition passes (Section 4.3, p.13). The paper reports k = 1 and k = 10.

Why the completeness edge exists: “To prevent annotations that are too trivial from being accepted, we test whether the annotations are strong enough by testing if they contain enough information to reconstruct functionally equivalent code.” (Section 3.2, p.6)

Verus form. The paper itself ran this: 41 of the examples were rewritten in Verus and the same checks were used with Verus as the formal tool (Section 4.6, p.16). The one further change it reports: “Also, because the Verus specification format is very new, we started each LLM prompt with a few simple examples of Verus specification syntax.” Inference on the mapping: annotations are the requires and ensures clauses of an executable function; loop invariant and decreases clauses, assert statements and proof blocks belong to the code side; anno-sound is a Verus run on the function. Inference: for code2doc the precondition can be shown as an assert at the top of the body as in the paper, or the requires clause can simply be left on the signature, since it is part of the function’s text in Rust.

Evidence, CloverBench ground truth, GPT-4, Dafny 4.0.0 (Table 1, p.13, and Table 2, p.14):

• whole check: 45/60 (75%) accepted at k = 1, 52/60 (87%) at k = 10
• anno-sound 60/60 at both k
• anno-complete 53/60 (88%), then 57/60 (95%)
• doc2anno 51/60 (85%), then 53/60 (88%)
• anno2doc 60/60 at both k
• code2doc 58/60 (97%), then 60/60
• doc2code 49/60 (82%), then 56/60 (93%)

Evidence, adversarial variants (Table 1, p.13): 0/60 accepted in each of the four categories C1, C2, C3 and C6, at k = 1 and at k = 10, so 0 of 240.

Evidence, Verus ground truth (the sentence is in Section 4.6, p.16; per-edge counts in Table 5, p.17): “For our 41 examples, Clover accepts 32 of 41 when k = 1 and 36 out of 41 when k = 10.” Per edge at k = 1 then k = 10: anno-complete 39/41 then 40/41; doc2anno 33/41 then 36/41; anno-sound, anno2doc, code2doc and doc2code 41/41 at both. Inference: no adversarial variants were built for Verus, so the paper has no false-positive measurement for Verus at all.

Evidence with an open model (Table 7, p.32, CodeLlama-34b, ground truth): anno-sound 60/60, anno-complete 6/60, code2doc 8/60, doc2code 2/60, anno2doc 48/60, doc2anno 2/60, all six edges 2/60.

Where it fails or what it assumes.

• Scope: one method, no helper functions or predicates (footnote 7, p.11). On MBPP-DFY-50 this excluded 15 of 50 programs, and 2 more for imprecise docstrings: “First, 17 of the 50 samples are out of scope for Clover.” (Section 4.4, p.15)
• Shared blind spots pass: “As another example, if the docstring, annotations, and code all miss the same edge case, the error cannot be detected.” (Appendix A.4.1, p.30)
• It filters and does not repair: “Clearly, the verification phase cannot compensate for poor generation, it can only detect and flag such examples.” (Appendix A.4.3, p.31)
• Annotations specify function, not algorithm or performance (Appendix A.4.1, p.30).
• Most ground-truth rejections come from GPT-4 writing invalid Dafny 4 syntax, such as leaving out the reads or modifies clause on first try (Section 4.3, p.14, and Appendix A.4.5, p.31).

technique 2: annotation equivalence as two lemmas

What it is. The only formal equivalence check in Clover, and the edge that carries most of the rejection. Original and regenerated annotations are wrapped in predicates, and Dafny is asked to prove that the preconditions are equivalent and that, under them, the postconditions are equivalent.

Steps, from Section 4.1 (p.11) and Appendix A.7 (p.32-34). The template for maxArray (Listing 1.14) has this shape:

predicate pre_original(a: array<int>, m: int) reads a { (a.Length >= 1) }
predicate pre_gen(a: array<int>, m: int) reads a { true // generated preconditions go here
}
lemma pre_eq(a: array<int>, m: int)
  ensures pre_original(a, m) <==> pre_gen(a, m)
{ }
predicate post_original(a: array<int>, m: int)
  requires pre_original(a, m) reads a
{ (forall k :: 0 <= k < a.Length ==> m >= a[k]) && (exists k :: 0 <= k < a.Length && m == a[k]) }
predicate post_gen(a: array<int>, m: int)
  requires pre_original(a, m) reads a
{ true // generated postconditions go here
}
lemma post_eq(a: array<int>, m: int)
  requires pre_original(a, m)
  requires pre_gen(a, m)
  ensures post_original(a, m) <==> post_gen(a, m)
{ }

1. Generate the template for each benchmark by script, with the parameters and return values of the method as the predicate parameters.
2. Paste the regenerated requires clauses into pre_gen and the regenerated ensures clauses into post_gen.
3. Run the verifier. Both lemmas have empty bodies; the check passes only if both verify.

Its guarantee: “This method is sound in the sense that it succeeds only if the two sets of annotations are indeed equivalent.” (Section 3.2, p.8) Its gap: “Note that the template is sound but not complete, that is, there could be cases when two predicates are indeed equivalent but Dafny cannot prove it.” (Appendix A.7, p.33) The paper’s failing case is only_once (Listing 1.15, p.34-35): one postcondition counts occurrences with multiset(a[..])[key] == 1, the other says there exists an index holding the key and no later index holds it; they describe the same property and the empty lemma does not prove them equal.

Verus form. Inference, a sketch that has not been compiled:

spec fn pre_original(a: Seq<int>) -> bool { a.len() >= 1 }
spec fn pre_gen(a: Seq<int>) -> bool { true /* regenerated requires */ }
proof fn pre_eq(a: Seq<int>)
    ensures pre_original(a) == pre_gen(a)
{ }
spec fn post_original(a: Seq<int>, m: int) -> bool {
    (forall|k: int| 0 <= k < a.len() ==> m >= a[k])
    && (exists|k: int| 0 <= k < a.len() && m == a[k])
}
spec fn post_gen(a: Seq<int>, m: int) -> bool { true /* regenerated ensures */ }
proof fn post_eq(a: Seq<int>, m: int)
    requires pre_original(a), pre_gen(a)
    ensures post_original(a, m) == post_gen(a, m)
{ }

Inference on what changes. The contract of an executable Verus function speaks about Rust values, so each parameter has to be lifted to its specification view (a Vec to a Seq) before it can be a spec fn parameter. A function that takes &mut needs two parameters per mutated argument in post_gen, one for the old value and one for the final value. Dafny’s reads clause has no counterpart to write. Dafny lets the postcondition predicates carry requires pre_original; a spec fn is total, so the precondition goes on the proof fn only, as above. What does not change is the incompleteness: quantified equivalences such as the only_once pair need hand-written proof, and with an empty body the check will reject them.

Evidence. doc2anno rejects 60/60 in C2 and 60/60 in C6 at both k, 57/60 then 54/60 in C1, and 44/60 then 30/60 in C3 (Table 4, p.16). The paper’s reading: “This is because we use Dafny to do a formal equivalence check, which guarantees that only logically equivalent annotations are accepted.” (Section 4.5, p.16) The cost shows on correct inputs: doc2anno is the lowest or second-lowest edge for ground truth in both Dafny (51/60) and Verus (33/41).

technique 3: code equivalence by a fixed set of input/output tests

Steps, from Section 4.1 (p.11) and Appendix A.8 (p.35-36):

1. For each benchmark write a test method that calls the function on five concrete inputs and prints each result (Listing 1.16 runs maxArray on five arrays, among them all negatives, all zeros and a single element).
2. Run it with the original body and record the output.
3. Swap in the regenerated body, run again, and compare the printed output.

The rule: “If the generated code has the same output as the original code for all five tests, then the code is considered to be equivalent” (Section 4.1, p.11). The paper calls the test imprecise and names concolic testing and formal equivalence checking as stronger options (Section 3.2, p.8).

When to use it. Inference: when the function is deterministic and the specification fixes a unique output, which is Clover’s input assumption anyway.

Verus form. Inference: executable Verus functions compile as ordinary Rust, so the five calls become a Rust test that prints or compares results, with no verifier involved. Inference: for the anno-complete edge there is a stronger option that the paper does not use. If the annotations determine a unique output, then any regenerated body that verifies against them is equivalent to the original on every input that satisfies the precondition, so running the verifier on the regenerated body would replace the five tests with a proof. Caveat, also inference: Verus does not require an executable function to terminate (see verus_linear), so a non-terminating regenerated body could pass, and a termination argument or a test would still be needed.

Where it fails. Five inputs chosen by the benchmark author. Evidence that the edge is weak on its own: in category C2, where only the annotations were weakened, anno-complete rejects 26/60 at k = 1 and 16/60 at k = 10 (Table 4, p.16). So for 44 of 60 weakened specifications, GPT-4 given ten chances still produced code that matched the original on the tests. The authors offer this as soft evidence of indirect data contamination, not as an explanation of the C2 result (Appendix A.4.4, p.31): “Some soft evidence for this is the observation that GPT-4 can sometimes generate the correct code even with incomplete docstrings or annotations.” (Appendix A.4.4, p.31)

technique 4: docstring equivalence by a memoryless LLM judge

Steps, from Section 3.3 (p.10) and the prompt list (p.37):

1. Generate three candidate docstrings independently in one session.
2. For each candidate, open a fresh call that has no access to the generation call and ask whether the two docstrings describe the same functional behaviour, answer yes or no.
3. Pass if any candidate is judged equivalent.

The separation is deliberate: “Note that the two calls to GPT-4 are independent to ensure that the second call contains no memory of the first call.” (Section 3.3, p.10) The judge’s system prompt reads: “Determine if two docstrings describe the exact same functional behavior of a dafny program. Make sure all details are exactly the same.” (p.37)

Verus form. Nothing here depends on the verifier; it carries over unchanged.

Evidence that it is the weakest part. On ground truth anno2doc accepts 60/60, which the authors do not take as good news: “As long as they do not directly contradict each other, information omissions or additions in docstrings frequently go unnoticed by GPT-4.” (Section 4.3, p.14) On adversarial input, anno2doc at k = 10 rejects only 13/60 in C2 and 4/60 in C3 (Table 4, p.16). Appendix A.2 (p.29) says the checker is good at detecting contradictory information but not added or omitted information.

technique 5: prompts that push toward the canonical specification

What it is. The reconstruction prompts are short and zero-shot, and they contain instructions that make two independent generations more likely to land on equivalent annotations. From the prompt list (p.37):

• doc2anno asks for the extreme specification: “Generate the weakest preconditions and strongest postconditions for the dafny programs based on the docstring.”
• doc2anno and code2anno forbid noise clauses (a requires true, a null check, a non-negativity requirement on naturals) and forbid assuming non-empty arrays or non-negative integers unless necessary.
• doc2anno forbids self-defined functions and int.MaxValue or int.MinValue.
• anno2code forbids helper functions and changes to the signature and annotations.
• code2doc says to leave out implementation details and to read assert as a precondition.
• function names are replaced: “To mitigate this potential bias in our experiments, we opted to replace the function names with generic, non-descriptive identifiers.” (Appendix A.4.4, p.31)

When to use it. Inference: whenever two specifications written separately must be compared formally: asking both writers for the weakest precondition and strongest postcondition removes most of the freedom that would make an equivalence proof fail.

Verus form. Inference: the same instructions apply, with the Verus list of noise clauses, for example a requires that only restates a type bound. The ban on self-defined functions is what keeps the template of technique 2 closed; a Verus specification that needs a helper spec fn falls outside what Clover supports.

Evidence. Dafny feedback matters in the generation experiments: annotation generation from code (not a Clover edge; it includes loop invariants) succeeds on 28 of 60 programs in one try and 41 of 60 with three tries and maximal feedback from Dafny (Section 4.2, p.12, Fig. 2b). For doc2anno the paper says the feedback mechanism is quite important (Section 3.3, p.9). The paper has no ablation of the individual prompt instructions.

technique 6: adversarial variants that still verify

What it is. A way to test a specification filter. For each correct triple, build wrong triples that the verifier alone would accept.

Steps, from Section 4.5 and Table 3 (p.14-15):

1. Enumerate which of the three artifacts are mutated: seven non-empty subsets, C1 to C7.
2. C1: mutate the docstring only (strengthen or weaken it).
3. C2: weaken the annotations only, so that the unchanged code still verifies.
4. C3: weaken annotations and docstring together so that they agree with each other.
5. C6: change code and annotations together so that the code still satisfies the annotations, while the docstring keeps the original meaning.
6. Drop C4 and C5 (code changed, annotations not) because they fail verification, and C7 (all three changed).
7. Write each variant by hand; 4 variants for each of 60 programs.

Why it is the right test: “Thus, for these examples, a naive approach using only Dafny (as in [44]) would result in a 100% false positive rate.” (Section 4.5, p.15)

Verus form. Inference: carries over directly, and C2 is the cheapest to automate for Verus: delete one ensures clause, or replace an equality by an inequality, and keep the variant if Verus still verifies the function.

Evidence per edge, rejections at k = 10 (Table 4, p.16):

• C1: anno-complete 3/60, doc2anno 54/60, anno2doc 34/60, code2doc 54/60, doc2code 37/60
• C2: anno-complete 16/60, doc2anno 60/60, anno2doc 13/60, code2doc 0/60, doc2code 4/60
• C3: anno-complete 21/60, doc2anno 30/60, anno2doc 4/60, code2doc 43/60, doc2code 18/60
• C6: anno-complete 27/60, doc2anno 60/60, anno2doc 27/60, code2doc 40/60, doc2code 55/60

Inference from these rows: no single edge rejects everything in C1 or C3, so the 0 of 240 result needs the conjunction. In C2 and C6 the formal doc2anno edge alone is sufficient. In C3 the best single edge is the LLM-judged code2doc at 43/60.

Limits. The variants are written by the same authors who designed the checks, on textbook programs. Footnote 13 (p.29) notes they were built to be hard to reject. Inference: zero accepted out of 240 hand-made cases bounds the false-positive rate only loosely, and only for this kind of mutation.

technique 7: generate many candidates and let the filter choose

Steps, from Section 4.2 (p.12): ask GPT-4 for code and annotations from the docstring alone, 20 independent times per problem; run the Clover check on each; keep any that pass.

Evidence (Fig. 2c and text, p.12-13; Table 8, p.44): the first try is correct for 24 of 60 problems; at least one of 20 tries is correct for 41 of 60; Clover accepts at least one correct candidate for 39 of those 41 and accepts no incorrect candidate. “Thus, we can fully automatically generate 39 of 60 programs from natural language alone, with the guarantee that the generated programs pass all Clover consistency checks.” (Section 4.2, p.12) Correctness of the candidates was judged by hand.

Other generation numbers from the same section: code from annotations, at best 53 of 60 with three tries and feedback from Dafny; annotations with loop invariants from code, 28 of 60 in one try and 41 of 60 with three tries and feedback.

Verus form. Inference: unchanged in structure. The cost is 20 generations times six edges, several of which make up to three LLM calls plus verifier runs; the paper reports no cost or time.

technique 8: the single-edge acceptance model

What it is. A way to reason about when a reconstruction test is trustworthy (Appendix A.1, p.26-28). Each domain has an equivalence relation. The LLM is a transfer model M(x, ·), a distribution over outputs for input x; f(x) is the equivalence class it most often produces. Two assumptions: alignment (for a consistent pair the most likely class is the right one with probability c1 near 1, and for an inconsistent pair it is the given one with probability c0 near 0) and concentration (with probability at least pc, the most likely class has mass at least l and every other class at most u). Then a consistent pair is accepted with probability at least l · pc · c1, and an inconsistent pair with probability at most u · pc · (1 − c0) + (1 − pc)(1 − c0) + c0.

How to use it. Inference: measure each edge’s accept rate on known-correct and known-wrong pairs, as Table 6 (p.28) does at k = 1, and look for edges where the wrong-pair accept rate is not small (inference: there the model’s most likely output does not separate right from wrong). Table 6 gives accept rates on wrong pairs of 0.30 (C1), 0.4 (C2) and 0.30 (C6) for anno2doc, and 0.48 (C3) for doc2code.

The edges are not independent, and the paper does not multiply them: “We do not attempt to theoretically analyze the full check, because we do not assume the edges to be independent (so multiplying acceptance probabilities is not necessarily meaningful).” (Appendix A.1, p.28) The measured whole-check acceptance on ground truth is 0.75 against a product of 0.59 (Appendix A.2, p.29).

Verus form. Not language-specific.

Limits. The analysis assumes a perfect equivalence checker (footnote 12, p.27). Repeating the test k times raises acceptance of correct pairs and, inference, by the same mechanism, of wrong pairs: every rejection count in Table 4 is lower or equal at k = 10.

numbers that do not add up

• Table 4 (p.16) prints anno2doc at k = 1 as 24/60 (60%) in both C2 and C3. 24/60 is 40%. Table 6 (p.28) gives an accept rate of 0.4 for anno2doc in C2, which fits 36 rejections (60%), so the count 24 is probably the number accepted.
• Section 4.4 (p.15) says that of the 6 incorrect MBPP-DFY-50 programs, 5 have contradictions between docstring and preconditions and 1 has trivial postconditions. Appendix A.9 (p.38-43) describes four precondition contradictions (tasks 472, 567, 632, 644) and two weak postconditions (task 576, whose annotations do not state the false case, and task 803, whose postcondition is a tautology).
• Section 4.5 (p.16) says doc2anno has the highest rejection rate. In C3 code2doc is higher at both k (51/60 against 44/60, and 43/60 against 30/60).
• The abstract’s “up to 87%” is the k = 10 figure; at k = 1 it is 75%.
• The MBPP-DFY-50 figure of 89% is 24 accepted of the 27 programs judged correct after inspection, out of 33 in scope and 50 in the dataset (Section 4.4, p.15).
• The ground-truth code2doc edge accepts 58/60 at k = 1 (Table 2), while in C2, where code and docstring are the same ground-truth pair, it rejects 0/60 (Table 4). Inference: this is run-to-run variation of the LLM judge, and it is the size of the noise in every LLM-judged cell.

already done, which VL should not redo

Inference, the study’s judgment of what the paper covers:

• The idea and a working prototype of round-trip specification checking over code, formal contract and prose, including a first Verus run.
• The equivalence-lemma template for comparing two contracts.
• The taxonomy of verifier-passing wrong triples (C1 to C7).
• The observation that an LLM judge of prose equivalence misses omissions and additions.
• Inference: left open by the paper: functions with helpers and predicates, specifications that do not fix a unique output, stateful or multi-function code, any cost accounting, a false-positive measurement in Verus, mutations produced by a generator instead of by the authors, and a completeness edge that uses a proof instead of five tests.

threat to VeruLaw

Inference: as a product, low. Clover is a research prototype for single textbook functions and the authors say additional breakthroughs or human-in-the-loop steps may be needed. As prior art, high: it is the reference for the claim that agent-written verified code needs a check that the specification matches intent, it already names Verus, and anyone proposing round-trip or consistency checking of specifications will be compared with it. The practical lesson for VL is which part did the work. In C2, where only the annotations are weakened, the formal equivalence of regenerated contracts (doc2anno) rejected 60/60 at both k, while no other edge rejected more than 16/60 at k = 10; in C3, where the docstring is weakened with the annotations, doc2anno rejected only 44/60 and 30/60 (Table 4, p.16).

techniques for the catalog

• six-edge consistency check: accept a code, contract and docstring triple only if verification passes and each artifact can be regenerated from each other one up to equivalence.
• annotation completeness by reconstruction: regenerate code from the contract alone under an anonymized name and reject the contract if the result differs from the original code.
• contract equivalence lemmas: wrap original and regenerated pre- and postconditions in predicates and have the verifier prove two empty-bodied equivalence lemmas.
• preconditions as asserts for code2doc: put the precondition into the code text before asking for a description, so the description can mention it.
• five-test code equivalence: compare printed outputs of original and regenerated code on a fixed set of inputs.
• memoryless docstring judge: decide prose equivalence in a fresh LLM call that cannot see how the candidate was generated.
• weakest-pre strongest-post prompting: ask for the extreme contract and ban noise clauses so that separately written contracts can be proved equal.
• function name anonymization: replace descriptive names with generic ones so reconstruction cannot rely on the name.
• compile-only feedback loop: when regenerating from prose, feed back compiler errors but not verifier errors, so the result depends on the prose alone.
• verifier-passing adversarial variants: build wrong triples by weakening the contract, changing the docstring, or changing code and contract together while verification still passes.
• any-of-k edge repetition: repeat each stochastic check k times and pass if any repetition passes, trading false rejections for false acceptances.
• sample-then-filter generation: draw many candidate solutions and keep those the consistency check accepts.
• single-edge acceptance model: bound an edge’s accept probability from the alignment and concentration of the regenerating model, and measure both rates on known pairs.

Last edited: 2026-10-13