Add TypeScript verification skills - #25
Conversation
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
Summary
WalkthroughAdd two documentation skill sets: fast-check property-based testing guidance and LemmaScript formal-verification guidance, each with reference pages covering usage, workflows, limitations, and integration. Changesfast-check documentation
LemmaScript documentation
Poem
🚥 Pre-merge checks | ✅ 20✅ Passed checks (20 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
Reviewer's GuideAdds 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 skillsflowchart 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"}
File-Level Changes
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
Add two agent skills covering verification of TypeScript and JavaScript: - `fast-check` — property-based testing with fast-check 4.x: arbitrary design and the filtering trap, model-based (stateful) testing with commands, race-condition detection with the scheduler, failure replay, and 3.x-to-4.x migration notes. - `lemmascript` — formal verification with LemmaScript (tech preview): the `//@` annotation surface and spec expression language, the Dafny `regen` three-way-merge edit loop, the Lean four-file scheme, recurring proof techniques, brownfield strategy, and CI wiring. Each skill follows the progressive-discovery layout: a SKILL.md overview with detail split into `references/` files. The skills cross-reference each other so sampled properties escalate to proof where the property is load-bearing, and proofs keep a fast-check regression net beneath them. Content is grounded in the upstream sources as of July 2026: fast-check 4.8.0 (fast-check.dev docs and migration guide) and LemmaScript SPEC.md v0.5.x, DESIGN.md, and GETTING_STARTED.md.
6085981 to
c2e3559
Compare
![sourcery-ai[bot]](https://avatars.githubusercontent.com/in/48477?s=60&v=4){kind=small}
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c2e3559ee0
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| the TypeScript source *is* the production code; there is no erasure and no | ||
| verified-model/production gap. Think "Verus is to Rust as LemmaScript is to |
There was a problem hiding this comment.
Remove the claim that there is no verified-model/production gap, or qualify it to mean only that the same source file is verified. The new annotation reference itself documents semantic differences from production JavaScript—including mathematical rather than IEEE-754 numbers (annotations.md, lines 128-129), lost short-circuiting (lines 136-137), and axiomatized cross-file calls (lines 144-147)—so a proof can succeed while the shipped runtime behaves differently. The absolute claim is especially unsafe because this skill recommends LemmaScript for security and other load-bearing properties.
Useful? React with 👍 / 👎.
| //@ ensures \result >= -1 && \result < arr.length | ||
| //@ ensures \result >= 0 ==> arr[\result] === target |
There was a problem hiding this comment.
Strengthen this introductory contract to require completeness and minimality. As written, an implementation that always returns -1 satisfies both postconditions for every permitted input, and one returning any matching index also passes even when an earlier match exists. That makes the flagship verification example demonstrate exactly the underspecified-proof failure warned about later in the skill rather than proving firstIndexOf correct.
Useful? React with 👍 / 👎.
| // Drive everything the scheduler currently knows about | ||
| await s.waitIdle(); | ||
|
|
||
| expect(q.drain()).toHaveLength(2); |
There was a problem hiding this comment.
Assert the queue's ordering rather than only its length. For any queue implementation that retains both items—including a LIFO queue or one that reverses concurrent writes—this property passes, so the scheduler example cannot detect the race condition named by the test. Capture the expected order established by the scheduled operations and compare the drained values to it, or rename this as a no-loss property.
Useful? React with 👍 / 👎.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 6
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
skills/lemmascript/references/annotations.md (1)
489-489: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winRemove the second-person pronoun.
Replace “a value you just
havoced” with impersonal wording such as “a value immediately assigned by//@ havoc”.Triage:
[type:docstyle]🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@skills/lemmascript/references/annotations.md` at line 489, Update the wording in the annotations documentation to remove the second-person pronoun, replacing “a value you just `havoc`ed” with impersonal wording such as “a value immediately assigned by `//@ havoc`.”Source: Path instructions
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@skills/fast-check/references/model-based-testing.md`:
- Around line 142-146: Update the scheduler guidance in the model-based testing
reference to state that s.waitIdle() drains all scheduled and recursively
scheduled work until the scheduler is idle. Retain waitAll as deprecated, and
clarify that s.waitFor(finalPromise) is only for awaiting a specific completion
condition rather than general idle draining.
In `@skills/fast-check/SKILL.md`:
- Line 10: Update the wording in the TypeScript/generated-input description to
use “handwritten” instead of “hand-written,” preserving the surrounding text and
meaning.
- Around line 113-115: Remove second-person phrasing at all three documented
sites: in skills/fast-check/SKILL.md lines 113-115, replace “async operations
you hand it” with “async operations supplied to it”; in lines 181-182, replace
“when you can compose” with “when composition is possible”; and in
skills/fast-check/references/model-based-testing.md lines 112-114, replace
“async work you hand it” with “async work supplied to it”.
- Line 46: Update the latest-version statement in the fast-check documentation
to reflect version 4.9.0, or rephrase it to avoid pinning a specific latest
version while preserving the Node.js compatibility information.
In `@skills/lemmascript/references/workflow.md`:
- Line 42: Replace “hand-written” with “handwritten” at both occurrences in
skills/lemmascript/references/workflow.md lines 42 and 53.
In `@skills/lemmascript/SKILL.md`:
- Around line 18-23: Update the LemmaScript description around the “no
verified-model/production gap” claim to qualify it: retain that TypeScript
source is the production code, but state that verification applies only within
the supported fragment and documented trust boundaries. Acknowledge the
runtime/model mismatches, JavaScript numeric semantics, and short-circuit
behavior limitations described in annotations.md without implying unconditional
equivalence.
---
Outside diff comments:
In `@skills/lemmascript/references/annotations.md`:
- Line 489: Update the wording in the annotations documentation to remove the
second-person pronoun, replacing “a value you just `havoc`ed” with impersonal
wording such as “a value immediately assigned by `//@ havoc`.”
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 61eb7328-4676-455d-9ff5-14b2bfff5951
📒 Files selected for processing (6)
skills/fast-check/SKILL.mdskills/fast-check/references/arbitraries.mdskills/fast-check/references/model-based-testing.mdskills/lemmascript/SKILL.mdskills/lemmascript/references/annotations.mdskills/lemmascript/references/workflow.md
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
leynos/cuprum(auto-detected)
| `waitOne` and `waitAll` are deprecated. Note the 4.x semantics: a task | ||
| scheduled *after* `waitIdle`/`waitAll` began its final drain stays pending — | ||
| tasks created behind intermediate `await`s are not magically picked up as they | ||
| sometimes were in 3.x. When the code under test schedules follow-up work | ||
| asynchronously, prefer `s.waitFor(finalPromise)`. |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Inspect the relevant section of the document with line numbers.
sed -n '130,155p' skills/fast-check/references/model-based-testing.md
# Locate any other references to waitIdle/waitAll/waitFor in the repository.
rg -n "waitIdle|waitAll|waitFor" skills/fast-check -S || trueRepository: leynos/agent-helper-scripts
Length of output: 1933
🌐 Web query:
fast-check Scheduler waitIdle waitAll waitFor semantics 4.x site:fast-check.dev
💡 Result:
In fast-check 4.x, the Scheduler API has been updated to provide more predictable and consistent behavior [1][2]. Notably, waitOne and waitAll are deprecated as of version 4.2.0 in favor of newer, more granular primitives [1][2]. The current semantics for these methods are as follows: waitIdle This method replaces waitAll [2][3]. It waits until the scheduler becomes idle, meaning all scheduled tasks and any tasks recursively scheduled by them have completed [4][3]. Unlike the older waitAll, which could have inconsistent behavior depending on micro-task timing and task scheduling latency, waitIdle provides a more predictable and reliable way to wait for the entire queue to clear [1][2]. It cannot, however, await tasks triggered by uncontrolled external sources (e.g., fetch or external events) [4][3]. waitFor(promise) This method waits for a specific, potentially unscheduled task to resolve [4][3]. It is highly useful when the task you are waiting for has not yet been scheduled, or when using testing frameworks (like supertest) that trigger queries only upon specific interactions [4][3]. It will wait as many scheduled tasks as needed—but only the minimal amount—to resolve the provided promise [4]. In version 4.1.0, waitFor was improved to exhaust all resolved micro-tasks before proceeding, ensuring better task capture and more effective reordering [5]. Deprecated Methods (waitOne, waitAll) These methods are deprecated as of version 4.2.0 [1][2]. - waitAll: Previously used to wait for all scheduled tasks, its behavior was often inconsistent due to dependencies on micro-task counts [1][2]. It is now replaced by waitIdle [4][2]. - waitOne: Previously used to wait for a single task, it is now effectively replaced by waitNext(1) [3]. When testing, it is recommended to use waitIdle for waiting for full completion and waitFor for specific, targeted synchronization [4][3]. For more granular control over task execution, consider using waitNext [1][3].
Citations:
- 1: https://fast-check.dev/docs/migration-guide/from-3.x-to-4.x/
- 2: https://fast-check.dev/blog/2025/07/18/whats-new-in-fast-check-4-2-0/
- 3: https://fast-check.dev/docs/advanced/race-conditions/
- 4: https://fast-check.dev/docs/api/interfaces/Scheduler/
- 5: https://fast-check.dev/blog/2025/04/06/whats-new-in-fast-check-4-1-0/
Correct the waitIdle() semantics in skills/fast-check/references/model-based-testing.md.
State that s.waitIdle() drains all scheduled and recursively scheduled work until the scheduler is idle. Keep waitAll as deprecated, and use s.waitFor(finalPromise) only for a specific completion condition.
🧰 Tools
🪛 LanguageTool
[uncategorized] ~144-~144: Possible missing comma found.
Context: ...diate awaits are not magically picked up as they sometimes were in 3.x. When the...
(AI_HYDRA_LEO_MISSING_COMMA)
[style] ~144-~144: The adverb ‘sometimes’ is usually put after the verb ‘were’.
Context: ...t`s are not magically picked up as they sometimes were in 3.x. When the code under test schedu...
(ADVERB_WORD_ORDER)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@skills/fast-check/references/model-based-testing.md` around lines 142 - 146,
Update the scheduler guidance in the model-based testing reference to state that
s.waitIdle() drains all scheduled and recursively scheduled work until the
scheduler is idle. Retain waitAll as deprecated, and clarify that
s.waitFor(finalPromise) is only for awaiting a specific completion condition
rather than general idle draining.
| scheduler, replay of failures, and CI tiering. Trigger whenever the user | ||
| mentions fast-check, property-based testing in TypeScript or JavaScript, | ||
| fc.assert, fc.property, arbitraries, model-based testing, fuzzing a | ||
| TypeScript function, or wants generated inputs instead of hand-written |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Use the spelling accepted by the CI gate.
Replace hand-written with handwritten; the spelling check currently fails this line.
Triage: [type:spelling]
Proposed fix
- test cases.
+ test cases.🧰 Tools
🪛 GitHub Actions: CI / 0_Makefile gates.txt
[error] 10-10: Typos/spelling check suggested replacement: 'hand-written' -> 'handwritten' (reported at :61).
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@skills/fast-check/SKILL.md` at line 10, Update the wording in the
TypeScript/generated-input description to use “handwritten” instead of
“hand-written,” preserving the surrounding text and meaning.
Source: Pipeline failures
| npm install --save-dev fast-check | ||
| ``` | ||
|
|
||
| The current major is 4.x (latest: 4.8.0). It requires Node ≥ 12.17 and, for |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '--- FILE SNIPPET ---\n'
sed -n '40,52p' skills/fast-check/SKILL.md | cat -n
printf '\n--- NPM METADATA ---\n'
python3 - <<'PY'
import json, urllib.request
url = 'https://registry.npmjs.org/fast-check'
with urllib.request.urlopen(url, timeout=20) as r:
data = json.load(r)
print('dist-tags.latest =', data.get('dist-tags', {}).get('latest'))
versions = sorted(data.get('versions', {}).keys(), key=lambda s: [int(x) if x.isdigit() else x for x in __import__('re').split(r'(\d+)', s)])
print('newest_version =', versions[-1] if versions else None)
PYRepository: leynos/agent-helper-scripts
Length of output: 256
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo '--- FILE SNIPPET ---'
sed -n '40,52p' skills/fast-check/SKILL.md | cat -n
echo
echo '--- NPM METADATA ---'
python3 - <<'PY'
import json, urllib.request
url = 'https://registry.npmjs.org/fast-check'
with urllib.request.urlopen(url, timeout=20) as r:
data = json.load(r)
print('dist-tags.latest =', data.get('dist-tags', {}).get('latest'))
print('version_count =', len(data.get('versions', {})))
print('latest_version_object_exists =', data.get('dist-tags', {}).get('latest') in data.get('versions', {}))
PYRepository: leynos/agent-helper-scripts
Length of output: 3278
🏁 Script executed (no clone):
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
import json, ssl, urllib.request
url = 'https://registry.npmjs.org/fast-check'
ctx = ssl._create_unverified_context()
with urllib.request.urlopen(url, context=ctx, timeout=20) as r:
data = json.load(r)
print('dist-tags.latest =', data.get('dist-tags', {}).get('latest'))
print('latest_version_exists =', data.get('dist-tags', {}).get('latest') in data.get('versions', {}))
PY
Length of output: 179
Update the latest-version claim. fast-check now reports 4.9.0 as latest, so latest: 4.8.0 is stale. Change it to 4.9.0 or rephrase the sentence to avoid pinning a moving target.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@skills/fast-check/SKILL.md` at line 46, Update the latest-version statement
in the fast-check documentation to reflect version 4.9.0, or rephrase it to
avoid pinning a specific latest version while preserving the Node.js
compatibility information.
| `fc.scheduler()` produces a scheduler arbitrary that reorders scheduled | ||
| promises to explore interleavings. Wrap the async operations under test with | ||
| `s.schedule(...)` (or `s.scheduleFunction`), then drive the run with |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Remove second-person pronouns from the documentation.
Rewrite these phrases to comply with the Markdown path instruction.
skills/fast-check/SKILL.md#L113-L115: replace “async operations you hand it” with “async operations supplied to it”.skills/fast-check/SKILL.md#L181-L182: replace “when you can compose” with “when composition is possible”.skills/fast-check/references/model-based-testing.md#L112-L114: replace “async work you hand it” with “async work supplied to it”.
Triage: [type:docstyle]
🧰 Tools
🪛 LanguageTool
[style] ~114-~114: Consider using the typographical ellipsis character here instead.
Context: ...ap the async operations under test with s.schedule(...) (or s.scheduleFunction), then drive...
(ELLIPSIS)
📍 Affects 2 files
skills/fast-check/SKILL.md#L113-L115(this comment)skills/fast-check/SKILL.md#L181-L182skills/fast-check/references/model-based-testing.md#L112-L114
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@skills/fast-check/SKILL.md` around lines 113 - 115, Remove second-person
phrasing at all three documented sites: in skills/fast-check/SKILL.md lines
113-115, replace “async operations you hand it” with “async operations supplied
to it”; in lines 181-182, replace “when you can compose” with “when composition
is possible”; and in skills/fast-check/references/model-based-testing.md lines
112-114, replace “async work you hand it” with “async work supplied to it”.
Source: Path instructions
|
|
||
| The diff `foo.dfy.gen` → `foo.dfy` must be **additions only**; `lsc check` | ||
| enforces it. Large proof developments often move the bulk of lemmas to a | ||
| separate hand-written file (`domain.proofs.dfy`). |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Replace “hand-written” with “handwritten”.
The repository spelling gate rejects both occurrences.
Triage: [type:spelling]
🧰 Tools
🪛 GitHub Actions: CI / 0_Makefile gates.txt
[error] 42-42: Typos/spelling check suggested replacement: 'hand-written' -> 'handwritten' (reported at :10).
🪛 LanguageTool
[misspelling] ~42-~42: This word is normally spelled as one.
Context: ...n move the bulk of lemmas to a separate hand-written file (domain.proofs.dfy). ### Lean (...
(EN_COMPOUNDS_HAND_WRITTEN)
📍 Affects 1 file
skills/lemmascript/references/workflow.md#L42-L42(this comment)skills/lemmascript/references/workflow.md#L53-L53
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@skills/lemmascript/references/workflow.md` at line 42, Replace “hand-written”
with “handwritten” at both occurrences in
skills/lemmascript/references/workflow.md lines 42 and 53.
Source: Pipeline failures
| LemmaScript is a verification toolchain for TypeScript. You write ordinary | ||
| TypeScript with `//@` specification comments; the `lsc` CLI generates formal | ||
| artefacts that a backend prover (Dafny, or Lean via Velvet/Loom) checks. The | ||
| annotations are comments — invisible to tsc, bundlers, and the runtime — and | ||
| the TypeScript source *is* the production code; there is no erasure and no | ||
| verified-model/production gap. Think "Verus is to Rust as LemmaScript is to |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
Qualify the “no verified-model/production gap” guarantee.
The claim overstates the assurance provided by this toolchain. skills/lemmascript/references/annotations.md documents runtime/model mismatches, JavaScript numeric semantics, lost short-circuit behaviour, and trusted boundaries. State that the TypeScript source remains production code, but verification is conditional on the supported fragment and explicitly documented trust boundaries.
🧰 Tools
🪛 SkillSpector (2.3.11)
[warning] 56: [RP1] null: npx commands without a version suffix (e.g. @1.0.0) create a rug-pull risk if the upstream server is compromised and publishes a malicious update.
Remediation: Pin the version: npx @scope/server@1.2.3
(MCP Rug Pull (RP1))
[warning] 83: [RP1] null: npx commands without a version suffix (e.g. @1.0.0) create a rug-pull risk if the upstream server is compromised and publishes a malicious update.
Remediation: Pin the version: npx @scope/server@1.2.3
(MCP Rug Pull (RP1))
[warning] 84: [RP1] null: npx commands without a version suffix (e.g. @1.0.0) create a rug-pull risk if the upstream server is compromised and publishes a malicious update.
Remediation: Pin the version: npx @scope/server@1.2.3
(MCP Rug Pull (RP1))
[warning] 85: [RP1] null: npx commands without a version suffix (e.g. @1.0.0) create a rug-pull risk if the upstream server is compromised and publishes a malicious update.
Remediation: Pin the version: npx @scope/server@1.2.3
(MCP Rug Pull (RP1))
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@skills/lemmascript/SKILL.md` around lines 18 - 23, Update the LemmaScript
description around the “no verified-model/production gap” claim to qualify it:
retain that TypeScript source is the production code, but state that
verification applies only within the supported fragment and documented trust
boundaries. Acknowledge the runtime/model mismatches, JavaScript numeric
semantics, and short-circuit behavior limitations described in annotations.md
without implying unconditional equivalence.
|
@coderabbitai review |
✅ Action performedReview finished.
|
There was a problem hiding this comment.
Actionable comments posted: 3
♻️ Duplicate comments (3)
skills/fast-check/SKILL.md (2)
10-10: 📐 Maintainability & Code Quality | 🟡 MinorUse the spelling accepted by the CI gate.
Replace “hand-written” with “handwritten” so the spelling check passes.
Triage:
[type:spelling]🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@skills/fast-check/SKILL.md` at line 10, Update the wording near the TypeScript function reference in SKILL.md by replacing “hand-written” with “handwritten”; leave the surrounding guidance unchanged.Source: Pipeline failures
46-46: 🎯 Functional Correctness | 🟡 MinorUpdate or remove the
latest: 4.8.0claim.As of July 26, 2026, the package registry lists fast-check 4.9.0 as the latest release. Rephrase this as the documented target version or update the claim. (npmjs.com)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@skills/fast-check/SKILL.md` at line 46, Update the fast-check version statement in the dependency requirements section to replace the stale “latest: 4.8.0” claim with 4.9.0, or rephrase it as the documented target version without asserting latest. Preserve the existing Node compatibility requirement.skills/fast-check/references/model-based-testing.md (1)
135-146: 🎯 Functional Correctness | 🟠 MajorCorrect the scheduler waiting semantics.
State that
s.waitIdle()drains currently scheduled tasks and any tasks they recursively schedule. Do not claim that such follow-up work remains pending; reserves.waitFor(promise)for waiting on a specific completion condition, including an unscheduled promise. The current wording conflicts with the guidance inskills/fast-check/SKILL.mdlines 116-118 and the fast-check API documentation. (fast-check.dev)Proposed correction
-`s.waitIdle()` — run until no scheduled task remains. +`s.waitIdle()` — drain currently scheduled tasks and any additional tasks they recursively schedule until idle. ... -`waitOne` and `waitAll` are deprecated. Note the 4.x semantics: a task - scheduled *after* `waitIdle`/`waitAll` began its final drain stays pending — - tasks created behind intermediate `await`s are not magically picked up as they - sometimes were in 3.x. When the code under test schedules follow-up work - asynchronously, prefer `s.waitFor(finalPromise)`. +`waitOne` and `waitAll` are deprecated. Use `s.waitFor(finalPromise)` when +waiting for a specific completion condition, especially when that promise was +not yet scheduled when the call began.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@skills/fast-check/references/model-based-testing.md` around lines 135 - 146, Correct the waiting semantics in the “Waiting primitives (4.2+)” section: describe s.waitIdle() as recursively draining currently scheduled tasks and tasks they schedule until idle. Remove the claim that follow-up tasks remain pending, and retain s.waitFor(finalPromise) only for waiting on a specific completion condition, particularly an unscheduled promise.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@skills/fast-check/SKILL.md`:
- Around line 13-15: Remove the blank line between the closing frontmatter
delimiter and the level-1 heading in SKILL.md, placing the title immediately
after the frontmatter block as required by the skill loader.
In `@skills/lemmascript/SKILL.md`:
- Around line 18-19: Remove second-person wording at all three documented sites:
rewrite “You write” in skills/lemmascript/SKILL.md lines 18-19, “what you wrote”
and “what you meant” in skills/lemmascript/SKILL.md lines 158-159, and “your
proof additions” in skills/lemmascript/references/workflow.md line 38 using
impersonal phrasing while preserving the original meaning.
- Around line 51-56: Pin all published LemmaScript CLI examples to a specific
release or lockfile-backed invocation. Update skills/lemmascript/SKILL.md lines
51-56 and 82-85, plus skills/lemmascript/references/workflow.md lines 16-21 and
24-28, including the npm install and npx lsc commands; preserve npx tsx
../LemmaScript/tools/src/lsc.ts as the brownfield live-edit path.
---
Duplicate comments:
In `@skills/fast-check/references/model-based-testing.md`:
- Around line 135-146: Correct the waiting semantics in the “Waiting primitives
(4.2+)” section: describe s.waitIdle() as recursively draining currently
scheduled tasks and tasks they schedule until idle. Remove the claim that
follow-up tasks remain pending, and retain s.waitFor(finalPromise) only for
waiting on a specific completion condition, particularly an unscheduled promise.
In `@skills/fast-check/SKILL.md`:
- Line 10: Update the wording near the TypeScript function reference in SKILL.md
by replacing “hand-written” with “handwritten”; leave the surrounding guidance
unchanged.
- Line 46: Update the fast-check version statement in the dependency
requirements section to replace the stale “latest: 4.8.0” claim with 4.9.0, or
rephrase it as the documented target version without asserting latest. Preserve
the existing Node compatibility requirement.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 41adf9b9-63e3-4392-88f9-1ed198e3b7c1
📒 Files selected for processing (6)
skills/fast-check/SKILL.mdskills/fast-check/references/arbitraries.mdskills/fast-check/references/model-based-testing.mdskills/lemmascript/SKILL.mdskills/lemmascript/references/annotations.mdskills/lemmascript/references/workflow.md
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
leynos/cuprum(auto-detected)
| --- | ||
|
|
||
| # fast-check property-based testing for TypeScript and JavaScript |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
Move the title directly after the frontmatter.
Delete the blank line between the closing --- and the level-1 heading. The skill loader requires the title to follow the frontmatter immediately.
Based on learnings, every SKILL.md file must place its level-1 heading immediately after the frontmatter block closes.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@skills/fast-check/SKILL.md` around lines 13 - 15, Remove the blank line
between the closing frontmatter delimiter and the level-1 heading in SKILL.md,
placing the title immediately after the frontmatter block as required by the
skill loader.
Source: Learnings
| LemmaScript is a verification toolchain for TypeScript. You write ordinary | ||
| TypeScript with `//@` specification comments; the `lsc` CLI generates formal |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Remove second-person language from the documentation.
skills/lemmascript/SKILL.md#L18-L19: rewrite “You write” impersonally.skills/lemmascript/SKILL.md#L158-L159: rewrite “what you wrote” and “what you meant” impersonally.skills/lemmascript/references/workflow.md#L38-L38: rewrite “your proof additions” impersonally.
Triage: [type:docstyle]
🧰 Tools
🪛 SkillSpector (2.3.11)
[warning] 56: [RP1] null: npx commands without a version suffix (e.g. @1.0.0) create a rug-pull risk if the upstream server is compromised and publishes a malicious update.
Remediation: Pin the version: npx @scope/server@1.2.3
(MCP Rug Pull (RP1))
[warning] 83: [RP1] null: npx commands without a version suffix (e.g. @1.0.0) create a rug-pull risk if the upstream server is compromised and publishes a malicious update.
Remediation: Pin the version: npx @scope/server@1.2.3
(MCP Rug Pull (RP1))
[warning] 84: [RP1] null: npx commands without a version suffix (e.g. @1.0.0) create a rug-pull risk if the upstream server is compromised and publishes a malicious update.
Remediation: Pin the version: npx @scope/server@1.2.3
(MCP Rug Pull (RP1))
[warning] 85: [RP1] null: npx commands without a version suffix (e.g. @1.0.0) create a rug-pull risk if the upstream server is compromised and publishes a malicious update.
Remediation: Pin the version: npx @scope/server@1.2.3
(MCP Rug Pull (RP1))
📍 Affects 2 files
skills/lemmascript/SKILL.md#L18-L19(this comment)skills/lemmascript/SKILL.md#L158-L159skills/lemmascript/references/workflow.md#L38-L38
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@skills/lemmascript/SKILL.md` around lines 18 - 19, Remove second-person
wording at all three documented sites: rewrite “You write” in
skills/lemmascript/SKILL.md lines 18-19, “what you wrote” and “what you meant”
in skills/lemmascript/SKILL.md lines 158-159, and “your proof additions” in
skills/lemmascript/references/workflow.md line 38 using impersonal phrasing
while preserving the original meaning.
Source: Path instructions
| ```sh | ||
| npm install lemmascript | ||
| ``` | ||
|
|
||
| For brownfield work, clone LemmaScript as a **sibling** of the target project | ||
| and invoke it from source (`npx tsx ../LemmaScript/tools/src/lsc.ts ...`) — it |
There was a problem hiding this comment.
🔒 Security & Privacy | 🟡 Minor | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
for f in skills/lemmascript/SKILL.md skills/lemmascript/references/workflow.md; do
echo "===== $f ====="
nl -ba "$f" | sed -n '1,220p'
echo
doneRepository: leynos/agent-helper-scripts
Length of output: 245
🏁 Script executed:
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
from pathlib import Path
paths = [
Path("skills/lemmascript/SKILL.md"),
Path("skills/lemmascript/references/workflow.md"),
]
for path in paths:
print(f"===== {path} =====")
for i, line in enumerate(path.read_text().splitlines(), 1):
print(f"{i:4d}: {line}")
print()
PYRepository: leynos/agent-helper-scripts
Length of output: 18131
🏁 Script executed:
#!/bin/bash
set -euo pipefail
rg -n "npm install lemmascript|npx lsc|tsx ../LemmaScript/tools/src/lsc.ts|LemmaScript-files.txt" skills README.md .Repository: leynos/agent-helper-scripts
Length of output: 3279
Pin the published CLI examples.
skills/lemmascript/SKILL.md#L51-L56and#L82-L85: pinnpm install lemmascriptand thenpx lscexamples to a specific release or lockfile-backed command.skills/lemmascript/references/workflow.md#L16-L28: do the same for the documentedlsccommands; keepnpx tsx ../LemmaScript/tools/src/lsc.tsas the brownfield live-edit path.
🧰 Tools
🪛 LanguageTool
[style] ~56-~56: Consider using the typographical ellipsis character here instead.
Context: ...rget project and invoke it from source (npx tsx ../LemmaScript/tools/src/lsc.ts ...) — it is a tech preview, and the clean...
(ELLIPSIS)
🪛 SkillSpector (2.3.11)
[warning] 56: [RP1] null: npx commands without a version suffix (e.g. @1.0.0) create a rug-pull risk if the upstream server is compromised and publishes a malicious update.
Remediation: Pin the version: npx @scope/server@1.2.3
(MCP Rug Pull (RP1))
[warning] 83: [RP1] null: npx commands without a version suffix (e.g. @1.0.0) create a rug-pull risk if the upstream server is compromised and publishes a malicious update.
Remediation: Pin the version: npx @scope/server@1.2.3
(MCP Rug Pull (RP1))
[warning] 84: [RP1] null: npx commands without a version suffix (e.g. @1.0.0) create a rug-pull risk if the upstream server is compromised and publishes a malicious update.
Remediation: Pin the version: npx @scope/server@1.2.3
(MCP Rug Pull (RP1))
[warning] 85: [RP1] null: npx commands without a version suffix (e.g. @1.0.0) create a rug-pull risk if the upstream server is compromised and publishes a malicious update.
Remediation: Pin the version: npx @scope/server@1.2.3
(MCP Rug Pull (RP1))
📍 Affects 2 files
skills/lemmascript/SKILL.md#L51-L56(this comment)skills/lemmascript/SKILL.md#L82-L85skills/lemmascript/references/workflow.md#L16-L21skills/lemmascript/references/workflow.md#L24-L28
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@skills/lemmascript/SKILL.md` around lines 51 - 56, Pin all published
LemmaScript CLI examples to a specific release or lockfile-backed invocation.
Update skills/lemmascript/SKILL.md lines 51-56 and 82-85, plus
skills/lemmascript/references/workflow.md lines 16-21 and 24-28, including the
npm install and npx lsc commands; preserve npx tsx
../LemmaScript/tools/src/lsc.ts as the brownfield live-edit path.
Source: Linters/SAST tools
2 participants
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
mainbranch but not yet onorigin/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
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 aftercheck-fmt,lint, andtypecheckpassed;pytestreported 79 passed and 1 failed.Failure detail:
Notes
The failing validation path is unchanged by this branch: rust-entrypoint-system has the same
VERSION_CODENAMElookup onorigin/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:
odw-testingskill 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.fast-checkskill 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.lemmascriptskill that explains how to apply LemmaScript for formal verification of TypeScript, including annotations, Dafny/Lean workflows, and brownfield adoption guidance, with detailed reference guides.