🎩 You're Invited:Meet the Socket team at Black Hat in Las Vegas, August 3-6.RSVP →
Sign In

lemmafit

Package Overview
Dependencies
Maintainers
3
Versions
12
Alerts
File Explorer

Advanced tools

License
Socket logo

Install Socket

Detect and block malicious and high-risk dependencies

Install

lemmafit - npm Package Compare versions

Comparing version
0.2.0
 to
0.2.1
+143
skills/lemmafit-guarantees/SKILL.md
---
name: lemmafit-guarantees
description: Generate human-readable guarantees from proven Dafny code and verify them with claimcheck. Use after verification succeeds and SPEC.yaml is in sync with Dafny. Produces guarantees.json, claimcheck-mapping.json, runs claimcheck-multi, and generates guarantees.md report.
---
# Generate Guarantees and Run Claimcheck
You are generating human-readable guarantees from proven Dafny code and verifying them with claimcheck.
## Step 0: Make sure the state of the project is verified
Check your context for verification status of the project.
## Step 1: Read project data
Read these files:
- `lemmafit/.vibe/claims.json` — extracted proof obligations from Dafny (predicates with conjuncts, lemmas with requires/ensures, functions with contracts, axioms)
- `SPEC.yaml` — natural language requirements with spec entries
- `lemmafit/dafny/Domain.dfy` — the Dafny source code
- `lemmafit/.vibe/config.json` — project config (need `appCore` field for claimcheck domain)
If `claims.json` doesn't exist, tell the user to run the daemon first (`npm run daemon` or `npm run dev`) so Dafny verification produces claims.
## Step 2: Map claims to spec entries
Analyze the claims from `claims.json` and map them to spec entries from `SPEC.yaml`.
**How claims work:**
- **Predicate conjuncts** (in `predicates[].conjuncts`) are invariant properties proven by the `StepPreservesInv` lemma. Each conjunct in the `Inv` predicate is a separate proven property.
- **Lemma ensures** (in `lemmas[].ensures`) are standalone proven properties. The lemma name is in `lemmas[].name`.
- **Function contracts** (in `functions[].requires` and `functions[].ensures`) are proven pre/postconditions.
- **Axioms** (in `axioms[]`) are assumed, NOT proven — they represent the trust surface.
**Mapping rules:**
- A claim "covers" a spec entry if the Dafny expression proves the property described by that spec entry
- One claim can cover multiple spec entries
- Spec entries with `status: trusted` don't need covering claims
- Spec entries with `verifiable: false` should be skipped
- Identify **gaps**: spec entries with `status: verified` that have NO covering claim
## Step 3: Write guarantees.json
Write `reports/guarantees.json` with this format:
```json
{
"generatedAt": "<ISO timestamp>",
"guarantees": [
{
"specId": "spec-001",
"requirement": "<title from SPEC.yaml>",
"status": "proven",
"coveredBy": [
{
"claimId": "inv:<Module>.<Predicate>:<conjunctIndex>",
"type": "invariant-conjunct",
"expression": "<the Dafny expression>",
"lemmaName": "StepPreservesInv"
}
],
"reasoning": "<why this claim covers this spec entry>"
}
],
"gaps": [
{
"specId": "spec-005",
"requirement": "<title>",
"reason": "<why no claim covers this>"
}
]
}
```
For `lemmaName`:
- Invariant conjuncts → `"StepPreservesInv"`
- Lemma ensures → the lemma's name (e.g. `"UndoReversesLast"`)
- Function contracts → the function's name
## Step 4: Handle multi-lemma requirements
If a single requirement is covered by **multiple** lemmas (e.g. an invariant conjunct AND a standalone lemma together prove one requirement), you must write a **new wrapper lemma** in the Dafny source that proves the full requirement in one place. The wrapper lemma should:
- Have a name that clearly describes the requirement (e.g. `Guarantee_UniqueUpvotes`)
- Call/use the individual lemmas as needed
- Have an `ensures` clause that directly expresses the full natural-language requirement
This is necessary because claimcheck needs exactly one lemma per requirement to verify faithfulness.
Wait for the daemon to re-verify after writing any new lemmas before proceeding.
## Step 5: Write claimcheck mapping
Write `lemmafit/.vibe/claimcheck-mapping.json` — an array of `{ requirement, lemmaName, file }` objects derived from the guarantees. The `file` field is a **path relative to the mapping file** (i.e. relative to `lemmafit/.vibe/`).
```json
[
{ "requirement": "Each user can only upvote once", "lemmaName": "Guarantee_UniqueUpvotes", "file": "../dafny/Domain.dfy" }
]
```
Each requirement should map to exactly one lemma. If you wrote wrapper lemmas in step 4, use those.
## Step 6: Run claimcheck
Run `claimcheck-multi` to verify that each lemma faithfully expresses its requirement.
**CRITICAL: claimcheck-multi MUST run in the background with output redirected to files.** It spawns `claude -p` as a subprocess, which will hang indefinitely if run in the foreground from a Claude Code session. Always use `&` and redirect stdout/stderr:
```bash
claimcheck-multi -m lemmafit/.vibe/claimcheck-mapping.json -d <appCore> --json --claude-code > lemmafit/.vibe/claimcheck.json 2> lemmafit/.vibe/claimcheck-err.log &
```
Replace `<appCore>` with the value from `lemmafit/.vibe/config.json`.
No `--dfy` flag needed — `claimcheck-multi` resolves file paths from the `file` field in each mapping entry (relative to the mapping file).
Wait for it to complete (poll with `cat lemmafit/.vibe/claimcheck.json` until it contains valid JSON), then read the results.
## Step 7: Report and iterate
Parse the claimcheck results and report:
- **Confirmed** — the lemma faithfully expresses the requirement. No action needed.
- **Disputed** — a discrepancy was found. Show the `discrepancy` text and `weakeningType` (tautology, weakened-postcondition, narrowed-scope, wrong-property).
- **Error** — lemma not found in source. Check the lemmaName.
**If any claims are disputed:** Suggest specific fixes to the Dafny code or the requirement text. If the user agrees, make the fixes, wait for re-verification, and re-run the guarantees process.
## Step 8: Ensure all files up to date
Once iteration is complete, compare `claimcheck-mapping.json` with `guarantees.json` to ensure they contain equivalent information. If there's a discrepancy, trace back to the Dafny code to find which is most accurate. Adjust the relevant file accordingly and re-run `/guarantees` command. Once confirmed, report that the files are in sync.
## Step 9: Generate guarantees.md via the script
Do this only after Step 8 confirms that `claimcheck-mapping.json` and `guarantees.json` are in sync.
Run the deterministic report generator:
```bash
npx lemmafit-generate-guarantees
```
This reads `reports/guarantees.json`, `reports/claimcheck.json`, and `SPEC.yaml` and writes `reports/guarantees.md`. Do NOT write this file manually — always use the script so the report matches the JSON exactly.
Report to the user: "A report of your app's guarantees has been generated in lemmafit/reports/guarantees.md"
+1
-1
blank-template/package.json

