Agent skill

Program Correctness Prover

Generate Isabelle or Coq proofs establishing partial or total correctness of imperative programs from code and formal specifications.

Apache-2.0Auto-check passed

Install Program Correctness Prover

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill program-correctness-prover -a claude-code

Project install by default; add -g for ~/.claude/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE program-correctness-prover --agent claude-code

Project scope by default; add --scope user for a personal install. Needs GitHub CLI 2.90.0 or later (public preview).

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .claude/skills && cp -r skills-src/skills/program-correctness-prover .claude/skills/program-correctness-prover && rm -rf skills-src

Use ~/.claude/skills/ instead of .claude/skills for a personal install. The folder must contain SKILL.md.

Claude Code skills documentation · loads skills from .claude/skills/

Paste into Claude Code

Install the "program-correctness-prover" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/program-correctness-prover into .claude/skills/program-correctness-prover/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "program-correctness-prover", then confirm the skill loads.

Claude Code copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

$skill-installer

$skill-installer install https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/program-correctness-prover

Type this inside Codex. $skill-installer <name> installs a curated skill from openai/skills. The installer writes to $CODEX_HOME/skills (default ~/.codex/skills). Restart Codex if the skill does not show up.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill program-correctness-prover -a codex

Project install goes to .agents/skills/; add -g for ~/.codex/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE program-correctness-prover --agent codex

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .agents/skills && cp -r skills-src/skills/program-correctness-prover .agents/skills/program-correctness-prover && rm -rf skills-src

Use ~/.agents/skills/ instead of .agents/skills for a personal install.

Codex skills documentation · loads skills from .agents/skills/

Paste into Codex

Install the "program-correctness-prover" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/program-correctness-prover into .agents/skills/program-correctness-prover/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "program-correctness-prover", then confirm the skill loads.

Codex copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill program-correctness-prover -a cursor

Project install goes to .agents/skills/; add -g for ~/.cursor/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE program-correctness-prover --agent cursor

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .cursor/skills && cp -r skills-src/skills/program-correctness-prover .cursor/skills/program-correctness-prover && rm -rf skills-src

Use ~/.cursor/skills/ instead of .cursor/skills for a personal install.

Cursor skills documentation · loads skills from .cursor/skills/, .agents/skills/, .claude/skills/, .codex/skills/

Paste into Cursor

Install the "program-correctness-prover" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/program-correctness-prover into .cursor/skills/program-correctness-prover/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "program-correctness-prover", then confirm the skill loads.

Cursor copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

gemini skills install

$ gemini skills install https://github.com/ArabelaTso/Skills-4-SE.git --path skills/program-correctness-prover

--scope user (default) or --scope workspace; --path is the subfolder of the repo that holds the skill; --consent skips the security confirmation prompt.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill program-correctness-prover -a gemini-cli

Project install goes to .agents/skills/; add -g for ~/.gemini/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE program-correctness-prover --agent gemini-cli

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .gemini/skills && cp -r skills-src/skills/program-correctness-prover .gemini/skills/program-correctness-prover && rm -rf skills-src

Use ~/.gemini/skills/ instead of .gemini/skills for a personal install, then run /skills reload.

Gemini CLI skills documentation · loads skills from .gemini/skills/, .agents/skills/

Paste into Gemini CLI

Install the "program-correctness-prover" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/program-correctness-prover into .gemini/skills/program-correctness-prover/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "program-correctness-prover", then confirm the skill loads.

Gemini CLI copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE program-correctness-prover

Installs for Copilot at project scope by default; add --scope user for a personal install. Preview a skill first with gh skill preview. Needs GitHub CLI 2.90.0 or later (public preview).

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill program-correctness-prover -a github-copilot

Project install goes to .agents/skills/; add -g for ~/.copilot/skills/.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .github/skills && cp -r skills-src/skills/program-correctness-prover .github/skills/program-correctness-prover && rm -rf skills-src

