### Install Verus and Dependencies for Local Setup

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README.md

These commands guide the local installation of Verus, including checking out a specific commit, downloading Z3, and building the Verus compiler. It also includes installing the Verus formatter.

```bash
git clone https://github.com/verus-lang/verus.git
cd verus
git checkout 33269ac6a0ea33a08109eefe5016c1fdd0ce9fbd
./tools/get-z3.sh && source tools/activate
vargo build --release

cargo install verusfmt  # Verus formatter
```

--------------------------------

### Build and Run Docker Container for AutoVerus

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README.md

These commands demonstrate how to build the AutoVerus Docker image and then run it interactively. This is the recommended way to start using the project, ensuring a consistent environment.

```bash
docker build -t autoverus .
docker run -it autoverus
```

--------------------------------

### Clone Repository and Install Python Dependencies

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README.md

This section details the steps for cloning the AutoVerus repository locally and installing the necessary Python packages using pip. It also includes setting the OpenAI API key.

```bash
# Clone repository
git clone https://github.com/microsoft/verus-proof-synthesis.git
cd verus-proof-synthesis

# Install Python dependencies  
pip install -r requirements.txt

# Set API key
export OPENAI_API_KEY=<your-openai-api-key>
```

--------------------------------

### Install Verus Formatter

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

Installs the Verus formatter using Cargo, a package manager for Rust.

```bash
cargo install verusfmt
```

--------------------------------

### Clone Project and Install Python Dependencies

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

This snippet covers cloning the project repository and installing its Python dependencies using pip.

```bash
git clone <repository-url>
cd verus-proof-synthesis
pip install -r requirements.txt
```

--------------------------------

### Dockerfile for AutoVerus Environment

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This Dockerfile sets up a build environment for AutoVerus. It installs Rust, clones and builds Verus from a specific commit, installs Python dependencies, and sets up the project's working directory.

```dockerfile
# Dockerfile structure (from project root)
FROM rust:latest

# Install Verus at specific commit
RUN git clone https://github.com/verus-lang/verus.git && \
    cd verus && \
    git checkout 33269ac6a0ea33a08109eefe5016c1fdd0ce9fbd && \
    ./tools/get-z3.sh && \
    source tools/activate && \
    vargo build --release

# Install Python dependencies
COPY requirements.txt .
RUN pip install -r requirements.txt

# Install verusfmt
RUN cargo install verusfmt

WORKDIR /home/appuser/verus-proof-synthesis
COPY . .

CMD ["/bin/bash"]
```

--------------------------------

### Ablation Study: Few-shot Example Impact (Bash)

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

Tests the impact of removing different few-shot examples from the first phase of the two-phase approach. This helps understand the contribution of each few-shot example.

```bash
python verify.py --name few-shot-ab-inference-without-3 --phase1-examples 6 7 --repair-num 0
python verify.py --name few-shot-ab-inference-without-6 --phase1-examples 3 7 --repair-num 0  
python verify.py --name few-shot-ab-inference-without-7 --phase1-examples 3 6 --repair-num 0
```

--------------------------------

### Docker Build Failure Example

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

An example of an error message indicating a failure during the Docker build process, often related to package installation.

```text
Error: Package installation failed
```

--------------------------------

### Run AutoVerus Proof Synthesis Locally

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README.md

This command executes the main Python script for proof synthesis after local setup. It requires specifying the input Rust file, output file for generated proofs, and a configuration file.

```bash
cd code
python main.py --input <input_file.rs> --output <output_file.rs> --config <config_file.json>
```

--------------------------------

### Verus Path Not Found Error Example

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

An example of an error message indicating that the Verus binary was not found.

```text
Error: Verus binary not found
```

--------------------------------

### Configure AutoVerus with OpenAI Credentials

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Sets up API credentials and paths for AutoVerus when using OpenAI. It specifies models, API endpoints, and local paths for Verus executables and example data. This configuration is loaded and parsed into an AttrDict for easy access.

```json
{
  "use_openai": true,
  "aoai_api_base": ["https://api.openai.com/v1/"],
  "aoai_api_version": "2024-12-01-preview",
  "aoai_api_key": [],
  "aoai_max_retries": 5,
  "max_token": 4096,
  "aoai_generation_model": "gpt-4o",
  "aoai_debug_model": "gpt-4o",
  "verus_path": "/home/user/verus/source/target-verus/release/verus",
  "example_path": "/home/user/verus-proof-synthesis/code/examples",
  "lemma_path": "/home/user/verus-proof-synthesis/code/lemmas",
  "util_path": "/home/user/verus-proof-synthesis/utils"
}
```

--------------------------------

### OpenAI API Rate Limit Error Example

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

An example of an error message indicating that the OpenAI API rate limit has been exceeded.

```text
Error: OpenAI API rate limit exceeded
```

--------------------------------

### Out of Memory Error Example

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

An example of an error message indicating that the system ran out of memory during proof generation.

```text
Error: Out of memory during proof generation
```

--------------------------------

### Configure AutoVerus with Azure OpenAI Credentials

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Sets up API credentials and paths for AutoVerus when using Azure OpenAI. It specifies models, API endpoints, and local paths for Verus executables and example data. This configuration is loaded and parsed into an AttrDict for easy access.