@@ -22,5 +22,5 @@ {

"@vitejs/plugin-react": "^4.2.0",
"typescript": "^5.3.0",
"typescript": "^5.3.0",
"vite": "^5.0.0"
}
}
+2
-2
cli/generate-guarantees-md.js
#!/usr/bin/env node
/**
* Generates lemmafit/.vibe/guarantees.md deterministically from:
* - lemmafit/.vibe/guarantees.json (claim-to-spec mapping)
* Generates reports/guarantees.md deterministically from:
* - reports/guarantees.json (claim-to-spec mapping)
* - lemmafit/.vibe/claimcheck.json (claimcheck results, optional)

@@ -6,0 +6,0 @@ * - SPEC.yaml (for trusted entries and group info)

+2
-1
cli/lemmafit.js

@@ -102,3 +102,4 @@ #!/usr/bin/env node

if (serverBase.toLowerCase() !== 'none') {
const serverWsUrl = `${serverBase}/ws?project=${encodeURIComponent(projectName)}`;
const sep = serverBase.includes('?') ? '&' : '?';
const serverWsUrl = `${serverBase}${sep}project=${encodeURIComponent(projectName)}`;
config.server = serverWsUrl;

@@ -105,0 +106,0 @@ }

+0
-13
cli/sync.js

@@ -113,15 +113,2 @@ #!/usr/bin/env node

// Sync .claude/commands/ from package
const srcCommands = path.join(__dirname, '..', 'commands');
if (fs.existsSync(srcCommands)) {
const commandsDir = path.join(claudeDir, 'commands');
fs.mkdirSync(commandsDir, { recursive: true });
for (const file of fs.readdirSync(srcCommands)) {
fs.copyFileSync(
path.join(srcCommands, file),
path.join(commandsDir, file)
);
}
}
// Sync .claude/skills/ from package

@@ -128,0 +115,0 @@ const srcSkills = path.join(__dirname, '..', 'skills');

+4
-0
docs/CLAUDE_INSTRUCTIONS.md

@@ -63,3 +63,7 @@ # Lemmafit Project

- `lemmafit-spec`: Load this skill when user asks to add or edit feature, and before writing or editing the spec.yaml file
- `lemmafit-guarantees`: Load this skill to generate a human-readable guarantees report from proven Dafny code and verify claims with claimcheck
- `lemmafit-pre-react-audits`: Load this skill before writing React to audit proof strength and catch unverified logic
- `lemmafit-post-react-audit`: Load this skill after writing React to catch effect-free logic that should be in Dafny
If you try to read any of these files and they are missing, alert the user.

@@ -66,0 +70,0 @@ 

+1
-2
package.json

@@ -18,3 +18,3 @@ {

],
"version": "0.2.0",
"version": "0.2.1",
"type": "commonjs",

@@ -26,3 +26,2 @@ "files": [

"skills/",
"commands/",
"kernels/",

@@ -29,0 +28,0 @@ "blank-template/"

+5
-3
README.md

@@ -34,5 +34,5 @@ # lemmafit

- lemmafit works with greenfield projects only. You must begin a project with lemmafit. Support for existing codebases is in the pipeline.
- 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 Typescript which then hooks into a React app. In the future, we will support other languages and frameworks.
- lemmafit compiles Dafny to Javascript/Typescript which then hooks into a runtime like a React app. In the future, we will support other languages.

@@ -48,3 +48,3 @@ - lemmafit is optimized to work with Claude Code. In the future, lemmafit will be agent-agnostic.

4. The agent will hook the generated TypeScript API into a React app — the logic is proven correct
5. After proofs complete, run custom command in Claude Code `/guarantees` to activate claimcheck and generate a guarantees report
5. After proofs complete, run the `/guarantees` skill to activate claimcheck and generate a guarantees report

@@ -62,2 +62,3 @@ ## Project Structure

│ │ ├── config.json # Project config
│ │ ├── modules.json # Module registry (for multi-module projects)
│ │ ├── status.json # Verification status (generated)

@@ -81,2 +82,3 @@ │ │ └── claims.json # Proof obligations (generated)

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)

@@ -83,0 +85,0 @@ lemmafit daemon [dir] # Run verification daemon standalone

+1
-1
skills/lemmafit-dafny/SKILL.md

@@ -9,3 +9,3 @@ ---

## When to Write Code in Dafny
- ALL `verifiable:true` entries in the spec MUST be written in Dafny (do not write verifiable code directly in JavaScript or TypeSscript)
- ALL `verifiable:true` entries in the spec MUST be written in Dafny (do not write verifiable code directly in JavaScript or TypeScript)

@@ -12,0 +12,0 @@ ## Dafny Pattern Example

+3
-2
skills/lemmafit-spec/SKILL.md

@@ -42,3 +42,3 @@ ---

- `guarantee_type` — `verified`, `assumed`, or `trusted`
- `state` - `DRAFT`, `ADDRESSED`, `null`- only use `addressed` if the corresponding Dafny module or property have been verified. Use null for `verifiable: false`
- `state` - `DRAFT`, `ADDRESSED`, `null` — only use `ADDRESSED` if the corresponding Dafny module or property have been verified. Use `null` for `verifiable: false`

@@ -58,3 +58,4 @@ ### Example

verifiable: true
status: verified
guarantee_type: verified
state: ADDRESSED
- id: spec-002

@@ -61,0 +62,0 @@ req_id: null

-138
commands/guarantees.md
# Generate Guarantees and Run Claimcheck
You are generating human-readable guarantees from proven Dafny code and verifying them with claimcheck.
## Step 0: Make sure the state of the project is verified
Check `lemmafit/.vibe/status.json` for the current verification status.
## Step 1: Read project data
Read these files:
- `lemmafit/.vibe/claims.json` — extracted proof obligations from Dafny (predicates with conjuncts, lemmas with requires/ensures, functions with contracts, axioms)
- `SPEC.yaml` — natural language requirements with spec entries
- `lemmafit/dafny/Domain.dfy` — the Dafny source code
- `lemmafit/.vibe/config.json` — project config (need `appCore` field for claimcheck domain)
If `claims.json` doesn't exist, tell the user to run the daemon first (`npm run daemon` or `npm run dev`) so Dafny verification produces claims.
## Step 2: Map claims to spec entries
Analyze the claims from `claims.json` and map them to spec entries from `SPEC.yaml`.
**How claims work:**
- **Predicate conjuncts** (in `predicates[].conjuncts`) are invariant properties proven by the `StepPreservesInv` lemma. Each conjunct in the `Inv` predicate is a separate proven property.
- **Lemma ensures** (in `lemmas[].ensures`) are standalone proven properties. The lemma name is in `lemmas[].name`.
- **Function contracts** (in `functions[].requires` and `functions[].ensures`) are proven pre/postconditions.
- **Axioms** (in `axioms[]`) are assumed, NOT proven — they represent the trust surface.
**Mapping rules:**
- A claim "covers" a spec entry if the Dafny expression proves the property described by that spec entry
- One claim can cover multiple spec entries
- Spec entries with `status: trusted` don't need covering claims
- Spec entries with `verifiable: false` should be skipped
- Identify **gaps**: spec entries with `status: verified` that have NO covering claim
## Step 3: Write guarantees.json
Write `lemmafit/.vibe/guarantees.json` with this format:
```json
{
"generatedAt": "<ISO timestamp>",
"guarantees": [
{
"specId": "spec-001",
"requirement": "<title from SPEC.yaml>",
"status": "proven",
"coveredBy": [
{
"claimId": "inv:<Module>.<Predicate>:<conjunctIndex>",
"type": "invariant-conjunct",
"expression": "<the Dafny expression>",
"lemmaName": "StepPreservesInv"
}
],
"reasoning": "<why this claim covers this spec entry>"
}
],
"gaps": [
{
"specId": "spec-005",
"requirement": "<title>",
"reason": "<why no claim covers this>"
}
]
}
```
For `lemmaName`:
- Invariant conjuncts → `"StepPreservesInv"`
- Lemma ensures → the lemma's name (e.g. `"UndoReversesLast"`)
- Function contracts → the function's name
## Step 4: Handle multi-lemma requirements
If a single requirement is covered by **multiple** lemmas (e.g. an invariant conjunct AND a standalone lemma together prove one requirement), you must write a **new wrapper lemma** in the Dafny source that proves the full requirement in one place. The wrapper lemma should:
- Have a name that clearly describes the requirement (e.g. `Guarantee_UniqueUpvotes`)
- Call/use the individual lemmas as needed
- Have an `ensures` clause that directly expresses the full natural-language requirement
This is necessary because claimcheck needs exactly one lemma per requirement to verify faithfulness.
Wait for the daemon to re-verify after writing any new lemmas before proceeding.
## Step 5: Write claimcheck mapping
Write `lemmafit/.vibe/claimcheck-mapping.json` — an array of `{ requirement, lemmaName, file }` objects derived from the guarantees. The `file` field is a **path relative to the mapping file** (i.e. relative to `lemmafit/.vibe/`).
```json
[
{ "requirement": "Each user can only upvote once", "lemmaName": "Guarantee_UniqueUpvotes", "file": "../dafny/Domain.dfy" }
]
```
Each requirement should map to exactly one lemma. If you wrote wrapper lemmas in step 4, use those.
## Step 6: Run claimcheck
Run `claimcheck-multi` to verify that each lemma faithfully expresses its requirement.
**CRITICAL: claimcheck-multi MUST run in the background with output redirected to files.** It spawns `claude -p` as a subprocess, which will hang indefinitely if run in the foreground from a Claude Code session. Always use `&` and redirect stdout/stderr:
```bash
claimcheck-multi -m lemmafit/.vibe/claimcheck-mapping.json -d <appCore> --json --claude-code > lemmafit/.vibe/claimcheck.json 2> lemmafit/.vibe/claimcheck-err.log &
```
Replace `<appCore>` with the value from `lemmafit/.vibe/config.json`.
No `--dfy` flag needed — `claimcheck-multi` resolves file paths from the `file` field in each mapping entry (relative to the mapping file).
Wait for it to complete (poll with `cat lemmafit/.vibe/claimcheck.json` until it contains valid JSON), then read the results.
## Step 7: Report and iterate
Parse the claimcheck results and report:
- **Confirmed** — the lemma faithfully expresses the requirement. No action needed.
- **Disputed** — a discrepancy was found. Show the `discrepancy` text and `weakeningType` (tautology, weakened-postcondition, narrowed-scope, wrong-property).
- **Error** — lemma not found in source. Check the lemmaName.
**If any claims are disputed:** Suggest specific fixes to the Dafny code or the requirement text. If the user agrees, make the fixes, wait for re-verification, and re-run the guarantees process.
## Step 8: Ensure all files up to date
Once iteration is complete, compare `claimcheck-mapping.json` with `guarantees.json` to ensure they contain equivalent information. If there's a discrepancy, trace back to the Dafny code to find which is most accurate. Adjust the relevant file accordingly and re-run `/guarantees` command. Once confirmed, report that the files are in sync.
## Step 9: Generate guarantees.md via the script
Do this only after Step 9 confirms that `claimcheck-mapping.json` and `guarantees.json` are in sync.
Run the deterministic report generator:
```bash
npx lemmafit-generate-guarantees
```
This reads `lemmafit/.vibe/guarantees.json`, `lemmafit/.vibe/claimcheck.json`, and `SPEC.yaml` and writes `lemmafit/.vibe/guarantees.md`. Do NOT write this file manually — always use the script so the report matches the JSON exactly.
Report to the user: "A report of your app's guarantees has been generated in lemmafit/reports/guarantees.md"