OpenSkillIndex← back to search
claude-codescience

Babysitter coq-proof-assistant

Interface with Coq proof assistant for formal verification

install
source · Clone the upstream repo
git clone https://github.com/a5c-ai/babysitter
Claude Code · Install into ~/.claude/skills/
T=$(mktemp -d) && git clone --depth=1 https://github.com/a5c-ai/babysitter "$T" && mkdir -p ~/.claude/skills && cp -r "$T/library/specializations/domains/science/mathematics/skills/coq-proof-assistant" ~/.claude/skills/a5c-ai-babysitter-coq-proof-assistant && rm -rf "$T"
manifest: library/specializations/domains/science/mathematics/skills/coq-proof-assistant/SKILL.md
tags
#coq#theorem-proving#formal-verification#mathematics#proof-assistant
source content

Coq Proof Assistant

Purpose

Provides expert guidance on using the Coq proof assistant for formal verification and mathematical formalization.

Capabilities

  • Ltac and Ltac2 tactic generation
  • SSReflect/MathComp library integration
  • Proof by reflection techniques
  • Extraction to OCaml/Haskell
  • Proof documentation generation

Usage Guidelines

  1. Proof Scripts: Write Coq vernacular with proper structuring
  2. Tactics: Use Ltac macros for proof automation
  3. Libraries: Leverage MathComp for algebra and SSReflect for reasoning
  4. Extraction: Generate verified executable code

Tools/Libraries

  • Coq
  • SSReflect
  • MathComp
  • CoqIDE or VS Code