```json
// Azure OpenAI configuration (config-artifact-azure.json)
{
  "use_openai": false,
  "aoai_api_base": [
    "https://your-resource.openai.azure.com/"
  ],
  "aoai_api_version": "2024-05-01-preview",
  "aoai_api_key": ["your-azure-api-key"],
  "aoai_max_retries": 5,
  "max_token": 2048,
  "aoai_generation_model": "gpt-4o",
  "aoai_debug_model": "gpt-4o",
  "verus_path": "/path/to/verus",
  "example_path": "/path/to/examples",
  "lemma_path": "/path/to/lemmas",
  "util_path": "/path/to/utils"
}
```

--------------------------------

### Perform Ablation Studies in Batch Experiments using Bash

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/code/README.md

These commands are for performing ablation studies within batch experiments. They utilize the `verify.py` script with various flags to isolate the impact of different components like the number of Phase-1 examples, repair uniformity, and direct repair.

```bash
python verify.py --name few-shot-ablation --phase1-examples 3 6 --repair-num 0
```

```bash
python verify.py --name repair-ablation --repair-uniform --direct-repair
```

--------------------------------

### Perform Phase Ablation Studies using Python

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/code/README.md

These commands are used for phase ablation studies in the proof synthesis pipeline. They allow for experimenting with different numbers of examples in Phase-1, merging phases, or disabling candidate ranking. These are advanced configurations for analyzing the contribution of each pipeline stage.

```python
python main.py --input problem.rs --phase1-examples 3 6  # Remove example 7
```

```python
python main.py --input problem.rs --phase-uniform        # Merge Phase-1 & Phase-2
```

```python
python main.py --input problem.rs --disable-ranking     # Disable candidate ranking
```

--------------------------------

### Repair Verus Code with Full Error-Guided Strategy

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Repairs Verus code using a full error-guided strategy by calling the ref.repair_veval function. It reads original code, attempts repair, and then evaluates the repaired code using VEval to get a final score. Dependencies include the 'ref' module and the 'VEval' class.

```python
original_code = open("input.rs").read()
repaired_code = ref.repair_veval(
    original_code,
    max_attempt=10,
    temp_dir=Path("repair-intermediate"),
    temp=1.0
)

# Check final result
veval = VEval(repaired_code, logger)
score = veval.eval_and_get_score()
print(f"Repair completed with score: {score}")
```

--------------------------------

### Set API Key and Run Sample Experiment with Python

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

This snippet demonstrates how to set the OpenAI API key as an environment variable and then execute a sample verification experiment using the `verify.py` script. It configures the experiment using a JSON file and targets sampled benchmarks.

```bash
cd /home/appuser/verus-proof-synthesis/code
export OPENAI_API_KEY=<your-openai-api-key>

# Quick test on sampled benchmarks
python verify.py --name gpt4o-ab-sampled --config-file config-artifact-openai.json
```

--------------------------------

### Build and Run Docker Container

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

These commands are used to build a Docker image for the AutoVerus project and then run an interactive container from that image. This is the initial step for setting up the environment to run the experiments.

```bash
docker build -t autoverus .
docker run -it autoverus /bin/bash
```

--------------------------------

### Clone Verus Repository and Build

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

This snippet shows how to clone the Verus repository, checkout a specific commit, set up the environment with Z3, and build the Verus binary.

```bash
git clone https://github.com/verus-lang/verus.git
cd verus
git checkout 33269ac6a0ea33a08109eefe5016c1fdd0ce9fbd
./tools/get-z3.sh && source tools/activate
vargo build --release
```

--------------------------------

### Run Batch Experiments on Benchmark Suite using Bash

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/code/README.md

This command initiates batch experiments on a specified benchmark suite. It uses the `verify.py` script, taking the benchmark suite name and a configuration file as input. This is essential for systematic evaluation across a collection of problems.

```bash
python verify.py --name gpt4o-mbpp --config-file config-artifact-openai.json
```

--------------------------------

### Load and Use Configuration in Python

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Demonstrates how to load configuration from a JSON file into a Python script using the `json` and `utils.AttrDict` modules. It also shows how to set the Verus path globally and access configuration values.

```python
# Loading and using configuration in Python code
import json
from utils import AttrDict

# Load configuration
config = json.load(open("config-artifact-openai.json"))
config = AttrDict(config)

# Set Verus path globally
from veval import verus
verus.set_verus_path(config.verus_path)

# Access configuration values
print(f"Using model: {config.aoai_generation_model}")
print(f"Max tokens: {config.max_token}")
print(f"Example path: {config.example_path}")
```

--------------------------------

### Build and Run AutoVerus Docker Container (Bash)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This bash script outlines the process for building the AutoVerus Docker image and running it. Inside the container, it shows how to set an API key, navigate to the code directory, and execute scripts for generating single proofs or running benchmark suites.

