CLEVER: A Curated Benchmark for Formally Verified Code Generation

May combine two claims.

Passing example-based test cases provides some evidence of functional correctness but offers only partial coverage and cannot guarantee semantic soundness.

“While passing these tests provides some evidence of functional correctness[25], we deliberately exclude them from our core success metric-since test cases offer only partial coverage and cannot guarantee semantic soundness (see Section 2 for discussion).”

• cites [25] [25] Liu, J., Xia, C. S., Wang, Y ., and Zhang, L. Is your code generated by chatGPT really correct? rigorous evaluation of large language models for code generation. In Thirty-seventh Conference on Neural Information Processing Systems , 2023. URL https://openreview.net/forum? id=1qvx610Cu7 . - sourceSupported

May combine two claims.

The hybrid using KiminaProver-7b with GPT-5-mini yielded the highest compilation rates (90.1% spec, 84.5% impl) but certified almost nothing (0 spec, 1 impl), as the pipeline was bottlenecked by parsing issues.

“This hybrid (Table 1) yielded the highest compilation rates (90.1% spec, 84.5% impl), highlighting GPT-5-mini 's fluency. However, it certified almost nothing (0 spec, 1 impl), as the pipeline was bottlenecked by these same parsing issues.”

• cites [33] [33] Wang, H., Unsal, M., Lin, X., Baksys, M., Liu, J., Santos, M. D., Sung, F., Vinyes, M., Ying, Z., Zhu, Z., et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354 , 2025. - sourcePartly supported

  The paper’s Table 1 identifies a 7B Kimina-Prover model, supporting the identification of a component of the hybrid. It reports miniF2F proof-solving results, not a GPT-5-mini hybrid, the stated compilation and certification counts, or parsing issues as a bottleneck. The searches for those terms found no supporting passage. (LLM, conf=0.83)

  Experimental — accuracy not yet measured

Probably not a substantial claim: may not pass S3 (load-bearing).

DafnyBench is a benchmark of 782 stand-alone Dafny programs collected from prior benchmarks and Dafny repositories, where the synthesis task is to generate the verification conditions that allow Dafny to prove correctness.

“DafnyBench [27] is a benchmark of 782 stand-alone Dafny programs collected from prior benchmarks and Dafny repositories, where the synthesis task is to generate the verification conditions that allow Dafny to prove correctness.”

• cites [27] [27] Loughridge, C., Sun, Q., Ahrenbach, S., Cassano, F., Sun, C., Sheng, Y., Mudide, A., Misu, M. R. H., Amin, N., and Tegmark, M. Dafnybench: A benchmark for formal software verification, 2024. URL https://arxiv.org/abs/2406.08467 . - sourcePartly supported

  Section 3.1 reports 782 stand-alone Dafny programs sourced from GitHub and the Clover and dafny-synthesis benchmarks. It describes the task as filling in removed verification hints—assert and invariant statements—so Dafny can verify the programs, not generating verification conditions. (LLM, conf=0.87)

  Experimental — accuracy not yet measured

May combine two claims.

GPT-5-mini with Kimina FS achieves 90.062% spec compiled, 0% spec proved, 84.472% impl compiled, 0.621% impl proved, and 0% end-to-end.

“GPT-5-mini | FS | Kimina FS | FS | Kimina FS | 90.062% | 0% | 84.472% | 0.621% | 0%”

• cites [33] [33] Wang, H., Unsal, M., Lin, X., Baksys, M., Liu, J., Santos, M. D., Sung, F., Vinyes, M., Ying, Z., Zhu, Z., et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354 , 2025. - sourceCould not verify

  Tables 1 and 2 (page unavailable in our copy) report miniF2F results for Kimina-Prover Preview and comparisons with o3-mini and Gemini, not GPT-5-mini with Kimina FS. Searches for the quoted percentages and for GPT-5-mini with specification, implementation, and end-to-end metrics found no passage addressing the claimed results. (LLM, conf=0.76)

  Experimental — accuracy not yet measured

May combine two claims.

The formal specifications in FVAPPS are often easily hackable, with verification correctness guarded by a layer of test cases.

“However, the formal specifications themselves are often easily hackable (see Section A.1), with verification correctness guarded by a layer of test cases.”

