QinxiangCao/QualifiedCProgramming
Skill Claude CodeCodex
Use after the run's sole annotation owner has formed the first candidate or repaired a candidate from retry feedback; the same annotation agent checks the current main-root C annotation, the existing formalcaselib, generated results, and coverage of aggregated blockers, iterates repairs within the permitted boundary…
QinxiangCao/QualifiedCProgramming
Skill Claude CodeCodex
Use when the controller first delivers an annotation attempt for a run, or appends annotation gaps summarized from annotation-check or parent/group results to the same owner; the run's sole, persistently reused annotation agent adds or repairs the target C annotation in main root, maintains the mathematical…
QinxiangCao/QualifiedCProgramming
Skill Claude CodeCodex
Use from the main agent after final-apply has written the accepted provingmerged result back to main root; verify consistency among generated files, manual, formalcaselib, versions, merge result, and cleanup.
QinxiangCao/QualifiedCProgramming
Skill Claude CodeCodex
Use after a group-worker receives a controller-claimed groupworkerinput.md or an append-group-worker for the same owner; prove assigned witnesses only in the fixed group directory, modify the handoff-provided copied manual and optional groupworkerlib, and deliver a terminal completed report or a report with a complete…
QinxiangCao/QualifiedCProgramming
Skill Claude CodeCodex
Use by an independent vc-checking owner after the controller has claimed a vc-checking attempt, the accepted selected-backend dependency snapshot is prepared, and the raw manual contains at least one top-level VC; read only the formal source bound by the handoff, complete the exhaustive split-first provability…
QinxiangCao/QualifiedCProgramming
Skill Claude CodeCodex
Use when the main agent controls a complete run for one C verification case in this repository; starting at init-run, follow controller actions to manage the sole annotation agent, vc-checking and every group-worker when needed, aggregated annotation-gap feedback, mechanical merge, final-apply, and final-check until…
QinxiangCao/QualifiedCProgramming
Instructions file CodexOpenCode
Repository instructions for verifying C programs through annotations, symbolic execution, manual verification conditions, and Rocq proofs. Rocq is a system for formally checking mathematical and program-correctness proofs.