```bash
# Build and run Docker container
docker build -t autoverus .
docker run -it autoverus

# Inside container
export OPENAI_API_KEY=sk-your-key
cd code

# Generate single proof
python main.py \
  --input ../benchmarks/CloverBench/unverified/is_prime.rs \
  --output verified_is_prime.rs \
  --config config-artifact-openai.json

# Run benchmark suite
python verify.py \
  --name gpt4o-ab-sampled \
  --config-file config-artifact-openai.json

# Results in _output/ directory
ls -la _output/
```

--------------------------------

### Set OpenAI API Key and Run AutoVerus Scripts

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README.md

This snippet shows how to set the OpenAI API key as an environment variable and then execute the main proof generation script or the verification script for a benchmark suite. It requires specifying input/output files and configuration files.

```bash
export OPENAI_API_KEY=<your-openai-api-key>

# Generate proof for a single file
python main.py --input <input_file.rs> --output <output_file.rs> --config config-artifact-openai.json

# Run on benchmark suite (small sample: 30 tasks)
python verify.py --name gpt4o-ab-sampled --config-file config-artifact-openai.json
```

--------------------------------

### Basic Proof Generation (Bash)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This command demonstrates the basic usage of the AutoVerus CLI for single file proof synthesis. It requires setting the OpenAI API key and specifies input, output, and configuration files. The `--repair` flag indicates the number of repair attempts.

```bash
export OPENAI_API_KEY=sk-your-key-here
cd code
python main.py \
  --input ../benchmarks/CloverBench/unverified/binary_search.rs \
  --output verified_binary_search.rs \
  --config config-artifact-openai.json \
  --repair 10 \
  --temp 1.0
```

--------------------------------

### Test Different LLM Models (Bash)

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

Runs the verify.py script with specified names and configuration files to test the impact of different LLM models on the results. This helps in understanding model performance.

```bash
python verify.py --name gpt4turbo-ab-sampled --config-file config-artifact-openai.json
python verify.py --name gpt35-ab-sampled --config-file config-artifact-openai.json
```

--------------------------------

### Batch Verification Pipeline (Bash)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

These commands illustrate how to run the AutoVerus batch verification pipeline on benchmark suites. Options include specifying benchmark names, configuration files, temperature, and the number of repair attempts. Results are stored in an organized output directory.

```bash
# Run on sampled benchmark (30 tasks, recommended for testing)
cd code
python verify.py \
  --name gpt4o-ab-sampled \
  --config-file config-artifact-openai.json \
  --temp 1.0 \
  --repair-num 10

# Run on specific benchmark suites
python verify.py --name gpt4o-mbpp --config-file config.json
python verify.py --name gpt4o-diffy --config-file config.json
python verify.py --name gpt4o-clover --config-file config.json
python verify.py --name gpt4o-misc --config-file config.json

# Ablation study configurations
python verify.py \
  --name gpt4o-ablation \
  --config-file config.json \
  --repair-uniform \
  --phase-uniform \
  --disable-ranking \
  --disable-one-refinement 0 \
  --phase1-examples "3" "6"
```

--------------------------------

### Execute Single File Proof Generation with AutoVerus (Bash)

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/code/README.md

This command initiates the AutoVerus proof generation process for a single Rust file. It takes the input Rust code, specifies an output file for the generated proof, and uses a configuration file for settings. The process involves loading files, generating candidates, refining them, and iteratively repairing verification errors.

```bash
python main.py --input problem.rs --output solution.rs --config config.json
```

--------------------------------

### Generate Proof for Single File using Python

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/code/README.md

This command generates a proof for a single Rust file using the main Python script. It takes the input file path and specifies the output file path for the generated proof. No specific dependencies are mentioned beyond the Python script itself.

```python
python main.py --input array_sum.rs --output array_sum_proved.rs
```

--------------------------------

### Set OpenAI API Key

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

Sets the OpenAI API key as an environment variable for use by the project.

```bash
export OPENAI_API_KEY=<your-openai-api-key>
```

--------------------------------

### Run Baseline Comparison using Python

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/code/README.md

This command executes a baseline comparison for a given Rust problem file. It uses the main Python script, specifying input and output files, and includes a flag to indicate a baseline run. This is useful for evaluating the performance of different synthesis approaches.

```python
python main.py --input problem.rs --output solution.rs --is-baseline
```

--------------------------------

### AutoVerus Command for Verification

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This bash command demonstrates how to use the `main.py` script from AutoVerus to verify a Rust file. It specifies input, output, configuration, and various synthesis parameters like repair attempts, merging, and temperature.

```bash
python main.py \
  --input ../benchmarks/CloverBench/unverified/binary_search.rs \
  --output verified_binary_search.rs \
  --config config-artifact-openai.json \
  --repair 10 \
  --merge 5 \
  --temp 1.0
```

--------------------------------

### Test Different Temperature Settings (Bash)

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

Runs the verify.py script with specified names and temperature settings to evaluate the effect of temperature on LLM output. This is used for tuning generation parameters.

```bash
python verify.py --name temp-ab-sampled --temp 0.1 --config-file config-artifact-openai.json
python verify.py --name temp-ab-sampled --temp 0.4 --config-file config-artifact-openai.json  
python verify.py --name temp-ab-sampled --temp 0.7 --config-file config-artifact-openai.json
```

--------------------------------

