Setup & Installation
Or with the ClawHub CLI, for registry-managed skill folders outside a full OpenClaw workspace:
What This Skill Does
Acorn Prover integrates the Acorn theorem prover into an AI agent workflow for writing and verifying formal proofs. It supports mathematical and cryptographic protocol formalization using Acorn's language and standard library. Handles verification, CI reverification, training data generation, and documentation generation.
Automates the verify-debug-iterate loop with direct CLI integration, so proof errors surface immediately without manual command construction.
When to use it
- Verifying a cryptographic protocol proof in an .ac file
- Running proof verification in a CI/CD pipeline
- Formalizing natural number theorems using acornlib
- Generating training data pairs from existing proofs
- Producing reference docs from the Acorn standard library
Example Workflow
Here's how your AI assistant might use this skill in practice.
User asks: verify my proof in group_theory.ac
- 1Source config.env to load ACORN_LIB and ACORN_PROJECT paths
- 2Check USE_MISE flag to select correct command variant
- 3Run acorn verify group_theory.ac against the configured library path
- 4Display full command output to the user
- 5If errors appear, consult syntax.md error table and suggest fixes
Verification result shown in full, with error diagnostics if the proof fails
Requirements
Accounts, API keys, or tools you or your AI assistant may need to set up while using this skill.