Instructions to use YuechunSun/TopoVerus-32B with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use YuechunSun/TopoVerus-32B with Transformers:

# Use a pipeline as a high-level helper
from transformers import pipeline

pipe = pipeline("text-generation", model="YuechunSun/TopoVerus-32B")
messages = [
    {"role": "user", "content": "Who are you?"},
]
pipe(messages)

# pip install -U transformers accelerate
# Load model directly
from transformers import AutoTokenizer, AutoModelForCausalLM

tokenizer = AutoTokenizer.from_pretrained("YuechunSun/TopoVerus-32B")
model = AutoModelForCausalLM.from_pretrained("YuechunSun/TopoVerus-32B", device_map="auto")
messages = [
    {"role": "user", "content": "Who are you?"},
]
inputs = tokenizer.apply_chat_template(
	messages,
	add_generation_prompt=True,
	tokenize=True,
	return_dict=True,
	return_tensors="pt",
).to(model.device)

outputs = model.generate(**inputs, max_new_tokens=256)
print(tokenizer.decode(outputs[0][inputs["input_ids"].shape[-1]:]))

Notebooks
Google Colab
Kaggle
Local Apps Settings

vLLM

How to use YuechunSun/TopoVerus-32B with vLLM:

Install from pip and serve model

# Install vLLM from pip:
pip install vllm
# Start the vLLM server:
vllm serve "YuechunSun/TopoVerus-32B"
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:8000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "YuechunSun/TopoVerus-32B",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker

docker model run hf.co/YuechunSun/TopoVerus-32B

SGLang

How to use YuechunSun/TopoVerus-32B with SGLang:

Install from pip and serve model

# Install SGLang from pip:
pip install sglang
# Start the SGLang server:
python3 -m sglang.launch_server \
    --model-path "YuechunSun/TopoVerus-32B" \
    --host 0.0.0.0 \
    --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "YuechunSun/TopoVerus-32B",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker images

docker run --gpus all \
    --shm-size 32g \
    -p 30000:30000 \
    -v ~/.cache/huggingface:/root/.cache/huggingface \
    --env "HF_TOKEN=<secret>" \
    --ipc=host \
    lmsysorg/sglang:latest \
    python3 -m sglang.launch_server \
        --model-path "YuechunSun/TopoVerus-32B" \
        --host 0.0.0.0 \
        --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "YuechunSun/TopoVerus-32B",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Docker Model Runner
How to use YuechunSun/TopoVerus-32B with Docker Model Runner:
```
docker model run hf.co/YuechunSun/TopoVerus-32B
```

TopoVerus-32B

TopoVerus-32B repairs proofs in Verus programs. It is a full-weight BF16 model derived from Qwen/QwQ-32B through counterexample-guided supervised fine-tuning and dependency-aware GRPO training.

Quick start

Install Transformers, PyTorch, Accelerate and safetensors in a compatible GPU environment. The example uses Transformers 4.52.1 and PyTorch 2.6.0. The BF16 weights occupy approximately 61 GiB; generation needs additional memory. Place the Verus program to repair in program.rs.

from pathlib import Path
import torch
from transformers import AutoModelForCausalLM, AutoTokenizer

model_id = "YuechunSun/TopoVerus-32B"
tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(
    model_id, torch_dtype=torch.bfloat16, device_map="auto"
)
code = Path("program.rs").read_text()
messages = [
    {
        "role": "system",
        "content": (
            "You are a Verus formal-verification expert. Repair only proof annotations. "
            "Preserve executable code, function contracts and specification functions. "
            "Respond with <think>...</think>, <counterexample> containing [State], "
            "[Execution Trace] and [Violation], <reasoning>...</reasoning>, then "
            "exactly one final Rust code fence. Do not use assume or admit."
        ),
    },
    {
        "role": "user",
        "content": f"Repair this Verus program.\n\n[Buggy Code]\n```rust\n{code}\n```",
    },
]
text = tokenizer.apply_chat_template(
    messages, tokenize=False, add_generation_prompt=True
)
inputs = tokenizer(text, return_tensors="pt").to(model.device)
with torch.inference_mode():
    output = model.generate(
        **inputs,
        max_new_tokens=8192,
        do_sample=True,
        temperature=0.7,
        top_p=0.9,
    )
print(tokenizer.decode(
    output[0, inputs.input_ids.shape[1]:], skip_special_tokens=True
))

The response includes reasoning and a final fenced Verus program. Extract the final program and run Verus on it. For iterative repair, provide the previous candidate and its verifier diagnostics in the next request.

License and attribution

This model is licensed under Apache-2.0; see LICENSE. It is derived from Qwen/QwQ-32B by Alibaba Cloud. Modifications include supervised fine-tuning, dependency-aware reinforcement learning, and export of the final weights to BF16.

Downloads last month: 21

Safetensors

Model size

33B params

Tensor type

BF16

Model tree for YuechunSun/TopoVerus-32B

Base model

Qwen/Qwen2.5-32B

Finetuned

Qwen/QwQ-32B

Finetuned

(95)

this model