### Run AutoVerus on Benchmark Suites (Bash)

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

Executes the AutoVerus script with specified names and configurations for different benchmark suites. It takes the model name and config file as input and is used for evaluating overall effectiveness.

```bash
python verify.py --name gpt4o-clover --config-file config-artifact-openai.json
python verify.py --name gpt4o-diffy --config-file config-artifact-openai.json
python verify.py --name gpt4o-mbpp --config-file config-artifact-openai.json
python verify.py --name gpt4o-misc --config-file config-artifact-openai.json
```

--------------------------------

### Ablation Study: Phase Fusion Analysis (Bash)

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

Compares merging Phase-1 and Phase-2 against keeping them separate. This examines the effectiveness of different phase interaction strategies.

```bash
python verify.py --name merge-inference-refinement-ab-inference --phase-uniform --repair-num 0
python verify.py --name merge-inference-refinement-ab-refinement --phase-uniform --repair-num 0
```

--------------------------------

### Run Baseline Approach on Benchmark Suites (Bash)

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

Executes the verify.py script for baseline comparisons on various benchmark suites. This command uses the --is-baseline flag to distinguish from AutoVerus runs and shows the benefit of the project's approach.

```bash
python verify.py --name baseline-clover-simple --is-baseline
python verify.py --name baseline-diffy-simple --is-baseline
python verify.py --name baseline-mbpp-simple --is-baseline
python verify.py --name baseline-misc-simple --is-baseline
```

--------------------------------

### Full Proof Generation Pipeline with Generation Class

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Executes the complete proof synthesis pipeline, including generating initial invariants and applying refinement agents. It takes input code, generates output code with proofs, evaluates the result using VEval, and writes the verified code to a file.

```python
from generation import Generation
from utils import AttrDict
import json
import logging

# Setup
logging.basicConfig(level=logging.INFO)
logger = logging.getLogger(__name__)
config = AttrDict(json.load(open("config.json")))

# Initialize generation engine
gen = Generation(
    config,
    logger,
    phase1_examples=["3", "6", "7"],  # Which examples to use for few-shot
    repair_uniform=False  # Use targeted repair strategies
)

# Read input code
input_code = open("input.rs").read()

# Generate proof with full pipeline (recommended)
from pathlib import Path
output_code = gen.generate_with_proof_func(
    input_code,
    with_inference=True,     # Generate initial invariants
    with_refine=True,        # Apply refinement agents
    merge_cand=5,            # Number of candidates to merge
    verbose=True,
    repair_steps=10,         # Maximum repair iterations
    temp=1.0,                # LLM temperature
    temp_dir=Path("output-intermediate-temp"),
    disable_ranking=False    # Use scoring to rank candidates
)

# Evaluate result
from veval import VEval
veval = VEval(output_code, logger)
score = veval.eval_and_get_score()
print(f"Verification result: {score}")  # (verified_count, error_count)

# Write output
with open("output.rs", "w") as f:
    f.write(output_code)
```

--------------------------------

### Configure LLM Model for Experiments (JSON)

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

Modifies the OpenAI artifact configuration file to specify a different LLM generation model. This is a prerequisite for testing different model choices.

```json
{
  "aoai_generation_model": "gpt-4-turbo"  // or "gpt-3.5-turbo"
}
```

--------------------------------

### Execute Batch Processing and Benchmarking with AutoVerus (Bash)

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/code/README.md

This command is used for batch processing of multiple Verus problems and for benchmarking the AutoVerus system. It specifies an experiment name and a configuration file. The process involves loading a benchmark suite, processing each problem through multiple iterations, and tracking success rates and timing statistics.

```bash
python verify.py --name experiment-name --config-file config.json
```

--------------------------------

### Ablation Study: All-in-one Repair (Bash)

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

Tests the all-in-one repair approach against targeted repair. This command is used to evaluate the effectiveness of different repair strategies.

```bash
python verify.py --name all-in-one-ab-repair --repair-uniform --direct-repair
```

--------------------------------

### Control LLM Temperature using Python

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/code/README.md

This command demonstrates controlling the temperature parameter for the Large Language Model (LLM) during proof synthesis. It uses the main Python script with input file path and the `--temp` flag to set the creativity level of the LLM. Higher temperatures lead to more diverse outputs.

```python
python main.py --input problem.rs --temp 0.7
```

--------------------------------

### Run Docker Container for Verus Synthesis

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This command mounts a local directory for persistent results and sets the OpenAI API key before running the AutoVerus Docker image. Inside the container, a Python script is executed to perform the verification.

```bash
docker run -it \
  -v $(pwd)/results:/home/appuser/results \
  -e OPENAI_API_API_KEY=$OPENAI_API_KEY \
  autoverus
```

```bash
# Inside container, output to mounted directory
python main.py \
  --input input.rs \
  --output /home/appuser/results/output.rs \
  --config config-artifact-openai.json
```

--------------------------------

### Ablation Study: Disabling Ranking Mechanism (Bash)

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README-artifact-evaluation.md

Tests the impact of disabling the ranking mechanism in the two-phase approach. This helps evaluate the importance of the ranking strategy.

