{"id":"32fc08a9-2d64-4fe7-8807-662d0cbabb24","arxiv_id":"2607.06341","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"unknown","formal_verification":"none","parameter_count":4,"one_line_summary":"A general LLM code agent paired with a Coq verification harness automatically proves all 4,257 Iris separation logic lemmas and 318 reglang lemmas with zero failures.","lead":"This paper shows that a general-purpose LLM coding agent (Claude Code), wrapped in a verification harness that feeds back errors, can automatically prove all 4,257 lemmas of the Iris separation logic framework in Coq with zero failures. If correct, this removes the primary expert bottleneck in formal software verification, potentially making verified software development routine.","discovery_kind":"unclear","skeptic_critique":{"model":"glm-5.2","headline":"The memorization concern is the most load-bearing issue, and the paper's strongest counter-evidence (iris-lean) is weaker than it appears: the corresponding Coq proofs for those 72 lemmas are publicly available, so the model could be translating memorized proofs rather than synthesizing from scratch","rationale":"The reader correctly identified memorization as the most fragile premise, and I agree it is the single most load-bearing concern. The paper's soundness guarantee (Coq/Lean kernel checking) is solid—every accepted proof is correct regardless of how it was found. The question is whether the result generalizes beyond proofs the model may have seen during training, which determines whether the 'full coverage' claim reflects a genuine capability or a recall artifact. The reader's assessment of the iris-lean counter-evidence as 'too small and structurally similar' is accurate but understates the specific problem: the corresponding Coq proofs are public, so the model has a direct source to translate from. The reader also raised two secondary concerns (single run with no variance analysis, no ablation isolating harness contribution) which are valid but less load-bearing than memorization. The CONDITIONAL verdict with MODERATE confidence is appropriate: the result is promising and the proofs are kernel-verified, but independent replication on genuinely novel benchmarks is needed before full acceptance. I note one additional consideration the reader did not emphasize: the max retry count of 28 (against a cap of 30) on at least one Iris lemma means the zero-failure result came close to the boundary in a single run, making the absence of variance analysis slightly more concerning than the reader suggested. However, this does not rise above the memorization concern as the primary issue.","tokens_in":20113,"tokens_out":4096,"duration_ms":225696,"concrete_test":"For the 72 iris-lean lemmas, extract the tactic-level structure of each Lean proof Aria produces (sequence of tactic invocations, case-split structure, named lemmas applied) and compare it against the tactic-level structure of the corresponding Coq proof in the upstream Iris repository. Compute a structural similarity score (e.g., normalized tree-edit distance on the proof script AST). If the median similarity is high (e.g., >70% of tactics match in type and order), this indicates the model is translating memorized Coq proofs into Lean rather than synthesizing proofs from the lemma statement alone. If similarity is low, the memorization concern is substantially weakened.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim—full coverage with zero failures—requires that the results reflect genuine proof synthesis, not recall from training data. The paper acknowledges this (Section VI-B) but its counter-evidence has a specific gap. (1) The claim that generated proofs 'differ from the upstream Iris proofs' is unquantified: a model can produce a textually different proof while reproducing the same tactic structure, case-split order, and lemma applications from memory. No systematic structural comparison is reported. (2) The iris-lean experiment (72 lemmas, Section VI-F) is presented as the strongest counter to memorization because 'no Lean proof exists.' But the corresponding Coq proofs for these exact lemmas DO exist in the public Iris repository, and the paper itself notes these are 'the same algebra' as the Coq versions. The model could be translating memorized Coq proof structure into Lean syntax. (3) All four benchmarks draw from publicly available, widely-cited repositories (Iris, RustBelt, reglang) that a frontier model trained on internet-scale data has almost certainly seen. The sandbox protocol (no network, no git) prevents inference-time retrieval but cannot prevent recall from training-time exposure. (4) The 79.2% first-attempt rate on Iris core is high for proofs described as taking 'hours or even days' for experts; while not impossible for a capable model, it is the rate most directly explained by familiarity. The paper does not report any experiment on lemmas that are both novel and lack a structural analog in public repositories, which is the only clean test against memorization.","agreement_with_reader":"agree"},"referee_report":{"model":"glm-5.2","summary":"The paper presents Aria, a system that pairs a general-purpose LLM code agent (Claude Code on Claude Opus 4.7) with a verification harness to automatically prove lemmas in Coq and Lean. The harness enforces soundness (kernel acceptance), completeness (no dropped goals), and termination (tactic timeouts), and is expressed in a declarative language called HHL. The central empirical claim is full coverage: all 4,257 Iris core lemmas, 217 RustBelt lemmas, all 318 reglang lemmas, and 72 iris-lean lemmas are proved with zero failures and no expert intervention. The paper compares favorably against prior LLM-based Coq provers (12–48% coverage) and includes a cross-prover (Lean) experiment and a private-vs-open-source model comparison.","tokens_in":20935,"tokens_out":1484,"duration_ms":298460,"significance":"The paper's strengths are substantial. The verification harness design is sound: trust is anchored in the Coq/Lean kernel, and the completeness check (no silently dropped or weakened lemmas) addresses a real gap in verifier-in-the-loop agent setups. The HHL abstraction is a genuine contribution, making the harness policy auditable and retargetable. The empirical scope—4,859 total lemmas across four independent benchmarks including the demanding Iris separation logic—is beyond what prior LLM prover evaluations have attempted. The reproducible code repository and the cross-model comparison (Opus 4.7 vs. Kimi K2.6) add credibility. The falsifiable claim of zero failures across the entire Iris core is a strong, testable prediction.","major_comments":[{"comment":"Section VI-B: The memorization concern is the most load-bearing issue for the central claim of genuine proof synthesis. The paper states that 'the proofs Aria generates differ from the upstream Iris proofs—it constructs them rather than recalling them,' but provides no systematic structural comparison (e.g., tactic sequence overlap, case-split order, lemma-application frequency). A textually different proof can reproduce the same proof structure from memory. Without quantification, the claim that generated proofs differ from upstream (Section VI-B) is unsupported. A structural diff metric or a comparison of tactic-graph isomorphism would substantially strengthen this.","section":null},{"comment":"Section VI-F: The iris-lean experiment (72 lemmas) is presented as the strongest counter to memorization because 'no Lean proof exists.' However, the paper itself notes these are 'the same algebra' as the corresponding Coq modules (functions.v, mra.v, ufrac.v), whose proofs are publicly available in the Iris repository. The model could be translating memorized Coq proof structure into Lean syntax. The paper should explicitly acknowledge this translation-from-memory pathway and discuss why the structural similarity to existing Coq proofs does not undermine the novelty claim. Ideally, a held-out benchmark with no publicly available proof in any prover would be included, or the iris-lean lemmas should be shown to require proof structures not present in the Coq versions.","section":null},{"comment":"Section VI-B: The 79.2% first-attempt success rate on Iris core is high for proofs the paper describes as taking 'hours or even days' for experts. While not impossible for a capable model, this rate is the metric most directly explained by training-time familiarity with the publicly available Iris repository. The sandbox protocol (Section VI-A: no network, no git) prevents inference-time retrieval but cannot prevent recall. The paper would benefit from an experiment on lemmas added or modified after the model's training cutoff, or from reporting the distribution of first-attempt successes across lemma difficulty tiers to show that the rate is not dominated by trivial lemmas. Without such evidence, the memorization concern remains a correctness-risk for the central claim.","section":null},{"comment":"Sections V-B, VI-A: Several free parameters—the retry cap of 30, the session reuse window of 6, the tactic timeout of 300 s, and the polish rounds of 2—are set to specific values without sensitivity analysis. The retry cap in particular is load-bearing: the paper reports that no lemma exhausted the budget (max 28 retries on Iris core), but it is unclear whether the zero-failure result depends on this specific cap or would hold under a tighter budget. A sensitivity analysis on at least the retry cap and session reuse window would clarify whether the full-coverage claim is robust or contingent on a finely tuned parameter set.","section":null}],"minor_comments":[{"comment":"Figure 4 caption mentions 4,123 lemmas (96.9%) with module-qualified log paths, with 134 omitted due to ambiguous file names. The main text (Section VI-B, Table III) reports 4,257. The discrepancy should be noted earlier or the figure should use the full count to avoid confusion.","section":null},{"comment":"Section VI-G: The comparison between Opus 4.7 and Kimi K2.6 is on only 40 lemmas (frac_auth.v). The claim of a 'genuine capability gap on long proofs' beyond 50 lines is stated qualitatively without supporting data. Either include the data for longer proofs or soften the claim to match what is reported.","section":null},{"comment":"Section IV-A, Figure 2: The HHL example is helpful but the compilation target (Table II) could include a brief note on how the Turn post-hook is implemented in the driver, as this is flagged as having 'no native counterpart.' A one-sentence clarification would improve reproducibility.","section":null},{"comment":"Section VI-H: The rubric criteria for proof polishing are illustrated with a single example (discrete_cmra_mixin). It would help to report what fraction of proofs passed all rubric criteria without polishing, and how many rounds were typically needed, to give a sense of the polish stage's practical impact.","section":null},{"comment":"The paper uses 'Claude Opus 4.7' throughout, but the model's training data cutoff and corpus composition are not publicly known. This should be explicitly acknowledged in the memorization discussion (Section VI-B), as it directly affects the interpretability of the first-attempt success rates.","section":null},{"comment":"Section VIII: Cobblestone is cited as reaching 48% (58% with oracle guidance) on general Coq. The comparison would be sharper if the paper noted whether Cobblestone was evaluated on any Iris or separation-logic benchmarks, or if the comparison is strictly on different corpora. This affects the strength of the 'Aria differs on both axes' claim.","section":null}],"recommendation":"major_revision","confidential_remarks":"The memorization concern is the central issue. The paper's claim of full coverage with zero failures is striking, but without a held-out benchmark or structural proof comparison, it is difficult to distinguish genuine synthesis from recall. The iris-lean experiment is weaker than presented because the corresponding Coq proofs exist publicly. I recommend major revision with a specific request for (a) a structural comparison between generated and upstream proofs, and (b) discussion of the translation-from-memory pathway for iris-lean. If the authors can provide even a small held-out experiment (e.g., lemmas modified post-cutoff), that would go a long way. The HHL contribution and harness design are solid and do not require revision."},"author_rebuttal":{"model":"glm-5.2","summary":"We thank the referee for a careful and constructive report. The referee recognizes the soundness of the harness design, the value of HHL as an auditable abstraction, the unprecedented empirical scope, and the testability of the zero-failure claim. The major comments all concern the memorization threat to the central claim and the robustness of the parameter choices. We address each below.","responses":[{"response":"The referee is correct that our current evidence—a qualitative statement that proofs differ textually—is insufficient to rule out structural memorization. We will add a quantitative structural comparison in revision. Specifically, we plan to: (1) compute tactic-sequence overlap (edit distance over normalized tactic tokens) between Aria-generated and upstream proofs; (2) compare case-split structure (bullet nesting depth and branching order); (3) compare lemma-application frequency distributions. We will report these metrics across all 4,257 Iris core lemmas. We note that the example in Section VI-H already shows a concrete structural difference (the LLM enumerates subgoals explicitly while the human proof uses 'try done' to collapse them), but we agree this should be systematic rather than illustrative. We cannot fully rule out that some proofs share structural templates with upstream—this is an inherent limitation of evaluating on a public library with a model whose training data is unknown. We will state this limitation explicitly.","revision_made":"yes","referee_comment":"Section VI-B: The memorization concern is the most load-bearing issue. The paper claims generated proofs differ from upstream but provides no systematic structural comparison (tactic sequence overlap, case-split order, lemma-application frequency). A textually different proof can reproduce the same proof structure from memory."},{"response":"This is a fair point that we should and will acknowledge explicitly. The iris-lean lemmas are indeed the same algebraic content as the corresponding Coq modules (functions.v, mra.v, ufrac.v), and the model could in principle translate memorized Coq proof structure into Lean. The iris-lean experiment therefore demonstrates cross-prover transfer and the retargetability of the harness, but it is not a clean memorization control. We will revise Section VI-F to state this limitation clearly and downgrade the claim accordingly. Regarding the ideal experiment—a held-out benchmark with no publicly available proof in any prover—we agree this would be the strongest control. We are investigating whether recently added Iris lemmas postdating the model's training cutoff can serve this purpose, but we cannot commit to having results ready in time for the next revision. We will be transparent about this gap.","revision_made":"partial","referee_comment":"Section VI-F: The iris-lean experiment is presented as the strongest counter to memorization because no Lean proof exists, but the same algebra exists in publicly available Coq proofs. The model could be translating memorized Coq proof structure into Lean syntax."},{"response":"We agree that the 79.2% first-attempt rate is the metric most vulnerable to the memorization explanation, and we should provide more evidence. Two responses: (1) We will add a difficulty-tier breakdown of first-attempt success rates, stratified by proof length and retry count, to show the rate is not dominated by trivial lemmas. The per-module breakdown in Figure 4 already shows variation (71.9% in algebra vs. 87.3% in base_logic), but a within-module difficulty stratification is more informative. (2) Regarding lemmas added after the training cutoff: we are actively investigating this. The Iris repository is continuously updated, and if we can identify a sufficient number of lemmas added after Claude Opus 4.7's training cutoff, we will run Aria on them and report the results. However, we cannot guarantee a large enough sample exists at this time. We acknowledge that without such an experiment, the recall-from-training pathway cannot be fully eliminated. We will state this as a standing limitation rather than claim we have closed the gap.","revision_made":"partial","referee_comment":"Section VI-B: The 79.2% first-attempt success rate is high for proofs described as taking experts hours or days. This rate is the metric most directly explained by training-time familiarity with the publicly available Iris repository. The sandbox prevents inference-time retrieval but cannot prevent recall. An experiment on lemmas added or modified after the model's training cutoff, or a difficulty-tier breakdown, would help."},{"response":"The referee is right that a sensitivity analysis is needed, particularly for the retry cap since it is most directly tied to the zero-failure claim. We will conduct and report a sensitivity analysis varying the retry cap (e.g., 5, 10, 15, 20, 25) and the session reuse window (e.g., 1, 3, 6, 12) on at least a representative subset of the Iris core, and ideally the full benchmark if compute permits. We note that the max retry count observed was 28 out of 30, which means the result is indeed contingent on the cap being at least 28—a tighter cap would have produced failures. This is an important fact that we should make more prominent. We will report the distribution of retry counts in finer detail (not just the mean and max) so readers can see how many lemmas are near the cap. For the tactic timeout and polish rounds, we will add brief discussion of why those values were chosen and whether results are sensitive to them, though we expect these to be less critical.","revision_made":"yes","referee_comment":"Sections V-B, VI-A: Several free parameters (retry cap of 30, session reuse window of 6, tactic timeout of 300s, polish rounds of 2) are set without sensitivity analysis. The retry cap is load-bearing: no lemma exhausted the budget (max 28 retries), but it is unclear whether zero-failure depends on this specific cap. A sensitivity analysis on at least the retry cap and session reuse window would clarify robustness."}],"tokens_in":19967,"tokens_out":1380,"duration_ms":205166,"standing_objections":["The memorization concern cannot be fully eliminated without knowledge of the model's training data, which is not publicly available. No experiment on a public benchmark with a proprietary model can definitively rule out that the model has seen the proofs during training. We can mitigate this with structural comparisons, difficulty stratification, and post-cutoff lemmas if available, but the concern is fundamental to evaluating LLM-based proof synthesis on public libraries.","A fully clean memorization control—a benchmark with no publicly available proof in any prover—does not currently exist at the scale needed to replicate the Iris core evaluation. The iris-lean experiment is the closest available but, as the referee correctly notes, shares algebraic content with public Coq proofs."]},"desk_editor":{"model":"glm-5.2","letter":"The headline: A general LLM code agent (Claude Code on Opus 4.7) paired with a verification harness proves all 4,257 Iris core lemmas, 217 RustBelt lemmas, 318 reglang lemmas, and 72 iris-lean lemmas — zero failures, no expert intervention. If this holds up, it is a genuine step change for automated formal verification. The proofs are kernel-checked (Coq and Lean), so soundness of individual proofs is not in question. The architectural insight — that you can drop hand-engineered proof-search strategies and just let a code agent work against a verifier with feedback — is the real contribution here, and it is well-motivated. HHL, the declarative harness language, is a modest but useful piece of engineering that makes the policy auditable and retargetable. The completeness check (no dropped or weakened goals) is a nice catch that I have not seen emphasized in prior agent-prover work. The comparison with prior LLM provers on reglang (318/318 vs. ~1 in 8) is a clean apples-to-apples win. The open-source model comparison (Kimi K2.6) is a good-faith effort at generality, though the capability gap on long proofs is honestly reported. The soft spot is memorization, and the reader and stress-test are right to flag it as load-bearing. The paper's counter-argument is thin. Saying generated proofs 'differ from upstream' is unquantified — a model can reproduce the same tactic structure and case-split order with different surface text. The iris-lean experiment (72 lemmas) is the strongest counter-evidence because no Lean proof exists, but the corresponding Coq proofs for those exact lemmas are public, and the paper itself says these are 'the same algebra.' So the model could be translating memorized Coq proof structure into Lean syntax. That said, I partially disagree with the stress-test's framing. A 79.2% first-attempt rate on Iris core is high, but the retry distribution and per-lemma timing (some proofs taking hours and 20+ retries) are not what pure recall looks like. The variance across modules — algebra being hardest, bi being easiest — tracks logical complexity, not memorization patterns. And the sandbox protocol (no network, no git) at least rules out inference-time retrieval. The missing experiment is obvious and the paper should have done it: a benchmark of genuinely novel lemmas with no structural analog in any public repository. Without that, the 100% claim is promising but not airtight. There is also no ablation isolating the harness from raw model capability, and no variance analysis — a single run per benchmark. This paper is for the formal verification and LLM-for-proving communities. It deserves a serious referee who will push hard on the memorization question and demand the novel-lemma experiment. The core architectural claim is worth engaging with regardless of whether the coverage numbers survive scrutiny.","headline":"100% proof coverage on Iris using a general code agent plus a verification harness — real result, but memorization concern is not fully discharged","tokens_in":21183,"tokens_out":689,"would_cite":true,"duration_ms":124848,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"glm-5.2","headline":"LLM Code Agent Proves Every Lemma in Iris Verification Library","keywords":["formal verification","automated theorem proving","interactive theorem proving","Coq","Lean","Iris separation logic","large language models","LLM code agents"],"falsifier":"Run Aria on a substantial body of lemmas from a Coq or Lean development created entirely after Claude Opus 4.7's training data cutoff, with no public analog in any form. If the success rate drops sharply, memorization is implicated; if it holds, the approach generalizes.","tokens_in":20161,"feed_emoji":"✅","tokens_out":1431,"duration_ms":251803,"temperature":0.7,"pith_summary":"This paper argues that the elaborate proof strategies prior automated theorem provers use—premise selectors, tactic-by-tactic search, divide-and-conquer decomposition—are not just unnecessary but actively limiting. The authors show that handing an entire unproved lemma to a general-purpose LLM code agent (Claude Code running Claude Opus 4.7), wrapped in a verification harness that checks each attempt against the Coq kernel and feeds back precise errors, achieves full coverage on benchmarks where prior systems proved only a fraction. The system, called Aria, proves all 4,257 lemmas of the Iris separation logic core, 217 RustBelt lemmas verifying Rust's standard libraries, all 318 lemmas of the reglang library (where prior provers managed roughly one in eight), and 72 not-yet-ported lemmas in a Lean 4 port of Iris—with zero failures and no human expert intervention. The central mechanism is the feedback loop: the agent proposes a proof, the harness checks it step-by-step against the Coq kernel, and on failure returns the exact line, error message, and pending proof goal, which the agent uses to revise. The harness also enforces completeness (no target lemma silently dropped or weakened) and termination (a 300-second per-tactic timeout catches divergent tactics). The authors express the harness policy in a declarative language called HHL, making it auditable and portable across agent runtimes and proof assistants.","feed_headline":"Code Agent Proves All 4,257 Iris Lemmas With Zero Failures","feed_subtitle":"No proof strategy, no premise selector, no expert—just an LLM code agent in a feedback loop with the Coq kernel. If real, verified software ","key_machinery":"The verification harness: a wrapper around the Coq (or Lean) kernel that checks each candidate proof step-by-step, returns the failing line, error message, and pending goal on rejection, enforces a ban on Admitted/Axiom, checks that the target lemma is still present and unweakened, and caps each tactic at 300 seconds to catch divergence. The harness is expressed in HHL, a declarative language compiled to Python hooks on the Claude Code SDK.","core_discovery":"The discovery is that a deliberately coarse loop—general code agent plus sound verifier with structured error feedback—outperforms systems built around hand-engineered proof strategies. The agent makes every strategic decision itself: which lemma to apply, how to decompose a goal, when to backtrack, which definitions to look up. The harness contributes only the ground-truth check (the Coq or Lean kernel accepts or rejects) and the feedback that turns rejection into a revision signal. This suffices for 100% coverage on the hardest separation-logic proofs the authors could find, including the full Iris core and its downstream Rust safety applications, suggesting that the bottleneck in automatm","pith_inferences":["The 100% success rate on Iris—a widely-cited, publicly available Coq development—cannot fully rule out memorization without knowing Claude Opus 4.7's training corpus composition. The iris-lean experiment (72 novel lemmas with no prior Lean proofs) partially addresses this, but the small sample and structural similarity to existing Coq versions limit its force as a counterexample. A stronger test w","If the approach scales beyond Iris to arbitrary Coq/Lean developments, it could shift the human expert's role from writing proofs to writing specifications—the unautomated upstream task the authors flag as a natural next step. This would change the economics of verified software: specification design becomes the bottleneck rather than proof construction.","The 380-hour model time for 4,257 lemmas (averaging ~321 seconds per lemma) suggests the approach is practical for library-scale verification but may face cost and latency challenges for interactive development workflows where a developer needs a proof in seconds, not minutes.","The observation that splitting developments into smaller lemmas improves the agent's first-attempt rate (90.3% on finer-grained iris-lean lemmas vs. 75.5% on coarser Coq versions) implies that proof structure itself is a lever: library authors could optimize lemma granularity for automated provability, not just human readability."],"forward_implications":["If the result generalizes, the manual proof bottleneck that keeps verified software from scaling could ease substantially: any Coq or Lean development with a sound kernel could potentially be automated by pairing a code agent with a feedback harness, without building domain-specific proof strategies.","The HHL harness language could become a reusable interface layer: the same harness description could drive different agent backends (Claude Code, Codex, others) and different proof assistants (Coq, Lean), making the approach portable across the verification ecosystem.","The finding that the agent independently discovers the strategy of mimicking structurally similar nearby proofs—rather than following an externally imposed search policy—suggests that future improvements may come from better context assembly rather than more elaborate proof-search machinery.","The capability gap observed between private and open-source models on long proofs (beyond ~50 lines) identifies a concrete frontier: open-source models that can maintain correctness over long multi-step constructions would democratize the approach."],"fun_headline_variants":["General LLM code agent beats hand-engineered Coq proof strategies on every lemma","Letting code agents pick proof strategy yields 100% coverage on Iris separation logic","No proof strategy, no premise selector—code agent proves all 318 reglang theorems","Code agent plus verification harness achieves full coverage on hardest separation-logic pr","Giving LLM code agents strategic freedom outperforms fixed proof tactics on Iris and Lean"],"cache_read_input_tokens":0,"weakest_assumption_plain":"The paper's most fragile premise is that the 100% success rate reflects genuine proof synthesis rather than recall of proofs the model may have seen during training. Iris is a widely-cited, publicly available Coq development, and Claude Opus 4.7's training data is not publicly known. The authors argue the generated proofs differ from upstream Iris proofs, but this does not fully exclude the possibility that the model learned proof patterns or individual tactics from the Iris源","fun_headline_variants_meta":{"raw":{"variants":["General LLM code agent beats hand-engineered Coq proof strategies on every lemma","Letting code agents pick proof strategy yields 100% coverage on Iris separation logic","No proof strategy, no premise selector—code agent proves all 318 reglang theorems","Code agent plus verification harness achieves full coverage on hardest separation-logic proofs","Giving LLM code agents strategic freedom outperforms fixed proof tactics on Iris and Lean"]},"model":"glm-5.2","effort":"high","cost_usd":0.0,"raw_usage":{"total_tokens":844,"prompt_tokens":736,"completion_tokens":108,"prompt_tokens_details":null},"tokens_in":736,"tokens_out":108,"duration_ms":124814,"temperature":1.0,"reasoning_tokens":null,"cache_read_input_tokens":0,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-08T09:10:44.066477+00:00","model_set":{"reader":"glm-5.2"},"falsifier":"Run Aria on a substantial body of lemmas from a Coq or Lean development created entirely after Claude Opus 4.7's training data cutoff, with no public analog in any form. If the success rate drops sharply, memorization is implicated; if it holds, the approach generalizes.","supporting_citations":[],"review_version":1}