| name | lemmafit-pre-react-audits |
| description | Audit workflow for lemmafit apps before React. Run before writing React code to catch proof gaps and unverified logic. Performs two audits — Proof Strength (are proofs complete and tight?) and Logic-in-JS (is any logic missing from Dafny?). Labels findings by severity and iterates until only minor findings remain. |
Lemmafit Audits
Run both audits below in order. Report findings in a structured table. Iterate with the lemmafit-proofs skill (Step 4) until only minor findings remain.
Audit 1: Proof Strength Audit
Check the strength of every proof in the Dafny codebase against the corresponding SPEC.yaml entries.
What to check
- Missing lemmas — Every
verifiable: true entry in SPEC.yaml with type: postcondition must have a corresponding lemma with a matching ensures clause. Invariant-only coverage is not sufficient for postcondition entries.
- Weak postconditions — Are
ensures clauses as strong as the property stated in SPEC.yaml? A proof that verifies but proves less than the spec claims is a gap. Look for postconditions that are trivially true or weaker than the stated property.
- Axiom debt — Flag every
assume {:axiom} statement. Each one is unverified trust. Check whether a real proof is feasible.
- Invariant tightness — Every code guard or clamp (e.g.,
if x > MAX then MAX else x) must have a matching bound in Inv at full strength (e.g., 0 <= x <= MAX). Loose invariants hide bugs.
- Missing biconditionals — For every "if X then Y" lemma, check whether the converse "if not X then not Y" is also proven (or document why it's unnecessary).
- Composition gaps — If two features interact, is there a lemma proving their combined properties? Implicit composition is a proof gap.
- Normalize reliance — Check if
StepPreservesInv only holds because of Normalize. If removing Normalize would break the proof, flag it — the Apply function should ideally preserve the invariant on its own for each action.
- Input validation — Every trust-boundary datatype should have a
Valid_* predicate, and Step should requires Valid_*(input) for external inputs. Missing validation predicates are gaps.
Audit 2: Logic-in-JS
Check whether any effect-free logic required for the current build phase is expected to be implemented in JavaScript/TypeScript directly instead of Dafny.
What to check
- 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.
- Validation in JS — Input validation, constraint checks, or boundary enforcement done in React hooks or components instead of Dafny predicates.
- 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.
- 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.
- Duplicated logic — Logic that exists in Dafny but is re-implemented in JS (even partially), creating a consistency risk.
- Utils with hidden logic — Utility functions that contain domain logic rather than pure display helpers.
Severity Labels
Label each finding with one of:
| Severity | Meaning | Action |
|---|
critical | Unverified logic that could produce wrong behavior, or a SPEC.yaml postcondition with no corresponding proof | Must fix before proceeding to React |
moderate | Weak proof that verifies but doesn't fully cover the spec property, or JS logic that should move to Dafny | Should fix before proceeding |
minor | Style issue, missing biconditional for an edge case, or axiom with clear justification | Can proceed, fix later |
Output Format
Present findings as a numbered list grouped by audit, with severity tag:
## Proof Strength Audit
1. [critical] spec-003 "Total weight is sum of sets" — no lemma found, only covered by Inv
2. [moderate] StepPreservesInv — only holds due to Normalize for AddSet action
3. [minor] UndoRedoRoundTrip — missing biconditional (converse not meaningful here)
## Logic-in-JS Audit
1. [critical] src/hooks/useWorkout.ts:24 — filters completed sets using JS logic, should be a Dafny function
2. [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 critical or moderate findings remain, return to Step 4 (proofs) to address them, then re-run audits.
