neurips2026-crychic/crychic-dafny-acsl

CRYCHIC Dafny-to-ACSL-C Verified Translation Benchmark

This anonymized review artifact accompanies the NeurIPS 2026 Evaluations and Datasets submission: CRYCHIC: A Universal Framework for Cross-Language Verified Code Translation.

CRYCHIC translates verified Dafny programs into C programs annotated with ACSL specifications, then checks the generated artifacts with Frama-C WP. This release contains the 1,679 fully verified Dafny/C+ACSL pairs used as the positive benchmark corpus.

The Dafny source programs in this benchmark are derived from the Re:Form corpus (Yan et al., 2025): https://github.com/Veri-Code/ReForm.

Contents

crychic_dataset_release/
├── programs/                 # Generated verified C+ACSL programs
├── sources/                  # Original Dafny source programs
├── records.jsonl             # Hugging Face / tabular viewer records with code text
├── records.csv               # Lightweight metadata table without code text
├── manifest.jsonl            # File-level manifest, provenance, checksums
├── metadata.json             # Full dataset metadata and statistics
├── croissant.json            # Croissant + RAI metadata for NeurIPS E&D hosting
├── DATASHEET.md              # Dataset card / datasheet
├── BENCHMARK_PROTOCOL.md     # Evaluation protocol
├── NEURIPS_ED_SUBMISSION_CHECKLIST.md
├── LICENSE.md
└── checksums.sha256

Dataset Summary

Schema

Each records.jsonl row contains:

• —program_id: anonymized stable ID.
• —source_dataset, original_file: source subset and anonymized original file name.
• —dafny_code: original Dafny program.
• —c_code: generated C+ACSL program.
• —dafny_loc, c_loc, complexity_bucket: size metadata.
• —requires_count, ensures_count, loop_invariant_count, assert_count: ACSL feature counts.
• —verified, final_status: final verification label. All released rows are fully verified.

Intended Use

Use this artifact to evaluate and analyze systems for cross-language verified-code generation, ACSL annotation generation, and verifier-guided repair. The primary benchmark task is:

Input: verified Dafny program. Output: C program with ACSL annotations that passes the CRYCHIC Frama-C WP verification protocol.

Verification Command

frama-c -wp -wp-prover alt-ergo,z3 -wp-timeout 5 programs/program_0001.c

The exact benchmark protocol and toolchain assumptions are documented in BENCHMARK_PROTOCOL.md.

Responsible Use

The generated C+ACSL programs are research artifacts. Passing the stated verifier configuration does not imply deployment safety, security, or correctness outside the encoded specifications and toolchain assumptions.

License and Anonymity

This is an anonymous review artifact. Licensing and provenance are documented in LICENSE.md. Re:Form source-data use is permission-based with attribution; after acceptance, anonymous metadata will be replaced with author metadata and final public release terms. The final release will cite the Re:Form paper and link back to https://github.com/Veri-Code/ReForm.

Citation

@inproceedings{anonymous2026crychic,
  title = {CRYCHIC: A Universal Framework for Cross-Language Verified Code Translation},
  author = {Anonymous},
  booktitle = {Advances in Neural Information Processing Systems},
  year = {2026},
  note = {Under review}
}