• cites [9] [9] Dougherty, Q. and Mehta, R. Proving the coding interview: A benchmark for formally verified code generation, 2025. URL https://arxiv.org/abs/2502.05714 . - sourcePartly supported

  The Discussion (page unavailable) acknowledges that some FVAPPS theorems may be vacuous or fail to express desirable properties, but does not say the specifications are often easily hackable. The Introduction and Results (pages unavailable) describe unit tests as a quality-assurance step for guarded samples, not as a general guarantee of verification correctness. (LLM, conf=0.83)

  Experimental — accuracy not yet measured

May combine two claims.

miniCodeProps contains 201 verification problems regarding data structures and induction problems, but does not include specification synthesis or equivalence tests.

“miniCodeProps [26] contains 201 verification problems regarding data structures and induction problems; however, they do not include specification synthesis or equivalence tests.”

• cites [26] [26] Lohn, E. and Welleck, S. minicodeprops: a minimal benchmark for proving code properties, 2024. URL https://arxiv.org/abs/2406.11915 . - sourceSupported

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

FVAPPS uses an LLM on scraped competition problems to automatically create formal specifications for 4715 problems, 1083 of which are guarded with test cases.

“FVAPPS [9] uses an LLM on scraped competition problems to automatically create formal specifications for 4715 problems, 1083 of which are guarded with test cases.”

• cites [9] [9] Dougherty, Q. and Mehta, R. Proving the coding interview: A benchmark for formally verified code generation, 2025. URL https://arxiv.org/abs/2502.05714 . - sourcePartly supported

  The Benchmark and Generation Pipeline sections describe FVAPPS as using an LLM to turn problems from the scraped APPS dataset into Lean specifications, and the Results section reports 4,715 samples. But Results says 2,089 samples passed the unit-test guard; 1,083 passed both that guard and a further plausibility check. The claim conflates the latter count with the number guarded by tests. (LLM, conf=0.88)

  Experimental — accuracy not yet measured

Probably not a substantial claim: may not pass S3 (load-bearing).

The FVAPPS benchmark is another code generation benchmark in Lean.

“The FVAPPS benchmark [9] is another code generation benchmark in Lean.”

• cites [9] [9] Dougherty, Q. and Mehta, R. Proving the coding interview: A benchmark for formally verified code generation, 2025. URL https://arxiv.org/abs/2502.05714 . - sourceSupported

Probably not a substantial claim: may not pass S3 (load-bearing).

The automatic nature of specification generation in FVEL means correctness is not guaranteed.

“However, the automatic nature of the specification generation means correctness is not guaranteed.”

• cites [23] [23] Lin, X., Cao, Q., Huang, Y., Wang, H., Lu, J., Liu, Z., Song, L., and Liang, X. Fvel: Interactive formal verification environment with large language models via theorem proving, 2024. URL https://arxiv.org/abs/2406.14408 . - sourceSupported

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

In the auxiliary dataset, one correctness proof spans 309 lines, while corresponding isomorphism proofs range from 29 to 82 lines.

“For example, one correctness proof spans 309 lines, while corresponding isomorphism proofs range from 29 to 82 lines.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

All problems in the auxiliary few-shot dataset include hand-written implementations, and some additionally include manually written equivalence and isomorphism proofs.

“All of these problems include hand-written implementations, and some of them additionally include manually written equivalence and isomorphism proofs.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Some problems involving complex non-computable specs required over an hour to write.

“Some problems involving complex non-computable specs required over an hour.”

Classified as probably not a substantial claim.

For the MD5 checksum problem (problem 162), the formal specification must, by necessity, describe the exact computation, making it closely related to the implementation itself.

“Here, the formal specification must, by necessity, describe the exact computation, making it closely related to the implementation itself.”

Probably not a substantial claim: may not pass S4 (based). May combine two claims.

All CLEVER specifications are manually written to be complete, implementation-agnostic, and free from exploitable artifacts, preventing models from shortcutting the intended semantics.

“All specifications are manually written to be complete, implementation-agnostic, and free from exploitable artifacts, preventing models from shortcutting the intended semantics.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

On average, writing a formal specification took annotators 25 minutes per problem, with an additional 15 minutes spent reviewing each other's specifications.

“On average, writing a formal specification took annotators 25 minutes per problem on average, with an additional 15 minutes spent reviewing each other's specifications.”

May combine two claims.

Claude-3.7 with COPRA can certify more implementations (14) than all other models, but its performance on specification certification is only comparable to other models.

“Another interesting observation is that Claude-3.7 , when used along with COPRA, can certify more implementations (14) than all other models; however, its performance on specification certification is only comparable to other models.”

