Crocq

A VS Code extension for developing functionally correct C code with the Verified Software Toolchain, following the workflows in Software Foundations Volume 5: Verifiable C.

Annotate C programs with /*@ ... */ specifications, jump between code and proof, and generate Rocq models with CompCert's clightgen.

See examples/ for small verified C programs with Crocq annotations demonstrating the features of the extension.

Crocq is under active development. Windows is not supported in this release; macOS on Apple Silicon, Linux x64 and Linux arm64 are supported.

Features

Annotate C code with special comments that link to the corresponding specification and proof:

Generate the Rocq model

Generate the model with clightgen; Crocq tracks whether it is up to date and warns when the C program changes.

Scaffold specifications and proofs

Create the boilerplate verif_<file>.v next to each annotated C file, so you can focus on the proofs. Existing files are not overwritten unless you use the overwrite variant.

Inline specifications and invariants

Keep VST assertions and funspecs close to their implementations with SPEC_INLINE and INV_INLINE. Diagnostics from VsRocq are forwarded into the annotation where the model is written.

Coming soon: Proof status

Crocq is being extended to show whether a function's proof is complete, admitted or failing, next to its PROOF clause.

---

Also included: diagnostics and syntax highlighting for annotations, navigation in both directions, dependency checks with status views, annotation formatting, and model-staleness tracking.

Supported platforms

0.1.0 ships native parser binaries for:

• macOS (Apple Silicon)
• Linux (x64/arm)

Windows is not supported yet. Intel Macs are not supported yet either. The extension refuses to activate with an explanation on any other platform.

Requirements

• VS Code 1.104 or later.
• Rocq 9.1 or later.
• CompCert 3.17 or later, including the clightgen tool. With opam: opam install coq-compcert.
• VsRocq 2.5.0 or later.
• A C compiler (gcc or clang).

If a dependency is missing or outdated, Crocq shows a notification and links to the installation guide in Software Foundations volume 5, Verifiable C — Practicalities. The same link is available from the Dependencies view.

Install

From the VS Code Marketplace, search for Crocq (publisher code2rocq), or install the VSIX attached to the latest release:

code --install-extension crocq-0.1.0.vsix

Reload the window after installing. VsRocq must be installed and enabled; Crocq checks for it and offers a link instead of failing silently.

Annotations

A function annotation links the C function to a Rocq specification and proof:

/*@
  SPEC verif_sumarray_linked.v:sumarray_spec
  PROOF verif_sumarray_linked.v:body_sumarray
*/
unsigned sumarray(unsigned a[], int n)
{
  /*@
    INV verif_sumarray_linked.v:loop_invariant
  */
  while (i < n)
  {
    /* ... */
  }
}

An annotation starts with /*@ and is made of clauses: an uppercase keyword followed by its contents. Clauses that link to a Rocq document use the path to the file, a colon, and the target name. Annotations are currently valid above function definitions and loops.

Clause	Applies to	Meaning
PROOF path.v:name	function	Links to the theorem/lemma that proves the function.
SPEC path.v:name	function	Links to the VST specification (funspec).
SPEC_INLINE <{ ... }>	function	Inline specification body (requires SPEC).
INV path.v:name	loop	Links to the loop invariant.
INV_INLINE <{ ... }>	loop	Inline invariant body (requires INV).

ℹ️ Links are relative to the C file.

SPEC_INLINE and INV_INLINE attach an inline body to the linked SPEC/INV clause. Saving the C file replaces the body of that definition in the .v file, so the C annotation is the source of truth for it.

Inline clause rules:

• the linked target must be a Rocq definition with a body (:=); its statement is kept and only the body is replaced;
• an annotation may have at most one inline clause, and it requires its link (SPEC_INLINE needs SPEC, INV_INLINE needs INV);
• edits made to that definition body in the proof document are overwritten the next time the C file is saved;
• the inline body cannot contain the C annotation terminator. A missing or unterminated wrapper is reported on the clause without disabling the rest of the annotation;
• diagnostics inside the linked definition are mirrored onto the inline body, so proof errors are visible where the model is written.

Commands

Command	What it does
Crocq: Create Rocq model of opened file	Runs clightgen -normalize on the active C file.
Crocq: Toggle auto-generation of Rocq model on save	Turns automatic model generation on or off for the workspace.
Crocq: Check Dependencies	Re-runs the Rocq/CompCert/VsRocq dependency check.
Crocq: Show Status	Reveals the Rocq model and Dependencies views.
Crocq: Create proof files for project	Scaffolds verif_<file>.v for every annotated C file; never overwrites.
Crocq: Create proof files for project (Overwrite existing)	Same, but overwrites existing generated proof files.
Crocq: Format annotations	Formats annotation blocks without touching C.

Settings

Setting	Default	Description
crocq.clightgen.path	clightgen	Path to the clightgen executable from CompCert. Use the bare name to look it up on PATH.
crocq.formatAnnotationsOnSave	follow	Format annotations on save. follow uses editor.formatOnSave; yes always formats; no never does.

As with editor.formatOnSave, an auto-save after a delay does not format; an explicit save does, even when files.autoSave is afterDelay. Formatting is applied as a will-save edit, so a C formatter still runs afterwards.

Known limitations

• Windows is not supported in 0.1.0. It is planned for a later release. The extension blocks installation on Windows and refuses to activate on unsupported architectures (for example Intel macOS).
• Generated proof documents contain placeholder specifications and invariants and do not compile until you fill them in.
• Inline clause bodies are authoritative. If you edit the linked definition in the .v file, saving the C file overwrites that edit.
• Proof status (solved/admitted) is not shown in the editor yet.
• Code completions for clause targets and Rocq definitions are not implemented yet.
• Opening some Rocq documents can surface VsRocq/Rocq errors; this is tracked in #93.

See https://git.marfavi.com/code2rocq/crocq/issues for all tracked issues.

Troubleshooting

• clightgen not found — set crocq.clightgen.path to the executable, or install CompCert with opam install coq-compcert.
• VsRocq missing or too old — install VsRocq 2.5.0 or later and reload the window.
• A command does nothing — run Crocq: Show Status and check the Dependencies view. Errors and command output are written to the Crocq output channel (View → Output → Crocq).
• Model looks stale — regenerate it with Crocq: Create Rocq model of opened file. The status view shows the clightgen command that was run.

Repository layout

Path	Contents
extension/	The VS Code extension (TypeScript).
tree-sitter-crocq/	The tree-sitter grammar for Crocq annotations.
examples/	Small verified C projects used for demos and manual testing.
.forgejo/	CI workflows, runner configuration and container images.

License

MIT.