{"data":{"kind":"file","path":"README.md","version_id":"fssye4sbjj7b6azbspib1nhi","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":6182,"modified_at":"2026-09-11T19:35:53.167000","content_hash":"9e60fa9cdaa329a901484a0bc7c3b44ecc2bd0b44382fc9c96996898658c63a0"},"entries":[],"content":"# Formally Verified C\n\nAn RL environment for generating C implementations that satisfy fixed ACSL\ncontracts. Model output is judged by Frama-C WP+RTE under a pinned toolchain.\nThe public package and Prime Hub slug are `formally-verified-c`; `acsl_c`\nremains the internal compatibility namespace.\n\n## Current status\n\nTechnical and public-data validation are complete for v0.1. The wheel bundles\nthe project-authored Apache-2.0 Core-v1 and excludes CASP-derived task payload.\nCASP remains a non-bundled research adapter until its per-file rights can be\nreconstructed or permission is obtained.\n\n- Exact API target: Prime-RL v0.9.0 plus its vendored Verifiers commit.\n- Public Core-v1: 33 train / 15 validation / 16 test (64 total).\n- Public proof replay: 64/64 references, 296/296 goals, 84/84 RTE goals,\n  zero timeouts; 64/64 deterministic negative cases rejected.\n- Research-only CASP corpus: 221 train / 47 validation / 48 test; 22 excluded.\n- Reward: parse gate 0.10, VC fraction 0.50, full proof 0.20, fixed-spec\n  integrity 0.20.\n- Persistent SQLite/WAL verdict cache includes source, prover policy, timeout,\n  runner schema, and full toolchain ID in its key.\n- Single-turn `null` and multi-turn `bash` harness modes are implemented.\n- Hints-mode fixed-contract completion is release-ready. Full specification\n  synthesis remains deliberately disabled; its accepted/rejected executor\n  contract now has a clean negative fixture, but it is a future task family.\n\nSee the repository's `docs/LEARNING_GUIDE.md` for concepts and\n`docs/EXPERIMENT_PROTOCOL.md` before running a claim-bearing experiment.\nFor the environment-specific release gates—especially reward hacking,\ncredit assignment, prompt boundaries, and what does *not* require a long RL\nrun—see `docs/ENVIRONMENT_VALIDATION.md`.\n\n## Layout\n\n```text\nsrc/acsl_c/taskset.py       typed taskset and reward hooks\nsrc/acsl_c/integrity.py     immutable-context / annotation checks\nsrc/acsl_c/framac.py        stable Frama-C verdict parser\nsrc/acsl_c/verify_script.py isolated runtime runner\nsrc/acsl_c/cache.py         cross-process verdict cache\nsrc/acsl_c/spectests.py     conservative strength policy\nscripts/ingest_casp.py      re-verification and vacuity quarantine\nscripts/build_splits.py     deterministic split manifest\nscripts/replay_references.py resumable production-image reference replay\nconfigs/train.toml          supported two-GPU GRPO config\nconfigs/agentic_eval_v0_9.toml multi-turn validation config\nconfigs/validate.toml       model-free Verifiers v1 container release smoke\ndocker/Dockerfile           pinned judge image definition\n```\n\n## Data contract\n\nPublic data are JSONL records in `data/packs/core-v1`, selected by that pack's\n`manifest.json`. Important fields include `mode`, `skeleton_c`,\n`reference_solution`, `negative_cases`, provenance and license fields, semantic\nand derivation families, `non_vacuous`, and `data_schema_version`. Explicit\nresearch directories retain compatibility with the older CASP schema; those\nrecords are never bundled implicitly.\n\nPublic tasks use explicit stable IDs. Imported research tasks use a dataset\nnamespace plus a SHA-256 digest of normalized reference source rather than a\nmutable row number.\n\n## Local validation\n\nThe primary deliverable is a correct, isolated, reproducible environment. A\nlong multi-seed GRPO campaign is optional research evidence, not a prerequisite\nfor validating this taskset. Run the adversarial and credit-assignment fixtures\ndescribed in `docs/ENVIRONMENT_VALIDATION.md` in addition to the happy-path\nsmokes below.\n\nRun inside Linux/WSL with Python 3.12 and uv:\n\n```bash\nuv venv /tmp/acslc-venv --python 3.12\nuv pip install --python /tmp/acslc-venv/bin/python -e '.[test]'\n/tmp/acslc-venv/bin/python -m pytest -q\n/tmp/acslc-venv/bin/python scripts/smoke_taskset.py\neval \"$(opam env)\"\n/tmp/acslc-venv/bin/python scripts/live_runtime_smoke.py\nuv run python scripts/preflight.py --prime-root /workspace/prime-rl\n```\n\nThe `live_runtime_smoke.py` command intentionally uses a host subprocess only\nwith trusted reference data. Never use that runtime for model-generated\noutput. `preflight.py` is read-only apart from an optional report file. Its\ndefault exit gate is environment release readiness; `--require async`\nadditionally requires two locally visible GPUs.\n\n## Container and training\n\n```bash\ndocker pull ghcr.io/stanleyngugi/formally-verified-c-judge@sha256:b7d7111eac04eb09405842b64af5084f671c8815f90a3d9ea7f5de92f0bcd593\ndocker image inspect ghcr.io/stanleyngugi/formally-verified-c-judge@sha256:b7d7111eac04eb09405842b64af5084f671c8815f90a3d9ea7f5de92f0bcd593 --format '{{.Id}}'\ndocker run --rm -v \"$PWD:/workspace/acsl-c\" ghcr.io/stanleyngugi/formally-verified-c-judge@sha256:b7d7111eac04eb09405842b64af5084f671c8815f90a3d9ea7f5de92f0bcd593 \\\n  python3 /workspace/acsl-c/scripts/replay_references.py \\\n  --data-dir /workspace/acsl-c/data --split all --jobs 1 \\\n  --output /workspace/acsl-c/artifacts/reference-replay.jsonl \\\n  --summary /workspace/acsl-c/artifacts/reference-replay.summary.json\n\n# From the pinned Prime-RL v0.9.0 checkout:\nuv run --no-sync validate @ /workspace/acsl-c/configs/validate.toml\nuv run --no-sync rl @ /workspace/acsl-c/configs/train.toml --dry-run True\nuv run rl @ /workspace/acsl-c/configs/train.toml\n```\n\n`configs/train.toml` assumes two GPUs: one trainer and one inference GPU. The old\n16 GB single-GPU TOML is retained only as a historical record of the 2026-08-25\nsmoke and depends on now-obsolete local Prime-RL patches.\n\n## Safety boundaries\n\n- `AcslCTask.NEEDS_CONTAINER = True` rejects subprocess production configs.\n- The model may change only the target function body in hints mode.\n- Scoring independently invokes the pinned runner; it does not trust an agent's\n  edited `verify.sh` or textual claim.\n- Unknown vacuity and malformed extraction are excluded from research splits.\n- Release configs use an empty runtime network allow-list; the release smoke\n  confirms direct egress is blocked and the host workspace is not mounted.\n- The wheel bundles the canonical corpus shards, split manifest, and exclusions,\n  so hub installation does not depend on a developer checkout path.\n","encoding":"utf-8","truncated":false,"total_bytes":6182},"status":null}