### Install FVS CLI

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/README.md

Run the FVS CLI to start the installation process. This command can be used for initial setup or updating to the latest version.

```bash
npx fv-skills-baif
```

```bash
npx fv-skills-baif@latest
```

--------------------------------

### FVS Configuration - Knowledge Base Setup

Source: https://context7.com/beneficial-ai-foundation/formal-verification-skills/llms.txt

Example JSON structure for configuring knowledge bases within the FVS configuration file.

```json
{
  "model_profile": "quality",
  "knowledge_bases": [
    {
      "name": "crypto-papers",
      "domain": "cryptography",
      "description": "Cryptographic protocol papers and standards"
    }
  ]
}
```

--------------------------------

### Install FVS CLI

Source: https://context7.com/beneficial-ai-foundation/formal-verification-skills/llms.txt

Use npx to install the FVS CLI. Interactive prompts guide runtime and location selection. Options include global or local installation, specifying runtimes (Claude Code, Codex, all), updating, and uninstalling.

```bash
npx fv-skills-baif
```

```bash
npx fv-skills-baif --claude --global
```

```bash
npx fv-skills-baif --codex --global
```

```bash
npx fv-skills-baif --all --global
```

```bash
npx fv-skills-baif --claude --local
```

```bash
npx fv-skills-baif@latest
```

```bash
npx fv-skills-baif --claude --global --uninstall
```

--------------------------------

### Successful KB Setup Summary

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/kb-setup.md

Displays a success summary after the knowledge base setup and test query are completed successfully. It confirms the virtual environment, library, authentication, and knowledge base details.

```text
FVS >> KB SETUP COMPLETE

Venv:     .formalising/.kb-venv/
Library:  notebooklm-py
Auth:     [OK] Authenticated
KB:       {KB_NAME} ({KB_DOMAIN})

Ready to use with /fvs:lean-formalise or any agent.
```

--------------------------------

### Partial KB Setup with Test Query Failure

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/kb-setup.md

Reports a partial setup status when the test query fails, indicating potential issues with the notebook ID or connection. It provides details on the components that passed and the specific error encountered.

```text
FVS >> KB SETUP PARTIAL

Venv:     [OK] .formalising/.kb-venv/
Library:  [OK] notebooklm-py installed
Auth:     [OK] Authenticated
KB:       [!!] Test query failed: {error}

The notebook ID may be incorrect. Check the ID and try:
  /fvs:kb-setup --add
```

--------------------------------

### Get Automation Hints with lean_hammer_premise

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/lean-lsp-mcp.instructions.md

Use `lean_hammer_premise` to get suggestions for lemmas that can be used with the `simp only [...]` tactic. This aids in automating simplification steps.

```shell
lean_hammer_premise
```

--------------------------------

### Setup Aeneas Simps Command

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/tactics-reference.md

Use this command at the top of your proof file to configure simplifier lemmas for code that uses `getElem!`.

```lean
#setup_aeneas_simps
```

--------------------------------

### Check Prerequisites with UV and .formalising Directory

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/kb-setup.md

Checks if 'uv' is installed and if the '.formalising' directory exists. If '.formalising' does not exist, it is created.

```bash
# Check uv is installed
command -v uv && echo "UV_OK" || echo "UV_MISSING"

# Check .formalising/ directory exists
[ -d ".formalising" ] && echo "FORMALISING_OK" || echo "FORMALISING_MISSING"
```

```bash
mkdir -p .formalising
```

--------------------------------

### Install NotebookLM and Playwright Dependencies

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/kb-setup.md

Installs the 'notebooklm-py' package with browser support and the 'playwright' Chromium browser, which are necessary for authentication and KB interaction.

```bash
uv pip install "notebooklm-py[browser]" --python .formalising/.kb-venv/bin/python
```

```bash
.formalising/.kb-venv/bin/playwright install chromium
```

--------------------------------

### FVS Configuration - Model Overrides and KBs

Source: https://context7.com/beneficial-ai-foundation/formal-verification-skills/llms.txt

Example FVS configuration file (.formalising/fvs-config.json) showing model profile settings and knowledge base definitions.

