ai-research-survey

scan.json (27630B)

---

 {
   "paper": {
     "title": "AutoVerus: Automated Proof Generation for Rust Code",
     "authors": [
       "Chenyuan Yang",
       "Xuheng Li",
       "Md Rakib Hossain Misu",
       "Jianan Yao",
       "Weidong Cui",
       "Yeyun Gong",
       "Chris Hawblitzel",
       "Shuvendu Lahiri",
       "Jacob R. Lorch",
       "Shuai Lu",
       "Fan Yang",
       "Ziqiao Zhou",
       "Shan Lu"
     ],
     "year": 2024,
     "venue": "Proc. ACM Program. Lang. (OOPSLA)",
     "arxiv_id": "2409.13082",
     "doi": "10.1145/3763174"
   },
   "checklist": {
     "artifacts": {
       "code_released": {
         "applies": true,
         "answer": true,
         "justification": "The Data-Availability Statement says 'The code and artifact of AutoVerus are available at microsoft/verus-proof-synthesis.' This is a GitHub repository URL."
       },
       "data_released": {
         "applies": true,
         "answer": true,
         "justification": "Verus-Bench, the benchmark suite of 150 proof tasks, is part of the released artifact at microsoft/verus-proof-synthesis. The benchmark was curated from public sources (Diffy, MBPP-DFY-153, CloverBench)."
       },
       "environment_specified": {
         "applies": true,
         "answer": true,
         "justification": "Section 6.2.1 specifies hardware (Ubuntu 22.04.1 LTS, 24-core CPUs, 64 GB RAM) and the default model (GPT-4o version 2024-05-13). The tool is a Python CLI using Azure OpenAI APIs. The released artifact would contain environment details, though the paper itself does not list a requirements.txt explicitly."
       },
       "reproduction_instructions": {
         "applies": true,
         "answer": true,
         "justification": "The paper provides a Data-Availability Statement pointing to the repository microsoft/verus-proof-synthesis. The tool is described as 'a command line Python tool' (Section 5), and the evaluation methodology is described in sufficient detail in Section 6 for reproduction. The released artifact at the repository provides instructions."
       }
     },
     "statistical_methodology": {
       "confidence_intervals_or_error_bars": {
         "applies": true,
         "answer": false,
         "justification": "No confidence intervals or error bars are reported. Results are given as counts (e.g., 137/150 tasks proved) without uncertainty quantification. The paper acknowledges LLM randomness but does not report CIs across the 3 runs."
       },
       "significance_tests": {
         "applies": true,
         "answer": false,
         "justification": "No statistical significance tests are used despite comparative claims between AutoVerus and the baseline (137 vs 67 tasks) and across model variants. The comparisons rely solely on raw count differences."
       },
       "effect_sizes_reported": {
         "applies": true,
         "answer": true,
         "justification": "The paper reports concrete effect sizes with baseline context: AutoVerus proves 137/150 (91.3%) vs baseline 67/150 (44.7%). Per-phase breakdowns are given (78, 22, 37 tasks). Cost is $37 total. Time comparisons show AutoVerus needs 22 seconds per task vs 458 seconds for baseline to reach the same number of proved tasks."
       },
       "sample_size_justified": {
         "applies": true,
         "answer": false,
         "justification": "The benchmark size of 150 tasks is not formally justified. Section 6.1 describes how tasks were selected from existing benchmarks but does not justify whether 150 is sufficient for the claims being made. The ablation study uses a 30-task subset without power analysis."
       },
       "variance_reported": {
         "applies": true,
         "answer": false,
         "justification": "The paper states results are reported 'after running AutoVerus for three times' (Section 6.2.3) and mentions 122 tasks proved on the first attempt, 10 on the second, 5 on the third. However, no standard deviation or variance across these three runs is reported. The 30-task ablation with different models also reports single aggregate numbers."
       }
     },
     "evaluation_design": {
       "baselines_included": {
         "applies": true,
         "answer": true,
         "justification": "A baseline of repeatedly invoking GPT-4o with a comprehensive prompt is included (Section 6.2.2). The baseline was deliberately made competitive: same temperature, same multi-output setting, and even given an unfair advantage of including answers to 4 tasks as examples."
       },
       "baselines_contemporary": {
         "applies": true,
         "answer": false,
         "justification": "The baseline is a custom repeated-prompting scheme, not a comparison against published state-of-the-art tools. While related work mentions Loopy, Laurel, DafnyBench, and others, none are directly compared experimentally. The paper argues these tools target different languages/tasks, but no head-to-head comparison with any existing LLM-for-proof system is conducted."
       },
       "ablation_study": {
         "applies": true,
         "answer": true,
         "justification": "Extensive ablation studies are presented in Section 7.4: Phase-1/2 ablations (Table 4) test few-shot example removal, phase fusion, and ranking disabling. Phase-3 ablation compares specialized repair agents vs a generic debugging agent. LLM choice and temperature ablations are in Table 5."
       },
       "multiple_metrics": {
         "applies": true,
         "answer": true,
         "justification": "Multiple metrics are reported: number of correctly verified tasks, time cost (seconds), number of LLM calls, per-phase breakdown of proved tasks, repair agent success rates, token consumption, and monetary cost ($37)."
       },
       "human_evaluation": {
         "applies": false,
         "answer": false,
         "justification": "Human evaluation is not applicable here. Verus formal verification provides a mathematically rigorous correctness check -- proofs either pass or fail verification. This is a stronger guarantee than human evaluation."
       },
       "held_out_test_set": {
         "applies": true,
         "answer": true,
         "justification": "Section 6.1 explicitly states the team designing AutoVerus did not overlap with the team setting up the majority of Verus-Bench (all MBPP and CloverBench tasks). The few-shot examples used in AutoVerus agents have no overlap with Verus-Bench. The 3 Misc tasks with potential leakage from Verus Tutorial are explicitly discussed in Section 8."
       },
       "per_category_breakdown": {
         "applies": true,
         "answer": true,
         "justification": "Table 2 breaks down results by benchmark source (CloverBench, Diffy, MBPP, Misc) and by phase. Table 3 provides per-agent statistics. Figure 11 breaks down repair agent invocations by LLM model. Table 4 and 5 provide detailed ablation breakdowns."
       },
       "failure_cases_discussed": {
         "applies": true,
         "answer": true,
         "justification": "Section 7.5 ('Failed cases') categorizes the 13 failed tasks into three types: arithmetic overflow difficulties (6 tasks), insufficient knowledge of vstd library (5 tasks), and complicated logic (2 tasks). Specific task examples (MBPP-170, Misc-deduplicate, MBPP-755) are discussed with detailed explanations."
       },
       "negative_results_reported": {
         "applies": true,
         "answer": true,
         "justification": "The paper reports that the fused Phase-1/2 design performs worse than separate agents (7 fewer tasks proved, Table 4). The generic debugging agent proves only 17/37 tasks vs AutoVerus's specialized agents. GPT-3.5-turbo proves only 18/30 tasks. Lower temperatures reduce performance."
       }
     },
     "claims_and_evidence": {
       "abstract_claims_supported": {
         "applies": true,
         "answer": true,
         "justification": "The abstract claims 'more than 90% of them' proved -- Table 2 shows 137/150 = 91.3%. The abstract claims 'more than half of them tackled in less than 30 seconds or 3 LLM calls' -- Section 7.2 and Figure 8 support this. All abstract claims are backed by specific results."
       },
       "causal_claims_justified": {
         "applies": true,
         "answer": true,
         "justification": "Causal claims are made through ablation studies: removing components (few-shot examples, ranking, individual phases) and measuring the effect on proved tasks. These are controlled single-variable manipulations. The ablation design in Tables 4 and 5 provides adequate evidence for 'component X contributes to performance' claims."
       },
       "generalization_bounded": {
         "applies": true,
         "answer": true,
         "justification": "Section 8 explicitly discusses three key limitations for scaling: code dependencies in large systems, specification complexity, and more diverse proof problems. The paper states 'it is still just a collection of 150 tasks. It cannot represent many real-world proof tasks in large system code.' The title specifies 'Rust Code' and the work is clearly scoped to Verus."
       },
       "alternative_explanations_discussed": {
         "applies": true,
         "answer": true,
         "justification": "Section 8 discusses data leakage as an alternative explanation for good performance (LLMs may have seen proof tasks in training data) and provides evidence against it: the baseline LLM cannot prove the 3 potentially leaked tasks, and AutoVerus's proof differs from the online tutorial version. LLM randomness is acknowledged."
       }
     },
     "setup_transparency": {
       "model_versions_specified": {
         "applies": true,
         "answer": true,
         "justification": "Section 6.2.1 specifies 'GPT-4o (model version 2024-05-13).' Section 8 also mentions 'earlier GPT-4o models (with 2024-02-15 and 2024-05-13 versions).' GPT-4-turbo, GPT-3.5-turbo, and Deepseek-R1-32B are also named. The GPT-4o version with specific date qualifies."
       },
       "prompts_provided": {
         "applies": true,
         "answer": false,
         "justification": "The paper describes prompt content in natural language (e.g., 'we ask it to add loop invariants to the given Rust code' in Section 4.1.1, repair strategy instructions in Sections 4.2 and 4.3) but does not provide the actual prompt text used. The few-shot examples are described ('three toy Verus examples') but not shown in full. The released code may contain prompts, but the paper itself does not."
       },
       "hyperparameters_reported": {
         "applies": true,
         "answer": true,
         "justification": "Temperature is set to 1.0 (Section 6.2.2, with ablation at 0.1, 0.4, 0.7 in Table 5). Multi-output is set to 5 for Phase 1 and repair agents (3 otherwise). Maximum debugging iterations is 10 (Section 4.3.2). Threshold for complex assert-repair agent is 3 attempts. These are clearly reported."
       },
       "scaffolding_described": {
         "applies": true,
         "answer": true,
         "justification": "The agentic scaffolding is described in extensive detail: three-phase workflow (Generation, Refinement, Debugging) in Section 4 with Algorithms 1-3, agent composition, error selection priority, repair acceptance criteria, Lynette for safety checking and merging, Houdini algorithm integration. The agent network is shown in Figure 2 and repair agent list in Figure 6."
       },
       "data_preprocessing_documented": {
         "applies": true,
         "answer": true,
         "justification": "Section 6.1 documents the benchmark construction: 153 MBPP-DFY problems -> 67 trivial removed, 8 untranslatable -> 78 included. CloverBench: 60 -> 39 translated -> 3 incompatible, 4 weak, 21 trivial -> 11 included. Diffy: 69 -> 31 non-linear removed -> 38 included. 23 Misc from tutorials. Filtering criteria and counts are explicit."
       }
     },
     "limitations_and_scope": {
       "limitations_section_present": {
         "applies": true,
         "answer": true,
         "justification": "Section 8 is titled 'Discussion & Threats to Validity' and provides substantive discussion of general threats, data leakage, and scaling challenges."
       },
       "threats_to_validity_specific": {
         "applies": true,
         "answer": true,
         "justification": "Section 8 discusses specific threats: the benchmark is only 150 tasks and cannot represent real-world system code; authors who designed AutoVerus were familiar with some Diffy and Misc tasks; three specific tasks may have data leakage from the Verus Tutorial; evaluation does not cover newest Rust features like iterators."
       },
       "scope_boundaries_stated": {
         "applies": true,
         "answer": true,
         "justification": "Section 8 ('How to scale up?') explicitly states three things the results do NOT show: handling complex code dependencies in large systems, generating specifications (only proof annotations), and handling the diversity of proof problems in real verified systems. The paper also states 'a single Rust function is the unit of proof generation' (Section 4 footnote)."
       }
     },
     "data_integrity": {
       "raw_data_available": {
         "applies": true,
         "answer": true,
         "justification": "The Verus-Bench benchmark suite and AutoVerus code are released at microsoft/verus-proof-synthesis. Since Verus verification is deterministic (given the proof, verification either passes or fails), the raw data can be independently verified."
       },
       "data_collection_described": {
         "applies": true,
         "answer": true,
         "justification": "Section 6.1 describes in detail how each benchmark source was collected and translated: MBPP-DFY-153 from Dafny, CloverBench from Dafny/Verus, Diffy from C, and Misc from Verus tutorials/libraries. Selection criteria and exclusion reasons are documented."
       },
       "recruitment_methods_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants are involved. The benchmark is constructed from existing public benchmark suites."
       },
       "data_pipeline_documented": {
         "applies": true,
         "answer": true,
         "justification": "The pipeline from source benchmarks to Verus-Bench is documented: translation from Dafny/C to Rust/Verus, filtering of trivial tasks (88 rejected), filtering of untranslatable tasks (8 rejected), manual inspection of CloverBench translations. Section 6.1 provides counts at each stage."
       }
     },
     "conflicts_of_interest": {
       "funding_disclosed": {
         "applies": true,
         "answer": false,
         "justification": "No funding statement is provided. The Acknowledgment section only mentions 'anonymous reviewers.' Given that 8 of 13 authors are affiliated with Microsoft Research and the tool uses Azure OpenAI APIs, funding should be disclosed."
       },
       "affiliations_disclosed": {
         "applies": true,
         "answer": true,
         "justification": "Author affiliations are clearly listed: 8 authors are at Microsoft Research (including Microsoft Research Asia), and others are at various universities. The Microsoft connection is transparent."
       },
       "funder_independent_of_outcome": {
         "applies": true,
         "answer": false,
         "justification": "Microsoft Research employees evaluate a tool built using Microsoft's Azure OpenAI APIs, for Microsoft's Verus verification tool. Microsoft has a commercial interest in demonstrating the value of its AI and verification tools. The funder is not independent of the outcome."
       },
       "financial_interests_declared": {
         "applies": true,
         "answer": false,
         "justification": "No competing interests statement is present in the paper. Given Microsoft's commercial interests in AI tools and Verus, a declaration should be included."
       }
     },
     "contamination": {
       "training_cutoff_stated": {
         "applies": true,
         "answer": true,
         "justification": "Section 8 discusses data leakage and mentions 'earlier GPT-4o models (with 2024-02-15 and 2024-05-13 versions), predating the widespread public availability of CloverBench.' While not stating an exact training cutoff date, the paper reasons about the temporal relationship between model versions and benchmark availability."
       },
       "train_test_overlap_discussed": {
         "applies": true,
         "answer": true,
         "justification": "Section 8 ('Data leakage') extensively discusses potential train/test overlap. It analyzes which Verus-Bench sources were publicly available before model training: Diffy and MBPP proofs were never public, CloverBench was released after the GPT-4o training cutoff, and only 3 Misc tasks had potential leakage from the Verus Tutorial."
       },
       "benchmark_contamination_addressed": {
         "applies": true,
         "answer": true,
         "justification": "Section 8 provides a two-pronged argument: (1) the scarcity of Verus resources online (fewer than 10 GitHub projects) means training data is minimal, and (2) the baseline GPT-4o cannot prove the 3 potentially leaked tasks without AutoVerus, suggesting LLMs did not memorize them. AutoVerus's proof differs from the tutorial version."
       }
     },
     "human_studies": {
       "pre_registered": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in the study."
       },
       "irb_or_ethics_approval": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in the study."
       },
       "demographics_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in the study."
       },
       "inclusion_exclusion_criteria": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in the study."
       },
       "randomization_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in the study."
       },
       "blinding_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in the study."
       },
       "attrition_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in the study."
       }
     },
     "cost_and_practicality": {
       "inference_cost_reported": {
         "applies": true,
         "answer": true,
         "justification": "Section 7.1 reports: 'This entire process consumed 3 million input and 1.5 million output tokens. Based on the Azure GPT-4o pricing... the total cost for the benchmark suite was approximately $37.' Average 8.8 LLM calls per task. Time costs are shown in Figure 8a (per-task time budgets)."
       },
       "compute_budget_stated": {
         "applies": true,
         "answer": true,
         "justification": "Total cost of $37 for the benchmark suite is stated. Hardware is specified (Ubuntu 22.04.1, 24-core CPUs, 64 GB RAM). Average time per task is reported (70.0 seconds for GPT-4o, 229.8 seconds for GPT-4-turbo). Token consumption is quantified."
       }
     }
   },
   "claims": [
     {
       "claim": "AutoVerus can automatically generate correct proof for more than 90% of the 150 Verus-Bench tasks.",
       "evidence": "Table 2 shows 137 out of 150 tasks (91.3%) proved. Results are from running AutoVerus up to 3 times per task (Section 7.1).",
       "supported": "strong"
     },
     {
       "claim": "AutoVerus proves roughly twice as many tasks as a competitive baseline under the same time and LLM-call budget.",
       "evidence": "Table 2 shows 137 vs 67 tasks. Figure 8 shows AutoVerus consistently proves about 2x more tasks at every budget level. The baseline had 10 minutes per task and included answer examples for 4 tasks (Section 7.2).",
       "supported": "strong"
     },
     {
       "claim": "With a tight budget of 30 seconds or 3 LLM calls, AutoVerus can prove more than half of the Verus-Bench tasks.",
       "evidence": "Section 7.2 states: 'if we give each task only 30 seconds, AutoVerus can generate correct proof for 81 tasks.' Figure 8 confirms this for both time and LLM-call budgets.",
       "supported": "strong"
     },
     {
       "claim": "The AutoVerus framework works well with different LLM models (GPT-4o, GPT-4-turbo, Deepseek-R1).",
       "evidence": "Table 5 shows GPT-4o and GPT-4-turbo both prove 26/30 tasks, Deepseek-R1 proves 23/30. However, GPT-4-turbo takes 229.8s vs 70.0s per task (Section 7.4.3).",
       "supported": "moderate"
     },
     {
       "claim": "Each phase of AutoVerus contributes meaningfully to the overall performance.",
       "evidence": "Table 2: Phase-1 proves 78, Phase-2 adds 22, Phase-3 adds 37. Ablation in Table 4 shows fusion of phases hurts (7 fewer tasks). Section 7.4.2 shows generic debugging agent proves only 17/37 tasks vs specialized agents.",
       "supported": "strong"
     },
     {
       "claim": "Merging proof candidates from multiple LLM outputs improves proof success.",
       "evidence": "Section 7.3.1: 'For 14 tasks, although none of the direct output of the Phase-1 agent is correct, merging some of them immediately provides correct proof.' Example in Figure 5.",
       "supported": "strong"
     }
   ],
   "methodology_tags": [
     "benchmark-eval"
   ],
   "key_findings": "AutoVerus, a multi-agent LLM system for automated proof generation in Verus (a Rust verification tool), successfully proves 137 of 150 benchmark tasks (91.3%), compared to 67 (44.7%) by a competitive baseline of repeatedly prompting GPT-4o. The system achieves this through a three-phase approach: preliminary proof generation, generic refinement, and error-driven debugging, each using specialized LLM agents. The tool is efficient, proving over half the tasks in under 30 seconds at a total cost of $37 for the full benchmark suite, and the framework generalizes across different LLM models.",
   "red_flags": [
     {
       "flag": "Corporate self-evaluation",
       "detail": "8 of 13 authors are Microsoft Research employees. AutoVerus uses Azure OpenAI APIs and targets Verus, which was developed by Microsoft Research. The paper essentially evaluates Microsoft tools using Microsoft infrastructure. No competing interests statement is provided."
     },
     {
       "flag": "Weak baseline design",
       "detail": "The sole baseline is a custom repeated-prompting scheme rather than any existing published tool for LLM-based proof generation (e.g., Loopy, DafnyBench). While the paper argues these target different languages, the absence of any head-to-head comparison with published systems makes it difficult to contextualize the results."
     },
     {
       "flag": "No variance across runs",
       "detail": "Despite acknowledging LLM randomness, the paper reports results from 3 runs without reporting variance or standard deviation. The claim of '137 tasks' appears to be a maximum across runs rather than an average with uncertainty bounds."
     },
     {
       "flag": "Partial benchmark designer overlap",
       "detail": "Section 8 acknowledges that 'the authors who participated in the design of AutoVerus are already familiar with some of the tasks in the Diffy benchmark and in the Misc set,' creating a potential for unintentional tuning to these tasks."
     }
   ],
   "cited_papers": [
     {
       "title": "Towards AI-Assisted Synthesis of Verified Dafny Methods",
       "authors": ["Md Rakib Hossain Misu", "Cristina V. Lopes", "Iris Ma", "James Noble"],
       "year": 2024,
       "doi": "10.1145/3643763",
       "relevance": "Evaluates LLM capability for generating verified code in Dafny, directly relevant to GenAI for formal verification."
     },
     {
       "title": "DafnyBench: A Benchmark for Formal Software Verification",
       "authors": ["Chloe Loughridge", "Qinyi Sun", "Seth Ahrenbach"],
       "year": 2024,
       "arxiv_id": "2406.08467",
       "relevance": "Creates a benchmark for LLM-based proof synthesis in Dafny, comparable evaluation methodology to AutoVerus."
     },
     {
       "title": "Clover: Closed-Loop Verifiable Code Generation",
       "authors": ["Chuyue Sun", "Ying Sheng", "Oded Padon", "Clark W. Barrett"],
       "year": 2024,
       "relevance": "LLM-based system for generating verified Dafny programs from natural language, one of the benchmark sources for Verus-Bench."
     },
     {
       "title": "LeanDojo: Theorem Proving with Retrieval-Augmented Language Models",
       "authors": ["Kaiyu Yang", "Aidan M. Swope", "Alex Gu"],
       "year": 2023,
       "relevance": "Uses LLMs with retrieval augmentation for theorem proving in LEAN, relevant to AI-assisted formal verification."
     },
     {
       "title": "Baldur: Whole-Proof Generation and Repair with Large Language Models",
       "authors": ["Emily First", "Markus N. Rabe", "Talia Ringer", "Yuriy Brun"],
       "year": 2023,
       "doi": "10.1145/3611643.3616243",
       "relevance": "LLM-based proof generation and repair for Isabelle, directly comparable approach to AutoVerus for a different verification framework."
     },
     {
       "title": "Finding Inductive Loop Invariants using Large Language Models",
       "authors": ["Adharsh Kamath", "Aditya Senthilnathan", "Saikat Chakraborty"],
       "year": 2023,
       "arxiv_id": "2311.07948",
       "relevance": "Uses LLMs and Houdini algorithm for loop invariant generation in C programs (Loopy), shares core techniques with AutoVerus."
     },
     {
       "title": "Lemur: Integrating Large Language Models in Automated Program Verification",
       "authors": ["Haoze Wu", "Clark W. Barrett", "Nina Narodytska"],
       "year": 2024,
       "relevance": "Integrates LLMs with automated reasoning for program verification, similar high-level approach to combining AI with formal methods."
     },
     {
       "title": "Evaluating large language models trained on code",
       "authors": ["Mark Chen", "Jerry Tworek", "Heewoo Jun"],
       "year": 2021,
       "arxiv_id": "2107.03374",
       "relevance": "Foundational evaluation of LLMs for code generation (Codex/HumanEval), relevant to the broader LLM code generation evaluation landscape."
     },
     {
       "title": "Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation",
       "authors": ["Jiawei Liu", "Chunqiu Steven Xia", "Yuyao Wang", "Lingming Zhang"],
       "year": 2023,
       "relevance": "Questions reliability of LLM-generated code, motivating the need for formal verification of AI-generated code."
     },
     {
       "title": "Keep the Conversation Going: Fixing 162 out of 337 bugs for $0.42 each using ChatGPT",
       "authors": ["Chunqiu Steven Xia", "Lingming Zhang"],
       "year": 2023,
       "arxiv_id": "2304.00385",
       "relevance": "Evaluates LLM-based automated program repair with cost analysis, relevant to AI-assisted software engineering evaluation methodology."
     },
     {
       "title": "Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming",
       "authors": ["Saikat Chakraborty", "Gabriel Ebner", "Siddharth Bhat"],
       "year": 2024,
       "arxiv_id": "2405.01787",
       "relevance": "Uses LLMs for proof generation in F*, another proof-oriented language, directly relevant to GenAI for formal verification."
     },
     {
       "title": "Laurel: Generating Dafny Assertions Using Large Language Models",
       "authors": ["Eric Mugnier", "Emmanuel Anaya Gonzalez", "Ranjit Jhala"],
       "year": 2024,
       "arxiv_id": "2405.16792",
       "relevance": "LLM-based assertion generation for Dafny verification, related approach to AutoVerus's assertion repair agents."
     }
   ]
 }