Skillget

lemmafit

skill
Security Audit
Fail
Health Pass
  • License — License: MIT
  • Description — Repository has a description
  • Active repo — Last push 0 days ago
  • Community trust — 37 GitHub stars
Code Fail
  • child_process — Shell command execution capability in cli/check-claimcheck.js
  • execSync — Synchronous shell command execution in cli/check-claimcheck.js
  • process.env — Environment variable access in cli/check-claimcheck.js
  • fs module — File system access in cli/context-hook.js
Permissions Pass
  • Permissions — No dangerous permissions requested
Purpose
This tool integrates Dafny formal verification into development workflows, forcing AI coding agents to mathematically prove their logic is correct before compiling it into TypeScript for use in applications.

Security Assessment
The scan identified a couple of notable security flags. The tool actively executes synchronous and asynchronous shell commands in its `check-claimcheck.js` file to interact with the Dafny compiler. It also accesses system environment variables and reads from the file system to monitor and compile your project files. No hardcoded secrets or dangerous network requests were found, and it does not request broad system permissions. Because the tool is designed to act as a system daemon that watches files and executes local binaries, these code behaviors are functionally expected for its core features. Overall risk is rated as Medium, primarily because running external shell commands always requires a degree of caution regarding untrusted inputs.

Quality Assessment
The project is actively maintained, with its most recent code push occurring today. It utilizes the highly permissive MIT license and clearly outlines its intended use cases. However, community trust and adoption remain quite low at only 37 GitHub stars, indicating it is likely an early-stage or niche project.

Verdict
Use with caution — the shell execution features behave exactly as required by its design, but its low community adoption signals that the project is still in its early stages.
SUMMARY

Make agents prove that their code is correct.

README.md

lemmafit

Make agents prove that their code is correct.

Read our launch post: Introducing lemmafit: A Verifier in the AI Loop.

Lemmafit integrates Dafny formal verification into your development workflow via Claude Code. Business logic, state machines, and other logic are written in Dafny, mathematically verified, then auto-compiled to TypeScript for use in your React app.

Quick Start

# Install lemmafit globally
npm install -g lemmafit

# Create a new project
lemmafit init PROJECT_NAME
cd PROJECT_NAME

# Install deps (downloads Dafny automatically)
npm install

# In one terminal, start the verification daemon
npm run daemon

# In another terminal, start the Vite dev server
npm run dev

# In a third terminal, open Claude Code
claude

Use Cases / Considerations

  • lemmafit works with greenfield projects. You typically begin a project with lemmafit init though lemmafit add provides rudimentary support for existing codebases.

  • lemmafit compiles Dafny to Javascript/Typescript which then hooks into a runtime like a React app. In the future, we will support other languages.

  • lemmafit is optimized to work with Claude Code. In the future, lemmafit will be agent-agnostic.

How It Works

  1. Prompt Claude Code as you normally would. You may use a simple starting prompt or a structured prompting system.
    Example: "Create a pomodoro app I can use personally and locally."
  2. The agent will write a SPEC.yaml and write verified logic in lemmafit/dafny/Domain.dfy
  3. The daemon watches .dfy files, runs dafny verify, and on success compiles to src/dafny/Domain.cjs + src/dafny/app.ts
  4. The agent will hook the generated TypeScript API into a React app — the logic is proven correct
  5. After proofs complete, run the /guarantees skill to activate claimcheck and generate a guarantees report

Project Structure

my-app/
├── SPEC.yaml                    # Your requirements
├── lemmafit/
│   ├── dafny/
│   │   └── Domain.dfy           # Your verified Dafny logic
│   │   └── Replay.dfy           # Generic Replay kernel
│   ├── .vibe/
│   │   ├── config.json           # Project config
│   │   ├── modules.json          # Module registry (for multi-module projects)
│   │   ├── status.json           # Verification status (generated)
│   │   └── claims.json           # Proof obligations (generated)
│   └── reports/
│       └── guarantees.md         # Guarantee report (generated)
├── src/
│   ├── dafny/
│   │   ├── Domain.cjs            # Compiled JS (generated)
│   │   └── app.ts                # TypeScript API (generated - DO NOT EDIT)
│   ├── App.tsx                   # Your React app
│   └── main.tsx
├── .claude/                      # Hooks & settings (managed by lemmafit)
└── package.json

CLI

lemmafit init [dir]                # Create project from template
lemmafit add [Name]                # Add a verified module to an existing project
lemmafit sync [dir]                # Re-sync system files (.claude/, hooks)
lemmafit daemon [dir]              # Run verification daemon standalone
lemmafit logs [dir]                # View daemon log
lemmafit logs --clear [dir]        # Clear daemon log

Updating

System files sync automatically on install:

npm update lemmafit
# postinstall re-syncs .claude/settings.json, hooks, and instructions

Requirements

  • Node.js 18+
  • Claude Code CLI
  • claimcheck (npm install -g claimcheck) — needed for the /guarantees skill

Dafny and dafny2js are downloaded automatically during npm install to ~/.lemmafit/.

Reviews (0)

No results found