```json
// .formalising/fvs-config.json
{
  "model_profile": "quality",
  "model_overrides": {
    "fvs-researcher": "sonnet",
    "fvs-executor": "opus"
  },
  "knowledge_bases": [
    {
      "name": "my-kb",
      "domain": "cryptography",
      "description": "Domain-specific knowledge base"
    }
  ]
}
```

--------------------------------

### Aeneas Project Directory Structure Example

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/aeneas-patterns.md

Provides an example of the typical directory layout for a Lean project generated by the Aeneas pipeline, highlighting auto-generated files and hand-written specification directories.

```text
ProjectRoot/
  lakefile.toml              # Build config; requires aeneas backend
  lean-toolchain             # Lean version pin
  functions.json             # Function metadata index
  extraction_notes.md        # Documents Aeneas limitations encountered

  ProjectName/               # Main Lean library (e.g., Curve25519Dalek/)
    Types.lean               # AUTO-GENERATED: all Rust types
    Funs.lean                # AUTO-GENERATED: all Rust function bodies
    TypesExternal.lean       # Stubs for opaque external types
    FunsExternal.lean        # Stubs for opaque external functions
    TypesAux.lean            # Auxiliary type definitions
    Aux.lean                 # Auxiliary lemmas
    Tactics.lean             # Project-specific tactics

    Defs.lean                # Mathematical constants and interpretation functions
    Defs/
      Edwards/
        Representation.lean
        Curve.lean

    Specs/                   # Specification theorems and proofs
      Backend/
        Serial/
          U64/
            Field/
              FieldElement51/
                Add.lean
                Sub.lean
                Mul.lean
                Reduce.lean
                ...
            Scalar/
              Scalar52/
                Add.lean
                MontgomeryMul.lean
                ...
          CurveModels/
            CompletedPoint/
              AsExtended.lean
              ...
      Edwards/
        EdwardsPoint/
          Add.lean
          Double.lean
          ...
      Montgomery/
        MontgomeryPoint/
          Mul.lean
          ...
      Scalar/
        Scalar/
          Reduce.lean
          ...

  Utils/                     # Utility executables (e.g., ListFuns, SyncStatus)
```

--------------------------------

### Lean Specification Example

Source: https://context7.com/beneficial-ai-foundation/formal-verification-skills/llms.txt

Example of a Lean specification file generated by FVS. It includes a natural language description, preconditions, postconditions, and a theorem with a 'sorry' placeholder for the proof.

```lean
import MyProject.Funs
import MyProject.Types

namespace Specs.MyModule

/--
Natural language description of what my_function does.
Preconditions: valid input bounds
Postconditions: result within expected range
-/ 
@[step]
theorem my_function_spec (arg1 : U64) (arg2 : U64) :
    arg1.val + arg2.val < U64.max →
    â?contemporary result, my_function arg1 arg2 = ok result 
      result.val = arg1.val + arg2.val := by
  sorry

end Specs.MyModule

```

--------------------------------

### Public Loop Specification (starts at 0)

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/proof-patterns.instructions.md

This public `@[step]` wrapper instantiates the generalized loop specification (`spec_gen`) at `start = 0`. It is used to derive the final postcondition from the raw postcondition provided by `spec_gen`.

```lean
@[step]
theorem my_loop.spec (out a : Slice Std.U16) (hlen : out.length = a.length) :
  my_loop { start := 0#usize, «end» := out.len } out a ⦃ fun res =>
    res.length = out.length ∧
    ∀ j, j < res.length →
      res[j] = f (a[j]) (out[j]) ⦄ := by
  apply WP.spec_mono
  · apply my_loop.spec_gen <;> agrind   -- instantiate spec_gen at start=0
  · intro res ⟨h1, h2⟩; split_conjs <;> agrind   -- derive final postcondition
```

--------------------------------

### functions.json Metadata Format Example

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/aeneas-patterns.md

Example structure of the functions.json file, which indexes extracted functions with their verification status, source files, Lean names, and dependencies. Key fields track progress and relationships between Rust and Lean code.

