Skip to main content
// install

Two ways in.

Use the package if you're using LemmaScript.
Use the kit if you're changing LemmaScript.

// recommended for getting started quickly

npm package

The standard setup: the lsc toolchain from npm, plus the skills that teach your agent to drive it.

  1. 1

    Check the prerequisites

    Node ≥ 18, Dafny ≥ 4.x (the engine that does the checking), and git.

    terminal
    $ node -v          # ≥ 18
$ dafny --version  # ≥ 4.x
  2. 2

    Install the package

    One global install puts lsc and companions like lsc claimcheck — on your PATH.

    terminal
    $ npm install -g lemmascript
  3. 3

    Add the skills

    Mount the skills repo at your agent's skills directory (e.g. .claude/skills for Claude Code). Your agent picks them up and drives the whole loop itself.

    terminal
    $ git clone https://github.com/midspiral/lemmascript-skills <your/skills/dir>
  4. 4

    Check something

    Point it at a file or at your whole project.

    terminal
    $ lsc check --backend=dafny path/to/file.ts
// recommended for working on the toolchain itself

From source: lemmascript-kit

Working on the toolchain itself, or want the tools and skills pinned together? The kit bundles the toolchain source and the skills as git submodules. One clone, one setup script, skills already in place.

  1. 1

    Clone the kit

    It uses submodules, so clone recursively, then bootstrap.

    terminal
    $ git clone --recurse-submodules https://github.com/midspiral/lemmascript-kit.git
$ cd lemmascript-kit
$ ./setup.sh
  2. 2

    Run from source

    The same commands, straight out of the source tree. The skills write the CLI as npx lsc — in the kit, substitute this form (or npm link the package).

    terminal
    $ npx tsx ../LemmaScript/tools/src/lsc.ts check --backend=dafny path/to/file.ts
i
Skills included. The kit already mounts the skills at .claude/skills/ — no separate step. Updating either piece is normal git discipline: bump the submodule, review the diff.

From here: the full reference, the contract language, and everything that snaps onto the core.

Read the docs → Explore the ecosystem