• cites [31] [31] Thakur, A., Tsoukalas, G., Wen, Y., Xin, J., and Chaudhuri, S. An in-context learning agent for formal theorem-proving. In First Conference on Language Modeling , 2024. -Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

Converting a naturally computable task into a semantically equivalent, non-computable formulation without leaking implementation details required layered recursive structures and careful abstraction.

“This required converting a naturally computable task into a semantically equivalent, non-computable formulation without leaking implementation details. As shown in Figure 11 (in Section A.3), achieving this often involves layered recursive structures and careful abstraction to ensure both correctness and opacity.”

May combine two claims.

Problem 53 is the only problem for which end-to-end verified code generation succeeds across multiple models; it asks for the sum of two integers.

“This distinction is especially evident in the only problem for which an end-to-end verified code generation succeeds across multiple models: problem 53 , which asks for the sum of two integers.”

Classified as probably not a substantial claim. May combine two claims.

Each CLEVER problem includes a natural language description, a human-authored formal specification, a Lean function signature for the implementation, and Lean theorems for both specification equivalence and implementation correctness.

“Each problem includes a natural language description ( ν ), a human-authored formal specification ( ψ ∗ ), a Lean function signature ( π sig) for the implementation, and Lean theorems for both specification equivalence and implementation correctness.”

Probably not a substantial claim: may not pass S3 (load-bearing).

For Problem 160, the authors reconstructed the behavior using inductive definitions over token lists and arithmetic expressions because Lean lacks direct string-based evaluation.

“Since Lean lacks direct string-based evaluation, we had to reconstruct the behavior using inductive definitions over token lists and arithmetic expressions.”

• AssumptionRests on an assumption: Lean lacks direct string-based evaluation.

May combine two claims.

In Figure 3, the right side (d-f) uses a non-computable spec and requires symbolic reasoning to prove correctness.

“On the right (d-f), the spec is non-computable and requires symbolic reasoning to prove correctness.”

May combine two claims.

CLEVER evaluates both formal specification generation and implementation synthesis from natural language, requiring formal correctness proofs for both.

“The benchmark comprises of 161 programming problems; it evaluates both formal specification generation and implementation synthesis from natural language, requiring formal correctness proofs for both.”

May combine two claims.

In Figure 3, the GPT-4o-generated implementation in (e) does not mirror the spec, and the proof fails without further reasoning.

“Notably, the GPT-4o-generated implementation in (e) does not mirror the spec, and the proof fails without further reasoning.”

Classified as probably not a substantial claim.

The ground-truth specification for problem 53 is expressed in a way that deliberately obfuscates the target behavior.

“Despite the simplicity of the implementation, the ground-truth specification is expressed in a way that deliberately obfuscates the target behavior.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The authors chose not to formalize the MD5 checksum problem because they could not find any popular hashing libraries in Lean.

“Since we could not find any popular hashing libraries in Lean, we chose not to formalize this specific problem.”

• AssumptionRests on an assumption: There are no popular hashing libraries in Lean.

May combine two claims.

CLEVER avoids test-case supervision, LLM-generated annotations, and specifications that leak implementation logic or allow vacuous solutions.

“Unlike prior benchmarks, CLEVER avoids test-case supervision, LLM-generated annotations, and specifications that leak implementation logic or allow vacuous solutions.”

May combine two claims.

Few-shot prompting typically yields shorter, more brittle proofs, while COPRA-augmented configurations show higher robustness, with more consistent success and a broader range of proof strategies.

“Few-shot prompting typically yields shorter, more brittle proofs, while COPRA-augmented configurations show higher robustness, with more consistent success and a broader range of proof strategies.”

• cites [31] [31] Thakur, A., Tsoukalas, G., Wen, Y., Xin, J., and Chaudhuri, S. An in-context learning agent for formal theorem-proving. In First Conference on Language Modeling , 2024. -Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

GPT-4o few-shot achieves 84.472% spec compiled, 0.621% spec proved, 68.323% impl compiled, 0.621% impl proved, and 0% end-to-end.

“GPT-4o | FS | FS | FS | FS | 84.472% | 0.621% | 68.323% | 0.621% | 0%”

Probably not a substantial claim: may not pass S3 (load-bearing).

COPRA using Claude-3.7 found a proof for implementation certification.

“Figure 22 shows an example of a proof found for implementation certification by Claude-3.7 using COPRA.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The proof involves reasoning over factorial identities, case analysis, and symbolic manipulation.