```json
{
  "functions": [
    {
      "rust_name": "curve25519_dalek::backend::serial::u64::field::FieldElement51::add",
      "lean_name": "curve25519_dalek.backend.serial.u64.field.FieldElement51.add",
      "source": "curve25519-dalek/src/backend/serial/u64/field.rs",
      "lines": "L120-L135",
      "verified": true,
      "specified": true,
      "fully_verified": true,
      "spec_file": "Curve25519Dalek/Specs/Backend/Serial/U64/Field/FieldElement51/Add.lean",
      "spec_statement": "theorem add_spec ...",
      "spec_docstring": "...",
      "is_relevant": true,
      "is_hidden": false,
      "is_extraction_artifact": false,
      "dependencies": ["...other_lean_function_names..."],
      "nested_children": []
    }
  ]
}
```

--------------------------------

### Two-Phase Dispatch Examples

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/model-profiles.md

Illustrates the sequential dispatch of researcher and executor subagents for various FVS commands. The researcher gathers context, and the executor writes files.

```shell
/fvs:map-code
  -> Task(fvs-researcher, model=resolve("fvs-researcher"), research_mode="map-code")
  -> Task(fvs-executor,   model=resolve("fvs-executor"),   execution_mode="map-code")
```

```shell
/fvs:plan
  -> Task(fvs-researcher, model=resolve("fvs-researcher"), research_mode="plan")
  -> Task(fvs-executor,   model=resolve("fvs-executor"),   execution_mode="plan")
```

```shell
/fvs:lean-specify
  -> Task(fvs-researcher, model=resolve("fvs-researcher"), research_mode="spec-generation")
  -> Task(fvs-executor,   model=resolve("fvs-executor"),   execution_mode="spec-generation")
```

```shell
/fvs:lean-verify
  -> Task(fvs-researcher, model=resolve("fvs-researcher"), research_mode="proof-attempt")
  -> Task(fvs-executor,   model=resolve("fvs-executor"),   execution_mode="proof-attempt")
```

```shell
/fvs:lean-refactor
  -> Task(fvs-researcher,       model=resolve("fvs-researcher"),       research_mode="lean-refactor")
  -> Task(fvs-lean-refactorer,  model=resolve("fvs-lean-refactorer"),  refactor_mode="iterative")
```

--------------------------------

### Decision Tree for Starting a Proof

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/aeneas-lean-core.instructions.md

Follow this decision tree to determine the initial proof strategy based on function structure and complexity.

```text
1. Does the function start with `match`/`if`?
   - YES → `unfold fn; split` then `step` per branch
   - NO → `unfold fn; step`

2. Is the function simple (few monadic steps, say ≤ 5)?
   - YES → `unfold fn; step*` may complete it directly (may take 60–120s on
     larger functions — see "Tactics can take a long time" below). If sub-goals
     remain, **immediately** scaffold one `· agrind` per sub-goal (see scaffolding
     workflow below).
   - NO → Use `step*?` to generate an expanded proof script, then work from there

3. Is the function large/complex (10+ monadic steps)?
   - **First, try to decompose using fold theorems** — extract logical phases
     (setup, hash, finalize) into auxiliary functions with their own
     `@[local step]` specs. Then the parent proof only `step`s through the
     phase calls instead of 50+ monadic operations at once.
   - If decomposition is not feasible (no natural phase boundaries), use
     `step*` to go as far as possible, then **immediately scaffold one `· agrind`
     per remaining sub-goal** — this is mandatory before doing anything else.
   - **⚠️ Before writing cdot blocks: check for missing solver attributes.**
     If 3+ remaining goals need the same constant unfolded (`simp [CONST]; solver`),
     register it with `@[grind =, agrind =]` FIRST, then re-run
     `step*` — the goals may vanish. See the `aeneas-tactics-quickref` skill file.
   - **NEVER use `<;>` after `step*` or any tactic that creates many subgoals.**
     `<;>` forces full re-elaboration on every edit. Use cdot blocks instead.
   - **NEVER use `all_goals`** — it has the same re-elaboration problem.
   - If heartbeats are tight, the function MUST be decomposed (fold theorems)
     — aim for < 8M heartbeats even for large proofs; increase the default
     to 1M as a baseline (see "Debugging Commands" in the tactics quickref)
   - **"Too many monadic steps" is NEVER a reason to skip a proof or axiomatize.**
     It is a reason to decompose via fold theorems.
```

