acorn-prover

---
name: acorn-prover
description: "Verify and write proofs using the Acorn theorem prover for mathematical and cryptographic formalization. Use when working with Acorn proof files (.ac), verifying theorems, formalizing mathematical or cryptographic protocols, or writing proofs in the Acorn language. Triggers on: (1) Creating or editing .ac files, (2) Running acorn verify commands, (3) Formalizing math or crypto proofs, (4) Questions about Acorn syntax or standard library."
---

# Acorn Prover

## Setup (MUST DO WHEN RUNNING FIRST TIME)

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

1. **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`)

2. **Verify** the paths exist using `list_dir` or equivalent. If a path is invalid, inform the user and ask again.

3. **Run setup.sh** with the validated paths:

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

4. **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 requi