```bash
python verify.py --name disable-ranking-ab-inference --disable-ranking --repair-num 0
python verify.py --name disable-ranking-ab-refinement --disable-ranking --repair-num 0
```

--------------------------------

### Advanced Proof Generation and Baseline Modes (Bash)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This showcases advanced AutoVerus CLI options including ablation studies and different operational modes like 'gen' (generation), 'baseline' (one-shot), and 'direct-repair'. It allows fine-tuning of refinement phases and disabling safety checks.

```bash
# Advanced usage with ablation options
python main.py \
  --input input.rs \
  --output output.rs \
  --config config.json \
  --mode gen \
  --repair 15 \
  --merge 5 \
  --temp 1.0 \
  --phase1-examples "3" "6" "7" \
  --disable-safe  # Only for debugging, skips safety checks

# Baseline mode (one-shot without refinement)
python main.py \
  --input input.rs \
  --output output.rs \
  --config config.json \
  --is-baseline

# Direct repair mode (skip inference, only repair)
python main.py \
  --input input.rs \
  --output output.rs \
  --config config.json \
  --direct-repair \
  --repair 20
```

--------------------------------

### AutoVerus Generated Files

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Lists the types of files generated by the AutoVerus verification process, including the final output, intermediate candidates, merged files, refinement attempts, and repair directories.

```bash
# Generated files:
# - verified_binary_search.rs (final output)
# - intermediate-binary_search/0-0.rs through 0-4.rs (initial candidates)
# - intermediate-binary_search/merged-0.rs through merged-4.rs
# - intermediate-binary_search/refine-0.rs through refine-3.rs
# - intermediate-binary_search/repair/ (repair attempts if needed)
# - intermediate-binary_search/final.rs (best result)
```

--------------------------------

### Targeted Repair for Specific Verus Assert/PostCond Failures

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Applies targeted repair strategies for specific Verus errors like PostCondFail and AssertFail. It evaluates buggy code, retrieves the first error, and routes it to the appropriate repair function using 'ref.repair_PostCondFail' or 'ref.repair_AssertFail'.

```python
# Targeted repair for specific Verus error
code = open("buggy.rs").read()
veval = VEval(code, logger)
veval.eval()
failures = veval.get_failures()

if failures:
    first_error = failures[0]

    # Route to appropriate repair strategy
    if first_error.error == VerusErrorType.PostCondFail:
        fixed = ref.repair_PostCondFail(code, first_error, num=3, temp=1.0)
        print("Applied postcondition repair strategy")

    elif first_error.error == VerusErrorType.AssertFail:
        fixed = ref.repair_AssertFail(code, first_error, num=3, temp=1.0)
        print("Applied assertion repair strategy")
```

--------------------------------

### Verus Binary Search (Unverified to Verified)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Compares the unverified input Rust code for a binary search function with the AutoVerus-generated verified output. The verified code includes loop invariants and assertions.

```rust
// Input: benchmarks/CloverBench/unverified/binary_search.rs
use vstd::prelude::*;

fn main() {}
verus! {

fn binary_search(v: &Vec<u64>, k: u64) -> (r: usize)
    requires
        forall|i: int, j: int| 0 <= i <= j < v.len() ==> v[i] <= v[j],
        exists|i: int| 0 <= i < v.len() && k == v[i],
    ensures
        r < v.len(),
        k == v[r as int],
{
    let mut i1: usize = 0;
    let mut i2: usize = v.len() - 1;
    while i1 != i2 {
        let ghost d = i2 - i1;
        let ix = i1 + (i2 - i1) / 2;
        if v[ix] < k {
            i1 = ix + 1;
        } else {
            i2 = ix;
        }
    }
    i1
}

} // verus!
```

```rust
// Output: AutoVerus generated verified code
use vstd::prelude::*;

fn main() {}
verus! {

fn binary_search(v: &Vec<u64>, k: u64) -> (r: usize)
    requires
        forall|i: int, j: int| 0 <= i <= j < v.len() ==> v[i] <= v[j],
        exists|i: int| 0 <= i < v.len() && k == v[i],
    ensures
        r < v.len(),
        k == v[r as int],
{
    let mut i1: usize = 0;
    let mut i2: usize = v.len() - 1;
    while i1 != i2
        invariant
            i2 < v.len(),
            exists|i: int| i1 <= i <= i2 && k == v[i],
            forall|i: int, j: int| 0 <= i <= j < v.len() ==> v[i] <= v[j],
    {
        let ghost d = i2 - i1;
        let ix = i1 + (i2 - i1) / 2;
        if v[ix] < k {
            i1 = ix + 1;
        } else {
            i2 = ix;
        }
        assert(i2 - i1 < d);
    }
    i1
}

} // verus!
// Score: (1, 0)
// Safe: true
```

--------------------------------

### Houdini: Merge Proof Candidates and Remove Failing Assertions

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Merges multiple proof candidates and removes failing assertions using the Houdini algorithm. It loads configuration, initializes Houdini, merges invariants from two code candidates, and evaluates the merged result. Dependencies include 'houdini', 'veval', 'utils', 'json', and 'logging'.