--------------------------------

### Real Example: FieldElement51::add Specification Theorem

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/lean-spec-conventions.md

A concrete implementation of the canonical theorem structure for the `FieldElement51::add` function, showcasing preconditions and postconditions.

```lean
@[step]
theorem add_spec (a b : Array U64 5#usize)
    (ha : ∀ i < 5, a[i]!.val < 2 ^ 53)
    (hb : ∀ i < 5, b[i]!.val < 2 ^ 53) :
    ∃ result, add a b = ok result ∧
    (∀ i < 5, result[i]!.val = a[i]!.val + b[i]!.val) ∧
    (∀ i < 5, result[i]!.val < 2 ^ 54) := by
  unfold add
  step*
```

--------------------------------

### Lean Tactic Usage Guide

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/aeneas-lean-core.instructions.md

Provides a quick reference for commonly used Lean tactics and their intended use cases. Avoid `simp_all` due to performance and hypothesis dropping.

```lean
agrind
```

```lean
grind
```

```lean
simp [*]
```

```lean
tauto
```

```lean
decide
```

--------------------------------

### Loop Entry-Point Specification (Lean)

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/proof-strategies.md

Instantiates the generalized loop specification `spec_gen` at the loop's starting point (index 0). It uses `spec_mono` and delegates to `my_loop.spec_gen`.

```lean
@[step]
theorem my_loop.spec (state : State) :
  my_loop { start := 0#usize, «end» := N } state ⦃ fun result =>
    ∀ j, j < N → processed j result 
⦄ := by
  apply WP.spec_mono
  · apply my_loop.spec_gen <;> agrind
  · intro res h; split_conjs <;> agrind

```

--------------------------------

### Display Verification Summary

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/map-code.md

This summary provides an overview of the formal verification process, including project details, function counts, spec status, and recommended starting points for verification.

```text
FVS >> MAP COMPLETE

Project: [name from directory or config]
Functions: [N] total, [M] leaf functions
Existing specs: [K] files ([J] with sorry remaining)
Recommended starting points: [top 5 leaf functions]

Written: .formalising/CODEMAP.md
```

--------------------------------

### Run Lean Profiler on a Theorem

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/lean-lsp-mcp.instructions.md

Use `lean_profile_proof` to get per-line timing for a specific theorem. This is useful for identifying performance bottlenecks in proofs, but should be used sparingly as it slows down the development process.

```shell
lean_profile_proof(file_path="MyProject/Properties/Foo.lean", line=42)
```

--------------------------------

### File-level Setup and Attribute Registration

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/aeneas-lean-core.instructions.md

This snippet shows how to set up file-level simplifications and register local lemmas for specific tactics like `simp_scalar_simps`, `simp_lists_simps`, and `agrind`. These are safe to activate as they are simp-based and do not cause complexity explosions.

```lean
-- File-level setup for crypto/array proofs
#setup_aeneas_simps
```

```lean
-- Register lemmas for tactics
attribute [local simp_scalar_simps] my_lemma
attribute [local simp_lists_simps] my_lemma
attribute [local agrind] my_lemma
```

--------------------------------

### Simplify list operations with `simp_lists`

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/aeneas-lean-core.instructions.md

Employ `simp_lists` to simplify structural operations on lists and slices, such as `setSlice!`, `replicate`, `append`, `take`, `drop`, `length`, `get`, and `set`. Lemmas can be provided to guide the simplification.

```lean
simp_lists [lemmas]
```

--------------------------------

### Using step* for Automated Proof Script Generation

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/proof-strategies.md

This example demonstrates using `step*` to automatically apply `step` repeatedly and handle branching cases. Use `step*?` to generate the full expanded proof script for review.

