# Lemmafit Post React Audit

> Audit workflow for lemmafit apps after React. Runs after writing React code to catch logic that slipped through. Performs audit and labels findings by severity and iterates until only minor findings remain. Use when this capability is needed.

- Skill: `tomevault-io/lemmafit-post-react-audit` (Agent Skill, multi-file: 2 files)
- Install (CLI): `npx skillmds@latest add tomevault-io/lemmafit-post-react-audit`
- Raw SKILL.md: https://api.skillmd.com/api/skills/tomevault-io/lemmafit-post-react-audit/raw
- Safety review: pending (external: skill-scanner PASS, skillspector PASS)
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Web & Frontend
- Author: tomevault-io (https://skillmd.com/u/tomevault-io)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/tomevault-io/lemmafit-post-react-audit

---


# Lemmafit Post React Audit


## Audit: Logic-in-JS-post

Check whether any effect-free logic required for the current build phase is found written directly in JavaScript or TypeScript instead of Dafny.

### What to check

1. **State derivations in React** — Any computed value derived from state (filtering, sorting, calculations, conditional logic) that is not exposed through `Api.Present` or a Dafny function. These belong in Dafny.
2. **Validation in JS** — Input validation, constraint checks, or boundary enforcement done in React hooks or components instead of Dafny predicates.
3. **Business rules in event handlers** — Pure conditional guards on dispatching (e.g., "only allow X if Y" where Y is derivable from model state) that aren't enforced by Dafny preconditions or exposed as predicates. Exclude effect-gating logic (e.g., "only call Stripe API if active") — that belongs in JS.
4. **Formatting with logic** — Display formatting that encodes business rules (e.g., color based on threshold, status text based on state) rather than pure cosmetic formatting.
5. **Duplicated logic** — Logic that exists in Dafny and is available via API but is re-implemented in JS (even partially), creating a consistency risk.
6. **Utils with hidden logic** — Utility functions in `src/utils` that contain domain logic rather than pure display helpers.

## Severity Labels

Label each finding with one of:

| Severity | Meaning | Action |
|---|---|---|
| `critical` | Effect-free logic in JS that could produce wrong behavior if it diverges from Dafny, or logic duplicated between JS and Dafny | Must move to Dafny before shipping |
| `moderate` | Effect-free logic in JS that should be a Dafny function or predicate but isn't yet causing a correctness risk | Should move to Dafny |
| `minor` | Borderline case where JS logic is arguably pure formatting, or a trivial derivation not worth a Dafny round-trip | Can keep in JS, document why |

## Output Format

Present findings as a numbered list with severity tag and file location:

```
## Logic-in-JS Post-React Audit

1. [critical] src/hooks/useSubscription.ts:42 — computes prorated refund in JS, duplicates Dafny proration logic
2. [moderate] src/components/PlanCard.tsx:18 — derives "canUpgrade" from state fields, should be a Dafny predicate
3. [minor] src/utils/format.ts:10 — date formatting, pure display (OK)
```

## Pass Criteria

The audit passes when there are **zero critical and zero moderate findings**. If any remain, move the logic to Dafny (back to Step 2), re-verify, then re-run this audit.

---
> Source: [midspiral/lemmafit](https://github.com/midspiral/lemmafit) — distributed by [TomeVault](https://tomevault.io).
<!-- tomevault:4.0:skill_md:2026-06-18 -->