validate

Files (1)

• SKILL.md

SKILL.md (first lines)

# validate

## When to invoke

- Current phase is `implement` and `mapping.md` rows reference real code.

## Steps

1. Read `.formal/settings/rules/validation.md`.
2. Run `rd-flow validate <name>`. It does the mechanical work for you:
   artefact presence, the TLA+/Dafny gates, check freshness, and both ends
   of every `mapping.md` row. Findings land in `validation-report.md` and
   on `manifest.yaml.blockers`.
3. Read the report. For each blocker:
   - *unfilled or broken mapping row* — fix `mapping.md` so it cites a
     real `file:line` and a real spec symbol,
   - *gate not green* — re-run `rd-flow tla check <name>` or
     `rd-flow dafny verify <name>`,
   - *check pre-dates its artefact* — the artefact changed after it was
     checked; re-run that check.
4. Re-run `rd-flow validate <name>` until it reports `passed`. It sets
   `current_phase` to `validate` itself — do not use `rd-flow advance` to
   force the phase past a blocker.
5. Optionally append a one-line summary to `.formal/steering/`.

## Notes

- `rd-flow validate <name> --strict` exits non-zero when blocked; use it
  if you are wiring the spec into CI.
- `--no-advance` runs the same checks without touching `current_phase`,
  which is useful for a mid-implementation progress read.

## Handoff

The spec is closed. Future work on it re-enters at `discovery`.

From KKuze/rd-flow, MIT.

More from KKuze/rd-flow