```lean
-- Using step* to do most of the work
theorem list_nth_mut1_spec'' {T: Type} [Inhabited T] (l : CList T) (i : U32)
  (h : i.val < l.toList.length) :
  list_nth_mut1 l i ⦃ x back =>
    x = l.toList[i.val]! ∧
    ∀ x', (back x').toList = l.toList.set i.val x' ⦄ := by
  unfold list_nth_mut1 list_nth_mut1_loop
  /- `step*` repeatedly applies `step`, while doing a case disjunction whenever it
      encounters a branching. Note that one can automatically generate the corresponding
      proof script by using `step*?`. -/
  step*
  simp_all
```

--------------------------------

### Detect Installed FVS Version

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/update.md

Checks for local and global FVS installations by looking for the VERSION file. It prioritizes local installations and handles edge cases where the current working directory is the home directory. Outputs the installed version and installation type (LOCAL, GLOBAL, or UNKNOWN).

```bash
# Check local first (takes priority), with path canonicalization
# to prevent misdetection when CWD=$HOME
LOCAL_DIR="" GLOBAL_DIR=""
if [ -f "./.claude/fv-skills/VERSION" ]; then
  LOCAL_DIR="$(cd ./.claude 2>/dev/null && pwd)"
fi
if [ -f "$HOME/.claude/fv-skills/VERSION" ]; then
  GLOBAL_DIR="$(cd "$HOME/.claude" 2>/dev/null && pwd)"
fi

# Only treat as LOCAL if resolved paths differ (handles CWD=$HOME edge case)
if [ -n "$LOCAL_DIR" ] && { [ -z "$GLOBAL_DIR" ] || [ "$LOCAL_DIR" != "$GLOBAL_DIR" ]; }; then
  cat "./.claude/fv-skills/VERSION"
  echo "LOCAL"
elif [ -n "$GLOBAL_DIR" ]; then
  cat "$HOME/.claude/fv-skills/VERSION"
  echo "GLOBAL"
else
  echo "UNKNOWN"
fi
```

--------------------------------

### Set up NotebookLM Knowledge Base Integration

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/help.md

Sets up NotebookLM knowledge base integration. It creates a Python virtual environment, installs necessary libraries, handles interactive login to NotebookLM, and registers the knowledge base with domain tags. The `--add` flag can be used to register additional KBs without recreating the venv.

```APIDOC
## POST /fvs:kb-setup

### Description
Set up NotebookLM knowledge base integration.

### Method
POST

### Endpoint
/fvs:kb-setup

### Parameters
#### Query Parameters
- **--add** (boolean) - Optional - Register additional KBs without recreating venv.

### Response
#### Success Response (200)
- **message** (string) - Confirmation of KB setup.

#### Response Example
```json
{
  "message": "NotebookLM knowledge base integration set up successfully."
}
```
```

--------------------------------

### Non-interactive FVS Installation

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/README.md

Install FVS non-interactively for use in Docker, CI, or scripts. Specify the runtime and installation scope (global or local).

```bash
# Claude Code
npx fv-skills-baif --claude --global   # Install to ~/.claude/
npx fv-skills-baif --claude --local    # Install to ./.claude/
```

```bash
# Codex
npx fv-skills-baif --codex --global    # Install to ~/.codex/
```

```bash
# OpenCode
npx fv-skills-baif --opencode --global # Install to ~/.config/opencode/
```

```bash
# Gemini CLI
npx fv-skills-baif --gemini --global   # Install to ~/.gemini/
```

```bash
# All runtimes
npx fv-skills-baif --all --global      # Install to all directories
```

--------------------------------

### Full Agent Prompt Example (Separate-Clone Mode)

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/launching-proof-agents.instructions.md

This prompt configures an agent for a 'separate-clone' mode, detailing the steps for skill invocation, initial build, and proof checking using lean-lsp-mcp tools. It specifies the target file and the 'sorry' to be fixed.

