Add TypeScript verification skills

[leynos]

Summary

This branch adds TypeScript verification guidance so agents can choose the right level of assurance for JavaScript and TypeScript work: sampled property testing with fast-check, machine-checked proof with LemmaScript, and deterministic test layers for ODW workflow scripts. It also carries the ODW testing skill that is present on the local main branch but not yet on origin/main, because the branch was cut from that local commit.

No roadmap task or issue is referenced by the branch. No execplan is present for this branch; the only execplan in the repository, docs/execplans/adopt-vendcurl.md, is a completed historical plan for unrelated vendcurl work.

Review walkthrough

• Start with skills/fast-check/SKILL.md to review the trigger rules, fast-check 4.x guidance, failure replay advice, and escalation boundary to formal proof.
• Then review skills/fast-check/references/arbitraries.md and skills/fast-check/references/model-based-testing.md for the supporting generator, shrinking, command-model, and scheduler examples.
• Continue with skills/lemmascript/SKILL.md to check the formal-verification routing guidance and the boundary between sampled properties and proof obligations.
• Review skills/lemmascript/references/annotations.md and skills/lemmascript/references/workflow.md for the annotation surface, Dafny and Lean workflow, CI guidance, and brownfield adoption advice.
• Finish with skills/odw-testing/SKILL.md to review the ODW workflow testing layers that are included in the full branch diff against origin/main.

Validation

• git diff --check origin/main...HEAD: passed.
• make all 2>&1 | tee /tmp/make-all-agent-helper-scripts-typescript-verification-skills.out: failed after check-fmt, lint, and typecheck passed; pytest reported 79 passed and 1 failed.

Failure detail:

tests/test_rust_entrypoints.py::test_system_phase_uses_temporary_checkout_and_installs_system_packages
AssertionError: system phase should succeed: expected 0 but got 1; stderr='[bootstrap] Using sudo for privileged ops\n.../rust-entrypoint-system: line 73: VERSION_CODENAME: unbound variable\n'

Notes

The failing validation path is unchanged by this branch: rust-entrypoint-system has the same VERSION_CODENAME lookup on origin/main, and the branch diff does not touch tests/test_rust_entrypoints.py.

Summary by Sourcery

Add new skills documentation for testing and formal verification of TypeScript/JavaScript and ODW workflows.

Documentation:

• Document an odw-testing skill describing layered testing strategies for Open Dynamic Workflows, including parse gates, helper-unit tests, fixture repos, simulations, mock-adapter end-to-end runs, and smoke tests.
• Document a fast-check skill that explains when and how to use fast-check 4.x for property-based testing in TypeScript/JavaScript, with references on arbitraries, model-based testing, and race-condition detection.
• Document a lemmascript skill that explains how to apply LemmaScript for formal verification of TypeScript, including annotations, Dafny/Lean workflows, and brownfield adoption guidance, with detailed reference guides.

[coderabbitai]

Important

Review skipped

Draft detected.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: db4a0c52-7eee-459b-83c4-e8ff74959fdf

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch typescript-verification-skills

---

_{Comment @coderabbitai help to get the list of available commands.}

[sourcery-ai]

Reviewer's Guide

Adds three new TypeScript verification-related skills (fast-check property-based testing, LemmaScript formal verification, and ODW workflow testing) along with reference documents, giving agents structured guidance on when and how to use sampled property testing, machine-checked proof, and deterministic workflow tests for JavaScript/TypeScript and ODW scripts.

Flow diagram for selecting TypeScript verification skills

flowchart TD
  user_request["User asks about verifying JS/TS or ODW workflows"]

  decision_kind{"What needs verification?"}
  js_ts_logic["JS/TS function or library behavior"]
  critical_property["Load-bearing property that must always hold"]
  odw_workflow["ODW workflow script behavior"]

  fast_check_skill["Use fast-check sampled property tests"]
  lemmascript_skill["Use LemmaScript formal verification"]
  odw_testing_skill["Use ODW deterministic workflow tests"]

  user_request --> decision_kind

  decision_kind --> js_ts_logic
  decision_kind --> critical_property
  decision_kind --> odw_workflow

  js_ts_logic --> fast_check_skill
  critical_property --> lemmascript_skill
  odw_workflow --> odw_testing_skill

  fast_check_skill -->|"Escalate when sampled testing is insufficient"| lemmascript_skill
  lemmascript_skill -->|"Keep broad regression net"| fast_check_skill

  odw_testing_skill --> odw_layers{"Pick test layer 0-6"}