```python
# Houdini Candidate Merging
from houdini import houdini
from veval import VEval
from utils import AttrDict
import json
import logging

logger = logging.getLogger(__name__)
config = AttrDict(json.load(open("config.json")))
hdn = houdini(config)

# Merge two proof candidates
code1 = open("candidate1.rs").read()
code2 = open("candidate2.rs").read()

try:
    merged_code = hdn.merge_invariant(code1, code2)
    print("Successfully merged invariants from both candidates")

    # Evaluate merged result
    veval = VEval(merged_code, logger)
    score = veval.eval_and_get_score()
    print(f"Merged code score: {score}")

except Exception as e:
    print(f"Merge failed: {e}")
    merged_code = code1  # Fall back to first candidate
```

--------------------------------

### Check Proof Correctness (Python)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This Python function, intended for use with the `verify.py` script, checks if a generated proof in a Rust file is correct. It parses the file content to look for safety violations, invalid proof shortcuts like `assume()` or `admit()`, and verifies the success criteria of the proof score.

```python
from pathlib import Path
import re

def is_correct(code_file_path: Path) -> bool:
    text = code_file_path.read_text()

    # Check for safety violations
    if "safe: false" in text.lower():
        return False

    # Check for invalid proof shortcuts (except in special cases)
    if "havoc_inline_post" not in code_file_path.name:
        if "assume(" in text or "admit()" in text:
            return False

    # Parse verification score
    score = re.search(r"[Ss]core: \((\d+), (\d+)\)", text)
    if score:
        verified, errors = int(score.group(1)), int(score.group(2))
        return verified > 0 and errors == 0
    return False

# Usage
result_file = Path("_output/20250118-gpt4o-mbpp-1.0/1-task_id_18.rs")
if is_correct(result_file):
    print("Proof verified successfully!")
```

--------------------------------

### Direct Inference with Generation Class

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Performs direct inference using the Generation class to obtain preliminary invariants. It takes input code and generates multiple candidate invariant sets, each evaluated for their score.

```python
# Direct inference only (preliminary invariants)
candidates = gen.direct_inference(
    code=input_code,
    temp=1.0,
    answer_num=5  # Generate 5 candidates
)

for i, candidate_code in enumerate(candidates):
    print(f"Candidate {i}:")
    veval = VEval(candidate_code, logger)
    score = veval.eval_and_get_score()
    print(f"  Score: {score}")
```

--------------------------------

### Insert Pre-proved Lemmas into Verus Code (Python)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This Python function `insert_lemma_func` injects specified pre-proved lemmas into a Verus Rust program. It typically inserts them after the `verus!` declaration, enabling the program to utilize these lemmas.

```python
from utils import (
    code_change_is_safe,
    evaluate,
    clean_code,
    get_nonlinear_lines,
    insert_lemma_func
)
import logging

logger = logging.getLogger(__name__)
verus_path = "/home/user/verus/source/target-verus/release/verus"

code = open("program.rs").read()
lemma_names = ["arithmetic_lemma", "sequence_lemma"]
lemma_path = "/path/to/lemmas"

# Lemmas are inserted after verus! declaration
code_with_lemmas = insert_lemma_func(code, lemma_names, lemma_path)

# Now the program can call arithmetic_lemma() and sequence_lemma()
with open("program_with_lemmas.rs", "w") as f:
    f.write(code_with_lemmas)
```

--------------------------------

### Merge Candidates and Verify with Houdini (Python)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This Python script iteratively merges multiple Rust code candidates, evaluates their scores, and attempts to verify the merged code using Houdini. It includes error handling for merge failures.

```python
candidates = [
    open("candidate1.rs").read(),
    open("candidate2.rs").read(),
    open("candidate3.rs").read()
]

best_code = candidates[0]
best_score = VEval(best_code, logger).eval_and_get_score()

for i, cand in enumerate(candidates[1:], 1):
    try:
        merged = hdn.merge_invariant(best_code, cand)
        score = VEval(merged, logger).eval_and_get_score()

        if score > best_score:
            print(f"Candidate {i} improved score from {best_score} to {score}")
            best_code = merged
            best_score = score

        # Try Houdini on merged result
        failed_lines, hdn_code = hdn.run(merged)
        if len(failed_lines) == 0:
            print(f"Houdini succeeded after merging candidate {i}!")
            best_code = hdn_code
            break

    except Exception as e:
        print(f"Failed to merge candidate {i}: {e}")
        continue

print(f"Final best score: {best_score}")
```

--------------------------------

### Adjust Repair Rounds using Python

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/code/README.md

This command adjusts the number of repair rounds for the proof synthesis process. It utilizes the main Python script, taking input and output file paths, and allows specifying the number of repair rounds via the `--repair` flag. This helps in controlling the depth of automated repair.

```python
python main.py --input problem.rs --output solution.rs --repair 5
```

--------------------------------

### VEval: Verus Verification Evaluation and Error Parsing

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Executes the Verus verifier and parses structured error output using the VEval class. It evaluates code, retrieves verification scores, and accesses detailed failure information including error type, line number, text, and label. Dependencies include 'veval' and 'logging'.