```text
Fix the inner loop sorry in `/path/to/clone/MyModule.lean`.

## Step 1: Invoke Skills
As your FIRST action, invoke these skills (use the `skill` tool):
1. `aeneas-lean-core` — translation model, spec patterns, pitfalls
2. `aeneas-tactics-quickref` — which tactic for which goal
3. `lean-lsp-mcp` — mandatory tooling for proof checking

## Step 2: ⛔ HARD REQUIREMENT — Initial build + lean-lsp-mcp tools ONLY
As your VERY FIRST action after reading skills, run `lake build` in the Lean
project directory to pre-compile .olean caches. This is required because the
lean-lsp-mcp LSP server will time out on first use if caches are stale.

After the initial build, do ALL proof checking via lean-lsp-mcp tools
(`lean_goal`, `lean_diagnostic_messages`, `lean_multi_attempt`, etc.).
Edit the file on disk, then use `lean_goal` and `lean_diagnostic_messages`
to inspect the result.
Do NOT use `lake build` for iterative proof development — only as (1) the initial
build and (2) a single final verification. Iterative `lake build` = REJECTED.

## The Sorry
`my_function_loop0_loop0_spec` at line ~421.

```

--------------------------------

### Run FVS Update (Global)

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/update.md

Executes the update command for a global FVS installation using `npx`. This is used when FVS is installed system-wide or when the installation type is unknown.

```bash
npx fv-skills-baif@latest --global
```

--------------------------------

### Check Local and Global FVS Installation Version

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/workflows/update.md

Detects if FVS is installed locally or globally by checking for the VERSION file in specific directories. It prioritizes local installations and handles edge cases like the current working directory being the home directory.

```bash
# Check local first (takes priority), with path canonicalization
# to prevent misdetection when CWD=$HOME
LOCAL_DIR="" GLOBAL_DIR=""
if [ -f "./.claude/fv-skills/VERSION" ]; then
  LOCAL_DIR="$(cd ./.claude 2>/dev/null && pwd)"
fi
if [ -f "$HOME/.claude/fv-skills/VERSION" ]; then
  GLOBAL_DIR="$(cd "$HOME/.claude" 2>/dev/null && pwd)"
fi

# Only treat as LOCAL if resolved paths differ (handles CWD=$HOME edge case)
if [ -n "$LOCAL_DIR" ] && { [ -z "$GLOBAL_DIR" ] || [ "$LOCAL_DIR" != "$GLOBAL_DIR" ]; }; then
  INSTALLED=$(cat "./.claude/fv-skills/VERSION")
  echo "$INSTALLED"
  echo "LOCAL"
elif [ -n "$GLOBAL_DIR" ]; then
  INSTALLED=$(cat "$HOME/.claude/fv-skills/VERSION")
  echo "$INSTALLED"
  echo "GLOBAL"
else
  echo "UNKNOWN"
fi
```

--------------------------------

### Scaffolding with `agrind` after `step*`

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/tactic-usage.md

Immediately scaffold `· agrind` after `step*` for each remaining sub-goal. This is the first step before inspecting goals or trying other tactics.

```lean
-- After step*:
step*
· agrind -- goal 1
· agrind -- goal 2
· agrind -- goal 3
```

```lean
-- After split_conjs:
split_conjs
· agrind -- conjunct 1
· agrind -- conjunct 2
```

--------------------------------

### Sorry'd Definition Example: Extraction

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/aeneas-patterns.md

For sorry'd definitions, provide a concrete Lean expression. This example demonstrates extracting a portion of byte data.

```Lean
(arrayToSpecBytes field).extract start len
```

--------------------------------

### Sorry'd Definition Example: Casting with Simp

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/aeneas-patterns.md

Provide a concrete Lean expression for sorry'd definitions. This example illustrates casting using the `simp` tactic.

```Lean
expr.cast (by simp [...])
```

--------------------------------

### Suggest Next Steps: No Change

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/lean-refactor.md

Informs the user that proofs are clean at the current mode's tier ceiling and suggests trying an 'aggressive' mode for further refactoring.

```bash
>> Proofs are already clean at the {mode} tier ceiling.

Try --mode aggressive for more aggressive refactoring.
/fvs:plan to select next verification target
```

--------------------------------

### Display FVS Already Up-to-Date Message

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/update.md

Informs the user that their FVS installation is already at the latest version. This message is displayed when the installed version matches the latest available version.

```markdown
## FVS Update

**Installed:** X.Y.Z
**Latest:** X.Y.Z

You're already on the latest version.
```

--------------------------------

### Step*? Workflow for Proof Development

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/launching-proof-agents.instructions.md