“This proof, generated by COPRA using Claude-3.7, spans 35 lines and involves reasoning over factorial identities, case analysis, and symbolic manipulation.”

May combine two claims.

o4-mini achieved a higher implementation compilation rate, which contrasts with its lower success in proving correctness.

“A notable exception is the higher implementation compilation rate achieved by o4-mini , which contrasts with its lower success in proving correctness.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The non-computable specification uses an inductive definition of a recursive function.

“The non-computable specification uses an inductive definition of a recursive function.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Figure 11(b) shows a non-computable version of the specification that checks if the result matches the output of evaluating the expression without leaking the implementation.

“Figure 11(b) shows a non-computable version of the specification that checks if the result matches the output of evaluating the expression without leaking the implementation.”

May combine two claims.

GPT-4o with COPRA achieves 76.398% spec compiled, 1.863% spec proved, 68.323% impl compiled, 3.727% impl proved, and 0.621% end-to-end.

“GPT-4o | FS | COPRA | FS | COPRA | 76.398% | 1.863% | 68.323% | 3.727% | 0.621%”

• cites [31] [31] Thakur, A., Tsoukalas, G., Wen, Y., Xin, J., and Chaudhuri, S. An in-context learning agent for formal theorem-proving. In First Conference on Language Modeling , 2024. -Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

This is the only HumanEval-derived task with full verification across multiple approaches.

“This is the only HumanEval-derived task with full verification across multiple approaches.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The proof generated by COPRA using Claude-3.7 spans 35 lines.

“This proof, generated by COPRA using Claude-3.7, spans 35 lines and involves reasoning over factorial identities, case analysis, and symbolic manipulation.”

May combine two claims.

o4-mini few-shot achieves 82.609% spec compiled, 1.242% spec proved, 83.230% impl compiled, 1.863% impl proved, and 0.621% end-to-end.

“o4-mini | FS | FS | FS | FS | 82.609% | 1.242% | 83.230% | 1.863% | 0.621%”

May combine two claims.

Claude-3.7 with COPRA achieves 81.366% spec compiled, 1.242% spec proved, 65.217% impl compiled, 8.696% impl proved, and 0.621% end-to-end.

“Claude-3.7 | FS | COPRA | FS | COPRA | 81.366% | 1.242% | 65.217% | 8.696% | 0.621%”

• cites [31] [31] Thakur, A., Tsoukalas, G., Wen, Y., Xin, J., and Chaudhuri, S. An in-context learning agent for formal theorem-proving. In First Conference on Language Modeling , 2024. -Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

Claude-3.7 few-shot achieves 86.957% spec compiled, 0.621% spec proved, 65.217% impl compiled, 1.863% impl proved, and 0.621% end-to-end.

“Claude-3.7 | FS | FS | FS | FS | 86.957% | 0.621% | 65.217% | 1.863% | 0.621%”

May combine two claims.

DeepSeek-R1 few-shot achieves 71.42% spec compiled, 0.621% spec proved, 60.870% impl compiled, 5.559% impl proved, and 0.621% end-to-end.

“DeepSeek-R1 | FS | FS | FS | FS | 71.42% | 0.621% | 60.870% | 5.559% | 0.621%”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Figure 11(a) evaluates the expression and later checks if the output matches the result, which is computable.

“Figure 11(a) evaluates the expression and later checks if the output matches the result (not specified in the figure), which is computable.”

May combine two claims.

The design of problem 53's specification makes the equivalence proof non-trivial and requires models (or COPRA) to recover the algebraic structure underlying addition.

“This design makes the equivalence proof non-trivial and requires models (or COPRA) to recover the algebraic structure underlying addition.”

Probably not a substantial claim: may not pass S4 (based).

Writing CLEVER specifications as non-computable logical propositions ensures that models cannot copy implementation logic from specification syntax.

“All formal specifications are written as non-computable logical propositions - i.e., they use quantifiers and logical connectives that cannot be directly evaluated - ensuring that models cannot copy implementation logic from specification syntax.”

May combine two claims.

The CLEVER pipeline avoids the pitfalls of both automatically generated specifications and test-based supervision.

“This rigorous pipeline avoids the pitfalls of both automatically generated specifications and test-based supervision.”

Classified as probably not a substantial claim.

Pass@k-seconds with k=600 reports the fraction of tasks where Lean successfully compiles outputs and accepts proofs within a 600-second time budget.

“Pass@k-seconds with k = 600 reports the fraction of tasks where Lean successfully compiles the outputs and accepts the associated proofs within a 600-second time budget.”

