# Coq Proof Assistant

> Interface with Coq proof assistant for formal verification

- Skill: `a5c-ai/coq-proof-assistant` (Agent Skill)
- Install (CLI): `npx skillmds@latest add a5c-ai/coq-proof-assistant`
- Raw SKILL.md: https://api.skillmd.com/api/skills/a5c-ai/coq-proof-assistant/raw
- Safety review: pending (external: skill-scanner PASS, skillspector PASS)
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: a5c-ai (https://skillmd.com/u/a5c-ai)
- Updated: 2026-09-09
- Page: https://skillmd.com/skills/a5c-ai/coq-proof-assistant

---


# 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