Utilize the `step*?` workflow for developing Lean proofs. This involves writing `step*?`, expanding it with `lean_code_actions`, integrating it into the proof, and refining sub-goals.

```text
### Use step*? to develop proofs

See the `lean-lsp-mcp` skill file for the full step*? workflow.
In short: write `step*?` → `lean_code_actions` on that line to read the expanded
script → copy it into your proof → fix sub-goals → collapse back to `step*` if possible.
```

--------------------------------

### Sorry'd Theorem Example: Tactic Proof

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/aeneas-patterns.md

For sorry'd theorems (`theorem foo := by sorry`), provide a tactic proof. This example shows a basic tactic sequence.

```Lean
by unfold ...; step*; ...
```

--------------------------------

### Sorry'd Definition Example: Casting

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/aeneas-patterns.md

When dealing with sorry'd definitions, a concrete Lean expression is required. This example shows casting an expression using a tactic proof.

```Lean
expr.cast (by scalar_tac)
```

--------------------------------

### Generate Proof Script with step*?

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/proof-strategies.md

Use `step*?` to generate a complete proof script by repeatedly applying `step` with case splits. This outputs a verbose but complete script that can be reviewed and refined.

```lean
theorem list_nth_mut1_spec {T: Type} [Inhabited T] (l : CList T) (i : U32)
  (h : i.val < l.toList.length) :
  list_nth_mut1 l i ⦃ x back =>
    x = l.toList[i.val]! ∧
    ∀ x', (back x').toList = l.toList.set i.val x' ⦄ := by
  unfold list_nth_mut1 list_nth_mut1_loop
  step*
  simp_all
```

--------------------------------

### Run FVS Update (Local)

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/update.md

Executes the update command for a local FVS installation using `npx`. It ensures the latest version of `fv-skills-baif` is installed in the current project's scope.

```bash
npx fv-skills-baif@latest --local
```

--------------------------------

### Generate `let*` script with named bindings using `step*?`

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/aeneas-lean-core.instructions.md

Use `step*?` to generate a proof script with explicit `let*` bindings for all intermediates. This is useful when many hypotheses need named access for complex goals. Note that generated scripts can be significantly slower than `step*`.

```lean
let* ⟨ x2, x2_post ⟩ ← U32.add_spec
let* ⟨ x3, x3_post ⟩ ← foo_spec
let* ⟨ x4 ⟩ ← bar_spec
...
```

--------------------------------

### Step-by-step Proof Generation Workflow

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/aeneas-lean-core.instructions.md

This workflow outlines the process of using `step*?` to generate an expanded proof script, scaffold sub-goals, and then refine the proof.

```text
1. `step*?` — generates expanded proof script (one `step` per monadic call)
2. Copy the generated script into your proof
3. **Immediately scaffold `· agrind` for every sub-goal** that remains open —
   this is the first thing you do after pasting. Do NOT attempt to close any
   goal before all are scaffolded.
4. Work through each `· agrind` one at a time: if `agrind` didn't close a goal, inspect with `lean_goal`, pick the right tactic, and replace
5. Once the full proof works, try collapsing sections back to `step*`
6. If `step*` works on the whole body, use that (shorter is better)
7. If not, keep the expanded script for the parts that need manual intervention
```

--------------------------------

### Example of Explicit Conflict Check Statement

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/agent-fleet-management.instructions.md

State conflict checks explicitly before launching agents to ensure parallelization safety. This example demonstrates a clear statement indicating no mutual dependencies.

```lean
"CT.lean imports Defs.lean, MulBS.lean imports MatDefs.lean — no mutual
dependencies, safe to parallelize."
```

--------------------------------

### Exploratory Tactic: Apply?

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/aeneas-patterns.md

Employ `apply?` to find suitable lemmas or theorems that can be applied to the current proof state. This aids in discovering correct lemma names.

```Lean
apply?
```

--------------------------------

### Scaffolding Goals After `step*`

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/aeneas-lean-core.instructions.md

Immediately after using `step*`, scaffold each remaining sub-goal with `agrind`. This is the first step before inspecting or attempting other tactics.

