ANCORA

ANCORA (Anchored Curriculum for Reasoning under Autoformal verification) is a self-play RL framework that learns to generate and solve formal-verification problems for the Verus prover.

This repository is a staged artifact release for ANCORA. It currently includes curated seed pools, a Verus verification harness, and reference figures. Additional training components are planned for a later release.

---

Why this matters

Conventional RL on verification tasks is bottlenecked by a fixed problem set. ANCORA replaces the static curriculum with a proposer-solver coupled loop:

1. A Q-Gen policy proposes new specifications, anchored to a manifold seeded by curated Verus problems.
2. An S-Gen policy attempts to verify each spec.
3. Pass-rate signals shape both rewards via a two-level group-relative advantage scheme that prevents the proposer from drifting off-manifold.
4. A UCB-guided Curriculum DAG grows online: solved-yet-frontier specs spawn descendants; pruned specs leave the active pool.

The result is a curriculum that adapts to the solver's evolving frontier without external teacher signal.

What's released here, and what's coming

This is the initial public artifact snapshot. The trainer source and checkpoints are not included in this snapshot; see ROADMAP.md for the staged release plan.

Asset	Status	Path
Transfer seed pool (234 problems)	released	data/seed_pool_transfer.jsonl
Test-time-training seed pool (436 problems)	released	data/seed_pool_ttt.jsonl
Verus verification harness	released	eval/verify_verus.py
Reference figures (PDF source)	released	figs/
Training shell entrypoints + Hydra configs	planned	see ROADMAP.md
Q-Gen / S-Gen trainer (qs_trainer.py)	planned	see ROADMAP.md
Self-distilled SFT pipeline	planned	see ROADMAP.md
Trained checkpoints	planned	see ROADMAP.md

The released assets are sufficient to reproduce evaluation against either seed pool and verify provenance of the curated problem sets. The full Hydra configuration for the training runs will ship together with the trainer so the released configs match the accompanying checkpoints rather than a hand-edited approximation.

Repository layout

ANCORA/
|-- README.md
|-- LICENSE                         # Apache-2.0
|-- CITATION.cff
|-- ROADMAP.md                      # release timeline for trainer + checkpoints
|-- data/
|   |-- README.md                   # seed-pool format and provenance
|   |-- seed_pool_transfer.jsonl    # 234 specs
|   `-- seed_pool_ttt.jsonl         # 436 specs
|-- eval/
|   |-- README.md
|   `-- verify_verus.py             # parallel Verus verification (Docker harness)
`-- figs/                           # reference figures
    |-- gsv_diagram.pdf
    |-- ucb_dag.pdf
    |-- q_balance_comparison.pdf
    `-- sft_bootstrap.pdf

Quick start (evaluation only)

The released harness can verify candidate Verus solutions against either seed pool. Trainer and checkpoint release will follow per ROADMAP.md.

# 1. Build the verifier container.
#    A Dockerfile is forthcoming with the trainer release; for now you need
#    a container named `verl_eval` with verus on PATH.

# 2. Inspect either seed pool.
head -1 data/seed_pool_transfer.jsonl | python -m json.tool

# 3. Run the verifier on (spec, candidate-impl) pairs.
python eval/verify_verus.py --help

See eval/README.md for harness details and data/README.md for seed-pool schema.

Citation

If you use the seed pools, verifier harness, or curriculum design, cite this artifact for now:

@misc{ancora_artifact_2026,
  title        = {ANCORA Artifact Release},
  author       = {ANCORA Authors},
  year         = {2026},
  howpublished = {GitHub repository}
}

Publication metadata will be added when available.

License

Code: Apache-2.0 (see LICENSE). Seed pools: derived from publicly available Verus / Dafny example sets; redistribution permitted under the same Apache-2.0 terms.

Acknowledgements

Built on top of verl (volcengine) for distributed RL infrastructure and Verus for formal verification.