Menu

Individual skill

bounded-model-checking-c

0upvotes

Use when C or C++ code needs memory-safety or undefined-behavior guarantees proved with CBMC, or ACSL contracts checked with Frama-C Eva or WP. Not for choosing the proof policy: use proof-driven.

.devin/skills/bounded-model-checking-c/SKILL.md

Read pinned source

Source commit b0e8ce89a19fac880251dc3ea1babfeb4503a4fe

What was checked

Matches the observed repository HEAD
Yes
Scanner rules are current
No
Repository scan complete
No
Skill scan complete
No
Observed behavior
Not checked yet
Last checked
Nov 4, 2026

These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.

Install this skill

Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.

An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.

Repository context

Repository stars (not skill ratings)
55
Repository last updated
Sep 28, 2026
License
Apache-2.0

Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.

Files and excerpt

File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.

Browse files
Read excerpt

# Bounded model checking C

## Contract

| Field | Bound contract |
|---|---|
| Trigger | A C or C++ function or module needs its memory safety, arithmetic, or user assertions checked exhaustively up to a bound (CBMC), its runtime errors bounded by abstract interpretation (Frama-C Eva), or its ACSL contracts proved deductively (Frama-C WP), or an existing run's trace or alarm must be read. |
| Authority | Reversible local: writes harness `.c` files, ACSL annotations in the source under analysis, and the tools' output directories; rollback is reverting those files. No remote mutation. |
| Side effect | Harness and annotated source on disk, CBMC GOTO binaries when `goto-cc` is used, WP proof-obligation files under `-wp-out`, and Frama-C session files when `-save` is used. |
| Done | Every property in scope is reported safe by CBMC under a recorded unwind bound, or has no Eva alarm, or is `Valid` under WP with a named prover, or has a trace or alarm mapped to a code defect and a fix. |

## Inputs

The C sources, the entry function, and the properties: absence of undefined behavior (out-of-bounds access, null or dangling dereference, overflow, division by zero), or functional contracts. Tool pins from the grounded set: CBMC cbmc-6.11.0 (`brew install cbmc` on macOS, `.deb` or `.msi` packages, or Docker `ghcr.io/diffblue/cbmc`) and Frama-C 33.0 "Arsenic" (`opam install frama-c`, or the Linux `.run` installer `frama-c-linux-x86-64-33.0-Arsenic.run`); WP needs Why3 and at least one prover on `PATH`, and Alt-Ergo is the documented first choice. Optional: per-loop unwind bounds, the target data model (`--LP64`, `--ILP32`), and an Eva precision level.