Use ~/.copilot/skills/ instead of .github/skills for a personal install. Commit .github/skills so cloud agent and code review can use it.

GitHub Copilot skills documentation · loads skills from .github/skills/, .claude/skills/, .agents/skills/

Paste into GitHub Copilot

Install the "program-correctness-prover" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/program-correctness-prover into .github/skills/program-correctness-prover/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "program-correctness-prover", then confirm the skill loads.

GitHub Copilot copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill program-correctness-prover -a opencode

OpenCode documents no install command of its own. Project install goes to .agents/skills/; add -g for ~/.config/opencode/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE program-correctness-prover --agent opencode

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .opencode/skills && cp -r skills-src/skills/program-correctness-prover .opencode/skills/program-correctness-prover && rm -rf skills-src

Use ~/.config/opencode/skills/ instead of .opencode/skills for a personal install.

OpenCode skills documentation · loads skills from .opencode/skills/, .claude/skills/, .agents/skills/

Paste into OpenCode

Install the "program-correctness-prover" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/program-correctness-prover into .opencode/skills/program-correctness-prover/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "program-correctness-prover", then confirm the skill loads.

OpenCode copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

Facts

Skill name: program-correctness-prover
GitHub stars: 253
Token cost: ~2.5k tokens
SKILL.md length: 743 words
Files: 3 (incl. references)
Skills in repo: 151
Repo updated: Aug 21, 2026
First seen: Oct 7, 2026
Licence: Apache-2.0

At a glance

Generate Isabelle or Coq proofs establishing partial or total correctness of imperative programs from code and formal specifications.

Works in 5 steps: Analyze Program Structure → Generate Loop Invariants → Generate Verification Conditions → …
Prove program correctness using Hoare logic
SKILL.md covers Overview, How to Use, Verification Workflow and Example: Sum of Array, plus 5 more sections
Instructions only: no scripts, shell commands, URLs or credentials in SKILL.md

What it does

