Proof-synthesis challenges mined from the git history of
AbsInt/CompCert, the formally verified C
compiler. Each challenge is a real proof-engineering edit that a human made in a
single commit: we take the repository state before the commit (the
challenge) and treat the state after the commit (the solution) as
ground truth. The model's job is to reconstruct the proof/spec work the human
did.
⚠️ License notice. CompCert is distributed under the… See the full description on the dataset page:
https://huggingface.co/datasets/for-all-dev/CompCert-eval.