May combine two claims.

Despite strong models like GPT-4o achieving high compilation rates, formal correctness remains challenging.

“Despite strong models like GPT-4o achieving high compilation rates, formal correctness remains challenging: no approach has yet succeeded across all stages on more than one problem (specifically problem 53).”

Classified as probably not a substantial claim.

Failures at various stages of the CLEVER pipeline are independently diagnosed using Lean's type checker.

“More generally, failures at the various stages of our pipeline are independently diagnosed using Lean's type checker.”

• AssumptionRests on an assumption: Lean's type checker is a reliable arbiter of machine-checkable correctness.

Classified as probably not a substantial claim.

CLEVER requires the generated implementation π to satisfy the ground-truth specification ψ* instead of the model-generated specification ψ.

“For example, note that we require the generated implementation π to satisfy the ground-truth specification ψ ∗ instead of the model-generated specification ψ .”

Classified as probably not a substantial claim.

A synthesis attempt is deemed successful only when both proofs generated in the two stages are fully verified by Lean's type checker.

“A synthesis attempt is deemed successful only when both the proofs generated in the two stages are fully verified by Lean's type checker.”

• Also stated in: § 3 Evaluation · p. 6 · plain

  “A task is marked as solved only if both the formal specification and the implementation are generated and verified via Lean's type checker.”

• AssumptionRests on an assumption: Lean's type checker is a reliable arbiter of machine-checkable correctness.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

Proof line counts serve as a coarse indicator of reasoning complexity.

“Proof line counts serve as a coarse indicator of reasoning complexity.”

May combine two claims.

The human-curated specifications in CLEVER ensure completeness and robustness, closing loopholes and surfacing the real verification complexity hidden in everyday programming problems.

“Our human-curated specifications ensure completeness and robustness, closing such loopholes and surfacing the real verification complexity hidden in everyday programming problems.”

May combine two claims.

By using non-computable specs across CLEVER, the benchmark eliminates leakage and enforces truly verified reasoning from models.

“By using non-computable specs across our benchmark, we eliminate leakage and enforce truly verified reasoning from models.”

May combine two claims.

The structurally rich proof landscape of CLEVER contrasts with the often-flat logical forms seen in MiniF2F and underscores the need for symbolic agents like COPRA that can perform guided proof search beyond tactic chaining.

“This structurally rich proof landscape contrasts with the often-flat logical forms seen in MiniF2F and underscores the need for symbolic agents like COPRA that can perform guided proof search beyond tactic chaining.”