```lean
-- After step*:
step*
· agrind -- goal 1
· agrind -- goal 2
· agrind -- goal 3
· agrind -- goal 4
```

--------------------------------

### Configure Knowledge Base Integration - FVS

Source: https://context7.com/beneficial-ai-foundation/formal-verification-skills/llms.txt

Sets up NotebookLM knowledge base integration, including Python virtual environment, authentication, and KB registration.

```bash
# Interactive KB setup
/fvs:kb-setup
```

--------------------------------

### Exploratory Tactic: Simp?

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/aeneas-patterns.md

Utilize `simp?` to explore simplification lemmas applicable to the current goal. This is helpful for discovering relevant lemmas without guessing.

```Lean
simp?
```

--------------------------------

### Sorry'd Definition Example: Byte Assembly

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/aeneas-patterns.md

When defining a sorry'd definition (`def foo := sorry`), provide a concrete Lean expression. This example shows composing conversion functions to create byte data.

```Lean
arrayToSpecBytes field1 ++ arrayToSpecBytes field2
```

--------------------------------

### Setting up Aeneas Simplifications in Lean

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/upstream/aeneas/proof-strategies.md

Use `#setup_aeneas_simps` to configure Aeneas simplifications. This deactivates lemmas that convert `getElem!` to `getElem?`/`getD` and activates lemmas that convert `getElem` to `getElem!` and `set` to `set!`.

```lean
#setup_aeneas_simps

-- Now getElem! is the preferred access pattern
```

--------------------------------

### Port Proofs from Other Languages to Lean

Source: https://context7.com/beneficial-ai-foundation/formal-verification-skills/llms.txt

Ports formal verification proofs from other languages to Lean, using the source proof as a strategy blueprint. Supports interactive porting, scan mode for comparison, and custom max attempts.

```bash
# Interactive proof porting
/fvs:lean-proof-port
```

```bash
# With scan mode for comparison table
/fvs:lean-proof-port --scan
```

```bash
# With custom max attempts
/fvs:lean-proof-port --max-attempts 20
```

--------------------------------

### Extract Changelog Entries

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/update.md

Parses the downloaded `CHANGELOG.md` content to extract specific version entries. It uses `sed` to find lines between the latest version header and the installed version header, excluding the installed version header itself. Assumes changelog headers follow the format `## [VERSION] - YYYY-MM-DD`.

```bash
# CHANGELOG uses headers like: ## [1.1.0] - 2026-03-09
# Extract everything from latest version header up to (but excluding) installed version header
echo "$CHANGELOG" | sed -n "/^## \[${LATEST}\]/ sum /^## \[${INSTALLED}\]/p" | sed '$d'
```

--------------------------------

### General FVS Commands

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/README.md

Framework-agnostic FVS commands for dependency mapping, verification planning, natural language explanations, and help.

```bash
/fvs:map-code
```

```bash
/fvs:plan
```

```bash
/fvs:natural-language
```

```bash
/fvs:help
```

```bash
/fvs:update
```

```bash
/fvs:reapply-patches
```

```bash
/fvs:sync-aeneas
```

--------------------------------

### Display Dispatch Indicator

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/map-code.md

This output indicates the start of the fvs-researcher agent dispatch process.

```text
>> Dispatching fvs-researcher (map-code)...
```

--------------------------------

### FVS Configuration File Example

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/model-profiles.md

The `.formalising/fvs-config.json` file specifies the active model profile and allows for model overrides for specific agents. If the file is missing, commands default to the 'quality' profile.

```json
{
  "model_profile": "quality",
  "model_overrides": {}
}
```

--------------------------------

### Display Executor Dispatch Indicator

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/commands/fvs/map-code.md

This output indicates the start of the fvs-executor agent dispatch process.

```text
>> Dispatching fvs-executor (map-code)...
```

--------------------------------

### Stage Banner Example

Source: https://github.com/beneficial-ai-foundation/formal-verification-skills/blob/main/fv-skills/references/ui-brand.md

Use this banner for major workflow transitions in FVS. Stage names should be in uppercase.

```text
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
 FVS >> {STAGE NAME}
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
```