Program Correctness Prover is an agent skill from ArabelaTso/Skills-4-SE. Generate Isabelle or Coq proofs establishing partial or total correctness of imperative programs from code and formal specifications. Use when users need to: (1) Prove program correctness using Hoare logic, (2) Generate verification conditions from pre/postconditions, (3) Construct loop invariants and termination arguments, (4) Verify imperative programs with assignments, conditionals, and loops. Supports both partial correctness (if terminates, postcondition holds) and total correctness (terminates and…

Its SKILL.md is about 2.5k tokens, which your agent loads only when the skill is triggered. The skill folder holds 3 other files, including reference files (for example `references/hoare_logic.md` and `references/verification_patterns.md`).

The repository describes itself as: A curated list of 180+ useful Claude Skills for Software Engineering and resources for customizing AI for SE workflows. The licence is Apache-2.0.

When your agent uses it

Prove program correctness using Hoare logic
Generate verification conditions from pre/postconditions
Construct loop invariants and termination arguments
Verify imperative programs with assignments

Example prompts

“/program-correctness-prover”

Workflow steps

5 steps, taken from the step headings in SKILL.md.

Analyze Program Structure
Generate Loop Invariants
Generate Verification Conditions
Construct Proof
Add Termination Argument (Total Correctness)

What it can do on your machine

Read from SKILL.md and the folder at commit 4f38503. It shows what the files ask for, not the result of running them.

Tool permissions
Pre-approves nothing: there is no allowed-tools line, so your agent's usual permission prompts apply.
From allowed-tools in the SKILL.md frontmatter.
Runs code
No scripts in the folder and no shell commands in SKILL.md (its code samples are isabelle and coq).
From the folder's file list and the shell code blocks in SKILL.md.
Network
No URLs in SKILL.md.
From URLs in SKILL.md, links to its own repository left out.
Credentials
Names no API keys, tokens, secrets or passwords.
From names ending in _API_KEY, _TOKEN, _SECRET, _KEY or _PASSWORD in SKILL.md.

Context cost

Program Correctness Prover loads about 2.5k tokens when it runs, and up to ~6.8k if it reads all its reference files. Until then it costs about 147 tokens; SKILL.md has 743 words of instructions outside code blocks.

Always · name and description, kept in context so the agent knows when to use it: ~147
When it runs · the whole SKILL.md, loaded when a task matches: ~2.5k
With references · SKILL.md plus every file in references/, read only if the agent opens them: ~6.8k

Estimates: characters ÷ 4, the usual rule of thumb; real counts depend on the model's tokenizer. Scripts and assets cost tokens only if the agent reads them.

Safety

Auto-check passed

The automated check found no risky patterns in SKILL.md.

Automated static check — not a guarantee. Review scripts before installing. It scans the text of SKILL.md for risky patterns (piping downloads into a shell, reading credential files, hidden Unicode, destructive commands); files beside SKILL.md are not scanned.

SKILL.md

The full file from ArabelaTso/Skills-4-SE at commit 4f38503, republished under its Apache-2.0 licence (© ArabelaTso). 743 words, ~2,452 tokens.

Download SKILL.mdSave it as .claude/skills/program-correctness-prover/SKILL.md (or your agent's skills folder). This skill also uses 2 other files; get the full folder from GitHub.

name: program-correctness-prover
description: Generate Isabelle or Coq proofs establishing partial or total correctness of imperative programs from code and formal specifications. Use when users need to: (1) Prove program correctness using Hoare logic, (2) Generate verification conditions from pre/postconditions, (3) Construct loop invariants and termination arguments, (4) Verify imperative programs with assignments, conditionals, and loops. Supports both partial correctness (if terminates, postcondition holds) and total correctness (terminates and postcondition holds) for both Isabelle/HOL and Coq.

Program Correctness Prover

Generate formal proofs establishing correctness of imperative programs.

Overview

This skill takes imperative program code with formal specifications (preconditions and postconditions) and generates complete correctness proofs in Isabelle or Coq using Hoare logic. It handles loop invariant generation, verification condition generation, and proof construction for both partial and total correctness.

How to Use

Provide:

Program code: Imperative program (assignments, conditionals, loops)
Specification: Precondition and postcondition
Target system: Isabelle or Coq
Correctness type: Partial or total correctness

The skill will generate:

Loop invariants (if needed)
Verification conditions
Complete formal proof
Termination argument (for total correctness)

Verification Workflow

Step 1: Analyze Program Structure

Identify program components:

Assignments: x := E
Sequences: C1; C2
Conditionals: if B then C1 else C2
Loops: while B do C

Step 2: Generate Loop Invariants

For each loop, construct an invariant that:

Holds initially: Precondition implies invariant
Preserved by loop body: {I ∧ B} C {I}
Implies postcondition: I ∧ ¬B ⟹ Q

Strategies:

Generalize postcondition by replacing constants with loop variables
Express partial computation at iteration i
Maintain relationships between variables

Step 3: Generate Verification Conditions

Apply Hoare logic rules to generate VCs:

Assignment: {P[E/x]} x := E {P}

Sequence: Chain intermediate conditions

Conditional: Prove both branches

Loop: Prove initialization, preservation, and termination

Step 4: Construct Proof

Build formal proof in target system:

Apply Hoare logic rules
Prove each verification condition
Use simplification and automation where possible

Step 5: Add Termination Argument (Total Correctness)

Provide variant function V that:

Is non-negative when loop condition holds
Strictly decreases each iteration

Example: Sum of Array

Program:

sum := 0;
i := 0;
while i < n do
  sum := sum + a[i];
  i := i + 1
done

Specification:

Precondition: n ≥ 0
Postcondition: sum = Σ(a[0..n-1])

Analysis:

Loop accumulates sum of array elements
Loop counter i ranges from 0 to n

Loop Invariant:

I: sum = Σ(a[0..i-1]) ∧ 0 ≤ i ≤ n

Verification Conditions:

Initialization: n ≥ 0 ⟹ 0 = Σ(a[0..-1]) ∧ 0 ≤ 0 ≤ n
- Simplifies to: n ≥ 0 ⟹ 0 = 0 ∧ 0 ≤ n ✓
Preservation: {I ∧ i < n} sum := sum + a[i]; i := i + 1 {I}
- WP: sum + a[i] = Σ(a[0..i]) ∧ 0 ≤ i + 1 ≤ n
- Verify: From I and i < n, this holds ✓
Postcondition: I ∧ ¬(i < n) ⟹ sum = Σ(a[0..n-1])
- From I and i ≥ n and i ≤ n, get i = n
- So sum = Σ(a[0..n-1]) ✓
Termination (total correctness): V = n - i
- Initially: V = n ≥ 0 ✓
- Decreases: i := i + 1 makes V' = V - 1 < V ✓
- Bounded: i ≤ n ⟹ V ≥ 0 ✓

Isabelle Proof (abbreviated):

isabelle

lemma sum_array_partial:
  "⦃λs. s ''n'' ≥ 0⦄
   sum := 0;; i := 0;;
   While (λs. s ''i'' < s ''n'')
   Do (sum := (λs. s ''sum'' + s ''a'' (s ''i''));;
       i := (λs. s ''i'' + 1))
   ⦃λs. s ''sum'' = (∑j<s ''n''. s ''a'' j)⦄"
proof -
  define I where "I = (λs. s ''sum'' = (∑j<s ''i''. s ''a'' j) ∧
                            0 ≤ s ''i'' ∧ s ''i'' ≤ s ''n'')"

  (* Initialization *)
  have "⦃λs. s ''n'' ≥ 0⦄ sum := 0;; i := 0 ⦃I⦄"
    unfolding I_def by (auto intro: hoare_seq hoare_asgn)

  (* Loop body preserves invariant *)
  moreover have "⦃λs. I s ∧ s ''i'' < s ''n''⦄
                 sum := (λs. s ''sum'' + s ''a'' (s ''i''));;
                 i := (λs. s ''i'' + 1)
                 ⦃I⦄"
    unfolding I_def by (auto intro: hoare_seq hoare_asgn)

  (* Apply while rule *)
  ultimately have "⦃λs. s ''n'' ≥ 0⦄
                   sum := 0;; i := 0;;
                   While (λs. s ''i'' < s ''n'')
                   Do (sum := (λs. s ''sum'' + s ''a'' (s ''i''));;
                       i := (λs. s ''i'' + 1))
                   ⦃λs. I s ∧ ¬(s ''i'' < s ''n'')⦄"
    by (auto intro: hoare_seq hoare_while)

  (* Postcondition follows from invariant *)
  then show ?thesis
    unfolding I_def by (rule hoare_conseq) auto
qed

Coq Proof (abbreviated):

coq

Theorem sum_array_partial : forall n a,
  n >= 0 ->
  {{ fun st => st N = n /\ n >= 0 }}
  sum ::= 0;;
  i ::= 0;;
  while i < N do
    sum ::= sum + a[i];;
    i ::= i + 1
  done
  {{ fun st => st sum = sum_array a n }}.
Proof.
  intros n a Hn.
  remember (fun st => st sum = sum_array a (st i) /\
                      0 <= st i /\ st i <= st N) as I.

  (* Initialization *)
  eapply hoare_seq. apply hoare_asgn.
  eapply hoare_seq. apply hoare_asgn.

  (* Loop *)
  eapply hoare_consequence_post.
  - apply hoare_while.
    (* Loop body *)
    eapply hoare_seq. apply hoare_asgn.
    eapply hoare_consequence_pre.
    + apply hoare_asgn.
    + intros st [HI Hcond]. subst I. simpl.
      destruct HI as [Hsum [Hi1 Hi2]].
      split; [|split]; try lia.
      rewrite Hsum. unfold sum_array. lia.
  - (* Postcondition *)
    intros st [HI Hcond]. subst I.
    destruct HI as [Hsum [Hi1 Hi2]].
    assert (st i = n) by lia.
    rewrite H. exact Hsum.
Qed.

Example: Maximum of Two Numbers

Program:

if x >= y then
  max := x
else
  max := y

Specification:

Precondition: true
Postcondition: max = max(x, y)

Analysis:

Conditional with two branches
No loops, so no invariants needed

Verification Conditions:

Then branch: {x ≥ y} max := x {max = max(x, y)}
- WP: x = max(x, y)
- Verify: x ≥ y ⟹ x = max(x, y) ✓
Else branch: {x < y} max := y {max = max(x, y)}
- WP: y = max(x, y)
- Verify: x < y ⟹ y = max(x, y) ✓

Isabelle Proof:

isabelle

lemma max_correct:
  "⦃λs. True⦄
   If (λs. s ''x'' ≥ s ''y'')
   Then max := (λs. s ''x'')
   Else max := (λs. s ''y'')
   ⦃λs. s ''max'' = max (s ''x'') (s ''y'')⦄"
proof (rule hoare_if)
  show "⦃λs. s ''x'' ≥ s ''y''⦄
        max := (λs. s ''x'')
        ⦃λs. s ''max'' = max (s ''x'') (s ''y'')⦄"
    by (rule hoare_conseq[OF hoare_asgn]) simp
next
  show "⦃λs. ¬(s ''x'' ≥ s ''y'')⦄
        max := (λs. s ''y'')
        ⦃λs. s ''max'' = max (s ''x'') (s ''y'')⦄"
    by (rule hoare_conseq[OF hoare_asgn]) simp
qed

Coq Proof:

coq

Example max_correct :
  {{ fun st => True }}
  if x >= y then
    max ::= x
  else
    max ::= y
  {{ fun st => st max = max (st x) (st y) }}.
Proof.
  apply hoare_if.
  - eapply hoare_consequence_pre.
    + apply hoare_asgn.
    + intros st H. simpl. lia.
  - eapply hoare_consequence_pre.
    + apply hoare_asgn.
    + intros st H. simpl. lia.
Qed.

Show full SKILL.md (287 more words)Show less

Common Patterns

Pattern: Sequential Assignments

Program: x := E1; y := E2; z := E3

Strategy: Work backwards with weakest precondition

Pattern: Accumulation Loop

Program: result := init; while i < n do result := f(result, a[i]); i := i + 1

Invariant: result = fold(f, init, a[0..i-1]) ∧ 0 ≤ i ≤ n

Pattern: Search Loop

Program: found := false; while i < n && !found do if a[i] == target then found := true else i := i + 1

Invariant: (∀j. 0 ≤ j < i ⟹ a[j] ≠ target) ∧ 0 ≤ i ≤ n

Pattern: Nested Loops

Program: Outer loop with inner loop

Invariants: Outer invariant + inner invariant (may depend on outer variables)

Correctness Types

Partial Correctness

Definition: If precondition holds and program terminates, postcondition holds

Hoare triple: {P} C {Q}

What to prove:

Initialization
Preservation
Postcondition follows from invariant

Total Correctness

Definition: If precondition holds, program terminates AND postcondition holds

Hoare triple: [P] C [Q] (square brackets)

What to prove:

Everything from partial correctness
Termination via variant function

Variant requirements:

Non-negative when loop condition holds
Strictly decreases each iteration

References

Detailed guides for program verification:

hoare_logic.md: Complete Hoare logic rules, weakest preconditions, and verification condition generation
verification_patterns.md: Common verification patterns with complete proofs in Isabelle and Coq

Load these references when:

Need detailed Hoare logic rules
Working with complex loop invariants
Generating verification conditions
Need example proofs for similar programs

Tips

Start simple: Verify assignments and sequences before loops
Generalize postcondition: Often leads to good loop invariants
State partial progress: Invariant should express what's computed so far
Include bounds: Always include loop counter bounds in invariant
Work backwards: Use weakest precondition for simple programs
Test invariant: Check initialization, preservation, and postcondition
Choose simple variants: n - i is often sufficient for termination
Use automation: Let simp/auto handle arithmetic when possible

Files

SKILL.md and 2 other files (references) in skills/program-correctness-prover of ArabelaTso/Skills-4-SE.

SKILL.md
references/hoare_logic.md
references/verification_patterns.md

Open the folder on GitHubat commit 4f38503

Compare with similar skills

Program Correctness Prover next to the 5 skills that share the most tags, products or categories with it. Stars are the repository's; “used in” counts other GitHub owners with a copy.

Program Correctness Prover compared with similar skills
Skill	Stars	Used in	Tokens	Auto-check	Licence	Repo updated
Program Correctness Prover this skillArabelaTso/Skills-4-SE	253	—	~2.5k	Automated safety check: Pass	Apache-2.0	1 mo ago
Audit Correctness Proofben-manes/caffeine	18k	—	~275	Automated safety check: Pass	Apache-2.0	2 days ago
Correctcursor/plugins	10k	3 repos	~612	Automated safety check: Pass	None	yesterday
CorrectionNxcoreAI/EverRoom	3k	—	~290	Automated safety check: Pass	Custom licence	yesterday
Implementing Zero Knowledge Proof For Authenticationmukul975/Anthropic-Cybersecurity-Skills	34k	—	~858	Automated safety check: Pass	Apache-2.0	1 mo ago
Rigorous Math Prooftradecatlabs/vibe-coding-cn	17k	—	~571	Automated safety check: Pass	MIT	6 days ago

Similar skills

Audit Correctness Proof
ben-manes/caffeine
Attempt formal correctness proofs for all public cache methods
18k GitHub stars~275 tokensUpdated 2 days ago
Auto-check passed
Correct
cursor/plugins
Official
Find the mistakes agents keep repeating in this repo and make each one impossible.
10k GitHub starsUsed in 3 repos~612 tokens
Auto-check passed
Correction
NxcoreAI/EverRoom
Compute Room overview corrections—citation corrections as per-claim edits and general corrections as a single proposal.
3k GitHub stars~290 tokensUpdated yesterday
Research & ScienceAuto-check passed
Implementing Zero Knowledge Proof For Authentication
mukul975/Anthropic-Cybersecurity-Skills
Implements the Schnorr identification protocol and a simplified Zero-Knowledge Password Proof (ZKPP) over the discrete logarithm problem, letting a prover authenticate by demonstrating knowledge of…
34k GitHub stars~858 tokensUpdated 1 mo ago
SecurityAuto-check passed
Rigorous Math Proof
tradecatlabs/vibe-coding-cn
Writes and audits natural-language math proofs as checkable packages, with explicit assumptions, proof obligations and counterexample hunting, refuting or repairing weak claims.
17k GitHub stars~571 tokensUpdated 6 days ago
Research & ScienceAuto-check passed
Proof Checker
wanshuiyin/Auto-claude-code-research-in-sleep
Rigorous mathematical proof verification and fixing workflow.
17k GitHub starsUsed in 1 repo~7.3k tokens
Documents & OfficeAuto-check: notes

Questions about Program Correctness Prover

What does Program Correctness Prover do?

Generate Isabelle or Coq proofs establishing partial or total correctness of imperative programs from code and formal specifications. Program Correctness Prover is an agent skill from ArabelaTso/Skills-4-SE. Generate Isabelle or Coq proofs establishing partial or total correctness of imperative programs from code and formal specifications.

When should I use Program Correctness Prover?

Program Correctness Prover fits situations like: prove program correctness using Hoare logic; generate verification conditions from pre/postconditions; construct loop invariants and termination arguments; verify imperative programs with assignments.

How do I install Program Correctness Prover in Claude Code?

Run `npx skills add ArabelaTso/Skills-4-SE --skill program-correctness-prover -a claude-code`. Or copy the skill folder (skills/program-correctness-prover in ArabelaTso/Skills-4-SE) into .claude/skills/program-correctness-prover in your project. Claude Code loads it when a task matches its description.

How do I install Program Correctness Prover in Codex?

Run `npx skills add ArabelaTso/Skills-4-SE --skill program-correctness-prover -a codex`. Or copy the skill folder (skills/program-correctness-prover in ArabelaTso/Skills-4-SE) into .agents/skills/program-correctness-prover in your project. Codex loads it when a task matches its description.

Can I use Program Correctness Prover in Cursor, Gemini CLI or GitHub Copilot?

Cursor, Gemini CLI, GitHub Copilot and OpenCode also load SKILL.md folders. With the skills CLI, run `npx skills add ArabelaTso/Skills-4-SE --skill program-correctness-prover -a cursor` (or -a gemini-cli, github-copilot or opencode for the others). To copy it by hand, put the folder in .cursor/skills/program-correctness-prover, .gemini/skills/program-correctness-prover, .github/skills/program-correctness-prover and .opencode/skills/program-correctness-prover in your project.

What does Program Correctness Prover need to run?

SKILL.md names no scripts, command-line tools or credentials: Program Correctness Prover is instructions for the agent only.

Does Program Correctness Prover access the network?

SKILL.md contains no URLs. Any network use would come from the scripts or tools the agent runs. This is read from the text; nothing was executed.

Is Program Correctness Prover safe to install?

Our automated static check of SKILL.md found no risky patterns, such as piping downloads into a shell, reading credential files or hidden Unicode. It is not a guarantee. Review the folder before installing.

What licence does Program Correctness Prover use?

Program Correctness Prover is published under the Apache-2.0 licence (the repository's licence). It allows redistribution, so the full SKILL.md is shown on this page.

How many tokens does Program Correctness Prover use?

About 2.5k tokens (SKILL.md is roughly 9.8k characters). Agents keep only the skill's name and description in context until a task matches; then they load SKILL.md in full. Its references folder adds about 4.3k tokens, read only when the agent opens those files.

What are the alternatives to Program Correctness Prover?

Skills that share tags, products or a category with Program Correctness Prover: Audit Correctness Proof (ben-manes/caffeine, 18k stars), Correct (cursor/plugins, 10k stars), Correction (NxcoreAI/EverRoom, 3k stars) and Implementing Zero Knowledge Proof For Authentication (mukul975/Anthropic-Cybersecurity-Skills, 34k stars). The comparison table on this page puts their stars, adoption, token cost, safety result and licence side by side.

Who maintains Program Correctness Prover?

ArabelaTso (a GitHub user) maintains it in ArabelaTso/Skills-4-SE, which has 253 GitHub stars. The repository holds 151 skills in this directory. The repository was last updated on August 21, 2026.

Source: ArabelaTso/Skills-4-SE on GitHub. Facts on this page come from the repository at the commit we read; the author's words are quoted as theirs.

Install Program Correctness Prover

Facts

At a glance

What it does

When your agent uses it

Example prompts

Workflow steps

What it can do on your machine

Tool permissions

Runs code

Network

Credentials

Context cost

Safety

SKILL.md

Program Correctness Prover

Overview

How to Use

Verification Workflow

Step 1: Analyze Program Structure

Step 2: Generate Loop Invariants

Step 3: Generate Verification Conditions

Step 4: Construct Proof

Step 5: Add Termination Argument (Total Correctness)

Example: Sum of Array

Example: Maximum of Two Numbers

Common Patterns

Pattern: Sequential Assignments

Pattern: Accumulation Loop

Pattern: Search Loop

Pattern: Nested Loops

Correctness Types

Partial Correctness

Total Correctness

References

Tips

Files

Compare with similar skills

Similar skills

More from ArabelaTso/Skills-4-SE

Questions about Program Correctness Prover