```python
from veval import VEval, EvalScore, VerusErrorType
import logging

logger = logging.getLogger(__name__)
code = open("test.rs").read()

# Run Verus verification
veval = VEval(code, logger)
veval.eval()

# Get verification score
score = veval.eval_and_get_score()
print(f"Verified: {score.verified}, Errors: {score.errors}")

if score.is_correct():
    print("Proof is complete!")
elif score.compilation_error:
    print("Code has compilation errors")
else:
    print("Verification failed")

# Access detailed error information
failures = veval.get_failures()
for i, failure in enumerate(failures):
    print(f"\nError {i+1}:")
    print(f"  Type: {failure.error}")
    print(f"  Line: {failure.trace[0].lines[0]}")
    print(f"  Text: {failure.trace[0].get_text()}")
    print(f"  Label: {failure.trace[0].strlabel}")
```

--------------------------------

### Clean LLM Rust Code Output (Python)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This function `clean_code` is designed to extract raw Rust code from a larger string, typically an LLM response. It removes markdown formatting and any surrounding explanatory text, returning only the executable Rust code.

```python
from utils import (
    code_change_is_safe,
    evaluate,
    clean_code,
    get_nonlinear_lines,
    insert_lemma_func
)
import logging

logger = logging.getLogger(__name__)
verus_path = "/home/user/verus/source/target-verus/release/verus"

llm_response = """
Here's the verified code:

```rust
verus! {
fn example(x: usize) -> usize {
    requires x < 100
    ensures result < 101
{
    x + 1
}
}
```

This code is now verified!
"

cleaned = clean_code(llm_response)
# Returns only the Rust code without markdown or explanations
print(cleaned)
```

--------------------------------

### BibTeX Citation for Autoverus Paper

Source: https://github.com/microsoft/verus-proof-synthesis/blob/main/README.md

This snippet provides the BibTeX formatted citation for the 'Autoverus: Automated Proof Generation for Rust Code' paper. It includes details such as title, authors, journal, volume, number, year, and publisher, commonly used for academic referencing in LaTeX documents.

```bibtex
@article{autoverus,
  title={Autoverus: Automated Proof Generation for Rust Code},
  author={Chenyuan Yang and Xuheng Li and Md Rakib Hossain Misu and Jianan Yao and Weidong Cui and Yeyun Gong and Chris Hawblitzel and Shuvendu K. Lahiri and Jacob R. Lorch and Shuai Lu and Fan Yang and Ziqiao Zhou and Shan Lu},
  journal={Proceedings of the ACM on Programming Languages},
  volume={9},
  number={OOPSLA2},
  year={2025},
  publisher={ACM New York, NY, USA}
}
```

--------------------------------

### Error-Specific Repair Strategies for Verus Code

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Implements error-specific repair strategies for Verus code based on identified failures. It evaluates code, retrieves failures, and applies targeted repair functions like repair_PreCondFail and repair_ArithmeticFlow based on the error type. Requires 'VerusErrorType' and 'VEval' from 'veval'.

```python
# Error-specific repair strategies
from pathlib import Path

# Get Verus errors
veval = VEval(code, logger)
veval.eval()
failures = veval.get_failures()

# Process each error type
for error in failures:
    if error.error == VerusErrorType.InvFailEnd:
        print("Invariant fails at loop end")
        print(f"  Line: {error.trace[0].lines[0]}")
        print(f"  Text: {error.trace[0].get_text()}")

    elif error.error == VerusErrorType.PreCondFail:
        print("Precondition not satisfied")
        # Repair with precondition failure strategy
        repaired = ref.repair_PreCondFail(code, error, temp=1.0)

    elif error.error == VerusErrorType.ArithmeticFlow:
        print("Arithmetic overflow detected")
        # Add bounds checking
        repaired = ref.repair_ArithmeticFlow(code, error, temp=1.0)
```

--------------------------------

### Score Comparison and Repair Assessment with EvalScore

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Compares verification scores and assesses the quality of repairs using the EvalScore class. It allows for direct comparison of scores, checking if a verification succeeded, and determining if a repair improved the code. Requires 'EvalScore' from 'veval'.

```python
# Score comparison for ranking candidates
from veval import EvalScore

score1 = EvalScore(verified=1, errors=0, compilation_error=False)
score2 = EvalScore(verified=0, errors=2, compilation_error=False)
score3 = EvalScore(verified=0, errors=0, compilation_error=True)

# Compare scores
if score1 > score2:
    print("score1 is better")

if score1.is_correct():
    print("Verification succeeded!")

# Check if new score is a good repair
if score2.is_good_repair(score3):
    print("Repair improved the code")

# Get worst possible score
worst = EvalScore.get_worst_score()
```

--------------------------------

### Direct Verus Code Evaluation (Python)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This Python code directly evaluates a Rust program using the Verus verifier. It captures the verification score (verified proofs and errors) and the standard output/error from the Verus execution, allowing for programmatic assessment of verification results.

```python
from utils import (
    code_change_is_safe,
    evaluate,
    clean_code,
    get_nonlinear_lines,
    insert_lemma_func
)
import logging

logger = logging.getLogger(__name__)
verus_path = "/home/user/verus/source/target-verus/release/verus"

code = open("test.rs").read()
score, result = evaluate(code, verus_path, func_name="main")
verified, errors = score

print(f"Verified: {verified}, Errors: {errors}")
print("Verus stdout:", result.stdout)
print("Verus stderr:", result.stderr)

if verified > 0 and errors == 0:
    print("All proofs verified!")
```

--------------------------------

### Individual Refinement Agents with Generation Class

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Applies individual refinement agents from the Generation class to improve code by adding specific types of invariants. This includes constant propagation, array length, quantifier range, conditional loop invariants, and non-linear arithmetic assertions.

```python
# Individual refinement agents
from utils import clean_code

code = clean_code(input_code)

# Constant propagation: copy bounds from preconditions to invariants
refined_code = gen.constantrefine_inference(code, temp=1.0, answer_num=1)[0]

# Array length: add x.len() invariants for all arrays
refined_code = gen.arraylen_inference(code, temp=1.0, answer_num=1)[0]

# Quantifier range: ensure forall ranges cover full array
refined_code = gen.arrayrefine_inference(code, temp=1.0, answer_num=1)[0]

# Conditional invariants: add index > 0 ==> P for first-iteration cases
refined_code = gen.condlooprefine_inference(code, temp=1.0, answer_num=1)[0]

# Non-linear arithmetic assertions
refined_code = gen.nonlinear_inference(code, temp=1.0, answer_num=1)[0]
```

--------------------------------

### Run Houdini Algorithm to Remove Failing Invariants

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Applies the Houdini algorithm to remove failing invariants from Verus code that is over-annotated. This snippet sets up the context for running Houdini on code containing numerous invariants.

```python
# Run Houdini algorithm to remove failing invariants
code_with_many_invariants = open("over_annotated.rs").read()
```

--------------------------------

### Detect Non-linear Arithmetic Expressions (Python)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This Python snippet uses the `get_nonlinear_lines` utility to identify and report lines in a Rust program that contain non-linear arithmetic expressions. It's useful for flagging areas that might require special handling or annotations in Verus.

```python
from utils import (
    code_change_is_safe,
    evaluate,
    clean_code,
    get_nonlinear_lines,
    insert_lemma_func
)
import logging

logger = logging.getLogger(__name__)
verus_path = "/home/user/verus/source/target-verus/release/verus"

code = open("program.rs").read()
nl_lines = get_nonlinear_lines(code, logger)

if nl_lines:
    print("Non-linear arithmetic detected at:")
    for start, end, text in nl_lines:
        print(f"  Lines {start}-{end}: {text}")
    # Need to add nonlinear_arith annotations
else:
    print("No non-linear arithmetic found")
```

--------------------------------

### Remove Failing Assertions with Houdini (Python)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This snippet demonstrates how Houdini iteratively removes failing assertions from Rust code until a fixed point is reached. It checks if all remaining invariants verify and saves the cleaned code.

```python
failed_lines, cleaned_code = hdn.run(code_with_many_invariants, verbose=True)

if len(failed_lines) == 0:
    print("Houdini succeeded! All remaining invariants verify.")
    with open("houdini_output.rs", "w") as f:
        f.write(cleaned_code)
else:
    print(f"Houdini removed assertions but {len(failed_lines)} issues remain")
    print(f"Remaining error lines: {failed_lines}")
```

--------------------------------

### Check Code Change Safety with Verus (Python)

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

This Python utility checks if code modifications are safe, meaning only proofs were altered and not functional code. It uses the `code_change_is_safe` function, requiring original and modified code, and the path to the Verus executable.

```python
from utils import (
    code_change_is_safe,
    evaluate,
    clean_code,
    get_nonlinear_lines,
    insert_lemma_func
)
import logging

logger = logging.getLogger(__name__)
verus_path = "/home/user/verus/source/target-verus/release/verus"

# Check if code changes are safe (no functional changes)
original = open("original.rs").read()
modified = open("modified.rs").read()

is_safe = code_change_is_safe(
    original,
    modified,
    verus_path,
    logger,
    target_mode=True,  # Check only target function
    util_path="../utils"
)

if is_safe:
    print("Code changes are safe - only proofs modified")
else:
    print("WARNING: Functional code was changed!")
```

--------------------------------

### Filtering Verus Errors by Type and Location

Source: https://context7.com/microsoft/verus-proof-synthesis/llms.txt

Filters Verus verification errors based on type and location using the VEval class. It can identify specific error categories like invariant failures or user-defined errors and extract relevant line numbers for further processing. Requires 'VEval' and 'VerusErrorType'.

```python
# Filter errors by type and location
veval = VEval(code, logger)
veval.eval()
failures = veval.get_failures()

# Find all invariant failures
inv_failures = [f for f in failures
                if f.error in [VerusErrorType.InvFailEnd,
                              VerusErrorType.InvFailFront]]

# Find errors not in standard library
user_errors = [f for f in failures if not f.trace[0].is_vstd_err()]

# Get error lines for Houdini removal
error_lines = []
for f in inv_failures:
    error_lines.append(f.trace[0].lines[0])
print(f"Lines with failing invariants: {error_lines}")
```