✓ Verified ✍️ Content Creation ✓ Enhanced Data

Acorn Prover

Verify and write proofs using the Acorn theorem prover for mathematical and cryptographic formalizat

Rating: 4.2 (309 reviews)
Downloads: 1,403 downloads
Version: 1.0.0

Overview

Verify and write proofs using the Acorn theorem prover for mathematical and cryptographic formalization.

Complete Documentation

View Source →

Acorn Prover

Setup (MUST DO WHEN RUNNING FIRST TIME)

If config.env does not exist in the skill directory:

Ask the user for the following paths:
ACORN_LIB - Path to acornlib (e.g., /path/to/acornprover/acornlib)
ACORN_PROJECT - Path to project directory for .ac files (e.g., /path/to/acorn-playground)
Verify the paths exist using list_dir or equivalent. If a path is invalid, inform the user and ask again.
Run setup.sh with the validated paths:

bash

bash skills/acorn-prover/scripts/setup.sh "<ACORN_LIB>" "<ACORN_PROJECT>"

Source the config to get ACORN_LIB, ACORN_PROJECT, and USE_MISE variables:

bash

source skills/acorn-prover/config.env

If any of the above are blank / not set, inform the user to set the variable manually. If any of the above are changed, ask the user for new paths and run setup again.

Configuration

Config values are stored in skills/acorn-prover/config.env:

Variable	Description
ACORN_LIB	Path to acornlib
ACORN_PROJECT	Project directory for .ac files
USE_MISE	true if mise is available

Verify Proofs

If USE_MISE=true:

bash

mise run acorn verify <filename>.ac

Otherwise, use the direct CLI:

bash

acorn --lib "$ACORN_LIB" verify <filename>.ac

Reverify Proofs (CI/CD)

Check that all proofs are cached with no AI searches required:

bash

# With mise
mise run acorn reverify

# Or direct CLI
acorn --lib "$ACORN_LIB" reverify

Use for CI pipelines to ensure all proofs are complete.

Training Data Generation

Generate training data (problem-proof pairs) for AI model development:

bash

# With mise
mise run acorn training ./training_data

# Or direct CLI
acorn --lib "$ACORN_LIB" training ./training_data

Argument: DIR - Directory to output training data.

Documentation Generation

Generate library reference documentation:

bash

# With mise
mise run acorn docs ./docs/library

# Or direct CLI
acorn --lib "$ACORN_LIB" docs ./docs/library

Argument: DIR - Directory to output documentation.

Workflow

Source config: source skills/acorn-prover/config.env
Write proof file in $ACORN_PROJECT/
Run the appropriate command (verify, reverify, training, docs)
Always show the full command output to the user (success or error)
Debug errors using the common errors table in references/syntax.md
Iterate until verification passes

Quick Syntax Overview

acorn

from nat import Nat
from add_comm_group import AddCommGroup

// Theorems - auto-proved or with hints
theorem example(a: Nat, b: Nat) {
    a < b implies a != b
}

// Typeclasses - axioms are named blocks, no "axiom" keyword
typeclass A: AddGroup extends Zero, Neg, Add {
    inverse_right(a: A) { a + -a = A.0 }
}

// Structures
structure Pair[T, U] { first: T  second: U }

// Inductive types - constructors MUST be lowercase
inductive MyBool { tru fls }

Key points:

Built-in logic keywords (not, and, or, implies, iff, true, false) are reserved - do not redefine
Constructor names must be lowercase
Typeclass axioms use named blocks, not the axiom keyword

Standard Library (`acornlib`)

Key modules in $ACORN_LIB/src:

Module	Contents
nat/	Natural number axioms, induction, addition
add_group.ac	AddGroup with a + -a = A.0
add_comm_group.ac	Abelian groups (AddCommGroup)

References

Full syntax, error table, examples: See references/syntax.md
Context7 docs: Use context7 MCP with /acornprover/acorn or /acornprover/acornlib for latest documentation

Installation

Terminal bash


openclaw install acorn-prover

Copied!

💻Code Examples

source skills/acorn-prover/config.env

source-skillsacorn-proverconfigenv.txt

If any of the above are blank / not set, inform the user to set the variable manually.
If any of the above are changed, ask the user for new paths and run setup again.

## Configuration

Config values are stored in `skills/acorn-prover/config.env`:

| Variable        | Description                     |
| --------------- | ------------------------------- |
| `ACORN_LIB`     | Path to acornlib                |
| `ACORN_PROJECT` | Project directory for .ac files |
| `USE_MISE`      | `true` if mise is available     |

## Verify Proofs

If `USE_MISE=true`:

acorn --lib "$ACORN_LIB" verify <filename>.ac

acorn---lib-acornlib-verify-filenameac.txt

## Reverify Proofs (CI/CD)

Check that all proofs are cached with no AI searches required:

acorn --lib "$ACORN_LIB" reverify

acorn---lib-acornlib-reverify.txt

Use for CI pipelines to ensure all proofs are complete.

## Training Data Generation

Generate training data (problem-proof pairs) for AI model development:

acorn --lib "$ACORN_LIB" training ./training_data

acorn---lib-acornlib-training-trainingdata.txt

Argument: `DIR` - Directory to output training data.

## Documentation Generation

Generate library reference documentation:

acorn --lib "$ACORN_LIB" docs ./docs/library

acorn---lib-acornlib-docs-docslibrary.txt

Argument: `DIR` - Directory to output documentation.

## Workflow

1. Source config: `source skills/acorn-prover/config.env`
2. Write proof file in `$ACORN_PROJECT/`
3. Run the appropriate command (verify, reverify, training, docs)
4. **Always show the full command output to the user** (success or error)
5. Debug errors using the common errors table in [references/syntax.md](references/syntax.md)
6. Iterate until verification passes

## Quick Syntax Overview

example.sh

# With mise
mise run acorn reverify

# Or direct CLI
acorn --lib "$ACORN_LIB" reverify

example.sh

# With mise
mise run acorn training ./training_data

# Or direct CLI
acorn --lib "$ACORN_LIB" training ./training_data

example.sh

# With mise
mise run acorn docs ./docs/library

# Or direct CLI
acorn --lib "$ACORN_LIB" docs ./docs/library

example.txt

from nat import Nat
from add_comm_group import AddCommGroup

// Theorems - auto-proved or with hints
theorem example(a: Nat, b: Nat) {
    a < b implies a != b
}

// Typeclasses - axioms are named blocks, no "axiom" keyword
typeclass A: AddGroup extends Zero, Neg, Add {
    inverse_right(a: A) { a + -a = A.0 }
}

// Structures
structure Pair[T, U] { first: T  second: U }

// Inductive types - constructors MUST be lowercase
inductive MyBool { tru fls }