• cites [38] [38] Zheng, K., Han, J. M., and Polu, S. Minif2f: a cross-system benchmark for formal olympiadlevel mathematics. arXiv preprint arXiv:2109.00110 , 2021. ``` /--solve_elections: There are n voters, and two ways to convince each of them to vote for you. The first way to convince the i -th voter is to pay him p i coins. The second way is to make m i other voters vote for you, and the i -th voter will vote for free. Moreover, the process of such voting takes place in several steps. For example, if there are five voters with m 1 = 1 , m 2 = 2 , m 3 = 2 , m 4 = 4 , m 5 = 5 , then you can buy the votNot matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S4 (based).

Verifying the generated specification via isomorphism proofs ensures semantic fidelity.

“In particular, verifying the generated specification via isomorphism proofs ensures semantic fidelity and introduces a novel opportunity: verified mining of natural language and formal specification pairs from model generations, which could be reused for bootstrapping new training data.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

The paper does not involve crowdsourcing nor research with human subjects.

“Our paper does not involve crowdsourcing nor research with human subjects.”

Probably not a substantial claim: may not pass S4 (based).

Complete formal specifications cannot be done accurately with automatic annotation.

“Here, we aim to provide complete formal specifications, which cannot be done accurately with automatic annotation.”

Classified as probably not a substantial claim.

The paper's primary evaluation metric focuses strictly on semantic correctness.

“Our primary evaluation metric focuses strictly on semantic correctness: a task is considered successful only if both the specification and the implementation are formally certified via Lean proofs.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

Writing non-computable specifications is a non-trivial task that requires a deep understanding of the problem.

“Writing non-computable specifications is a non-trivial task that requires a deep understanding of the problem.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based). May combine two claims.

The code link and data link are shared in the paper.

“The code link, data link are shared in the paper.”

Probably not a substantial claim: may not pass S3 (load-bearing).

All the source code is released.

“All the source code is released, and every Github repository has a README.”

Probably not a substantial claim: may not pass S3 (load-bearing).

COPRA's system prompt, used for both isomorphism and correctness, is nearly identical to the original one in the COPRA paper.

“COPRA's system prompt, used for both isomorphism and correctness, is nearly identical to the original one in the COPRA paper [31].”

• cites [31] [31] Thakur, A., Tsoukalas, G., Wen, Y., Xin, J., and Chaudhuri, S. An in-context learning agent for formal theorem-proving. In First Conference on Language Modeling , 2024. -Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Classified as probably not a substantial claim.

Our evaluation protocol is deliberately staged, decomposing the pipeline into independently checkable phases: specification generation, isomorphism proof, implementation synthesis, and correctness proof.

“Our evaluation protocol is deliberately staged, decomposing the pipeline into independently checkable phases: specification generation, isomorphism proof, implementation synthesis, and correctness proof.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The authors do not use their own compute, making calls to models hosted elsewhere.

“We don't use our own compute as we make calls to models hosted elsewhere”

Classified as probably not a substantial claim. May combine two claims.

Verifying generated specifications via isomorphism proofs introduces a novel opportunity: verified mining of natural language and formal specification pairs from model generations, which could be reused for bootstrapping new training data.

“In particular, verifying the generated specification via isomorphism proofs ensures semantic fidelity and introduces a novel opportunity: verified mining of natural language and formal specification pairs from model generations, which could be reused for bootstrapping new training data.”

Classified as probably not a substantial claim.

By enforcing a separation between specification intent and implementation behavior, the benchmark demands genuine reasoning rather than pattern matching or memorization.

“By enforcing a separation between specification intent and implementation behavior, the benchmark demands genuine reasoning rather than pattern matching or memorization.”

Classified as probably not a substantial claim.

No model is trained in this work.

“We don't train any model in this work, as it is a benchmark paper.”

Probably not a substantial claim: may not pass S2 (checkable).

A verified code generation benchmark must require proofs of full program behavior, not just program properties.

“This highlights the necessity of a verified code generation benchmark to require proofs of full program behavior, not just program properties.”

Probably not a substantial claim: may not pass S3 (load-bearing).

All the models used in the work are mentioned in the paper.

“But we mention all the models we have used.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

All the licenses are mentioned in the GitHub repositories of the links shared.

“All the licenses are mentioned in the GitHub repositories of the links shared.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

The core method development was not carried out with the involvement of LLMs.

“The core method development was not carried out with the involvement of LLMs.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

While the implementation is simple, the spec equivalence proof requires symbolic reasoning.

“While the implementation is simple, the spec equivalence proof requires symbolic reasoning.”

Probably not a substantial claim: may not pass S4 (based). May combine two claims.

Our tasks reflect the branching structure of real-world programs, requiring symbolic reasoning over control flow, recursion, and invariants-scenarios where automation alone breaks down.

“In contrast, our tasks reflect the branching structure of real-world programs, requiring symbolic reasoning over control flow, recursion, and invariants-scenarios where automation alone breaks down.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Implementation compilation includes type-checking against the declared function signature and validation against a suite of example-based test cases adapted from the original HUMANEVAL prompts.

“In particular, implementation compilation includes not only type-checking against the declared function signature, but also validation against a suite of example-based test cases adapted from the original HUMANEVAL prompts.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

All the models used for the experiments are described in the evaluation section of the paper.

“All the models used for the experiments are described in the evaluation section.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The code used for running the evaluations is shared in the paper.

“The code used for running these evaluations is shared in the paper.”

Classified as probably not a substantial claim.

By combining structural complexity with formal soundness, non-leakage by design, and staged verification, the benchmark offers a rigorous, semantics-grounded testbed for verified code generation.

“By combining structural complexity with formal soundness, non-leakage by design, and staged verification, the benchmark offers a rigorous, semantics-grounded testbed for verified code generation.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

The research conforms to the NeurIPS Code of Ethics.

“I read the code of ethics, and I can assure that my research conforms to it.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

Every Github repository has a README.

“All the source code is released, and every Github repository has a README.”

Probably not a substantial claim: may not pass S3 (load-bearing).

We need multiple inductive recursive definitions to ensure that the specification is clean and non-computable.

“One can notice that we need multiple inductive recursive definitions to ensure that the specification is clean and non-computable.”

Classified as probably not a substantial claim.

The paper tests the capabilities of various LLMs on its problems.

“we test the capabilities of various LLMs on our problems”