Loading

File-Level Changes

Change	Details	Files
Introduce an ODW workflow testing skill describing a layered strategy for testing ODW JavaScript workflows with deterministic local techniques and mock adapters.	Add a new odw-testing skill with trigger description and usage guidance for testing ODW workflow scripts executed by the odw CLI. Define a multi-layer test strategy (parse gate, helper-surface unit tests, schema contract tests, git/filesystem fixtures, source invariants, control-loop simulation, mock-adapter end-to-end, and live smoke runs). Provide concrete Node.js and shell snippets for parsing workflows, slicing helper regions, constructing fixture repositories, simulating control loops with scripted primitives, and running odw with mock adapters. Document anti-patterns and a checklist to keep tests deterministic, hermetic, and decoupled from prompt wording.	skills/odw-testing/SKILL.md
Introduce a fast-check skill for property-based testing in TypeScript/JavaScript, plus detailed references for arbitraries, model-based testing, and race-condition detection.	Add a fast-check SKILL document explaining when to use fast-check, core concepts (arbitraries, properties, async properties), and how to configure runs and integrate into projects. Highlight 4.x-specific guidance and migration notes from 3.x, including new string APIs, scheduler changes, and deprecated helpers. Add an arbitraries reference covering common arbitraries, composition patterns with map/chain/record/letrec, and guidance on avoiding the filtering trap. Add a model-based testing reference that defines commands, shows a worked example, explains replay via replayPath, and demonstrates using fc.scheduler for race-condition detection.	skills/fast-check/SKILL.md skills/fast-check/references/model-based-testing.md skills/fast-check/references/arbitraries.md
Introduce a LemmaScript skill for formal verification of TypeScript along with references for annotations and workflow/backends.	Add a LemmaScript SKILL document describing when to escalate from sampled testing to formal proofs, installation and backend prerequisites, core annotation concepts (requires/ensures/invariants/decreases), and project integration patterns. Document anti-patterns around misuse of assume, erasing .dfy work, or verifying parallel models instead of production functions, plus lessons learned from case studies. Add an annotations reference detailing the LemmaScript annotation surface (file-level directives, function/loop contracts, declaration/statement-level annotations), the spec expression language, supported TS subset, purity rules, and common gotchas. Add a workflow reference explaining backend choices (Dafny vs Lean), the lsc CLI, file/artefact layout per backend, the Dafny regen-based edit loop, proof techniques, brownfield strategy, and CI integration via LemmaScript-files.txt.	skills/lemmascript/SKILL.md skills/lemmascript/references/annotations.md skills/lemmascript/references/workflow.md

---

Tips and commands

Interacting with Sourcery

• Trigger a new review: Comment @sourcery-ai review on the pull request.
• Continue discussions: Reply directly to Sourcery's review comments.
• Generate a GitHub issue from a review comment: Ask Sourcery to create an
  issue from a review comment by replying to it. You can also reply to a
  review comment with @sourcery-ai issue to create an issue from it.
• Generate a pull request title: Write @sourcery-ai anywhere in the pull
  request title to generate a title at any time. You can also comment
  @sourcery-ai title on the pull request to (re-)generate the title at any time.
• Generate a pull request summary: Write @sourcery-ai summary anywhere in
  the pull request body to generate a PR summary at any time exactly where you
  want it. You can also comment @sourcery-ai summary on the pull request to
  (re-)generate the summary at any time.
• Generate reviewer's guide: Comment @sourcery-ai guide on the pull
  request to (re-)generate the reviewer's guide at any time.
• Resolve all Sourcery comments: Comment @sourcery-ai resolve on the
  pull request to resolve all Sourcery comments. Useful if you've already
  addressed all the comments and don't want to see them anymore.
• Dismiss all Sourcery reviews: Comment @sourcery-ai dismiss on the pull
  request to dismiss all existing Sourcery reviews. Especially useful if you
  want to start fresh with a new review - don't forget to comment
  @sourcery-ai review to trigger a new review!

Customizing Your Experience

Access your dashboard to:

• Enable or disable review features such as the Sourcery-generated pull request
  summary, the reviewer's guide, and others.
• Change the review language.
• Add, remove or edit custom review instructions.
• Adjust other review settings.

Getting Help

• Contact our support team for questions or feedback.
• Visit our documentation for detailed guides and information.
• Keep in touch with the Sourcery team by following us on X/Twitter, LinkedIn or GitHub.