Repository navigation
Conversation
Vendor the quint-lang and quint-modeling skills from the Quint LLM Kit at a pinned commit, and add a proxy-quint skill for the rules specific to Proxy: TLC is part of the checks, properties are fixed, a finding needs a failing test first, trace every lifecycle hook on a path, and add a mutation and a witness for each new rule and action. CLAUDE.md points to it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The earlier commit meant to add this pointer through CLAUDE.md, which is a symlink to AGENTS.md, so the edit was left unstaged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Add quint:install and quint:check mise tasks, put the pinned Quint CLI in specs/quint on PATH for tools such as Quint Connect that call `quint` directly, and document both in DEVELOPMENT.md. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
tobyhede
force-pushed
the
claude/project-thread-98m2dc
branch
from
October 26, 2026 01:48
8b935bd to
16ecb9f
Compare
tobyhede
pushed a commit
that referenced
this pull request
Oct 26, 2026
tobyhede
changed the title
- Use mise's `usage` spec for the quint:check stage, replacing the
deprecated `{{arg()}}` template.
- Name the mapped Rust files in the AGENTS.md pointer, so it can fire
from a diff, and widen the skill description to adding and reviewing
models.
- In proxy-quint: separate requirements changes from implementation
changes, bound the path trace by the code rather than the table, list
all four places a finding is recorded, note the mutate() limits, run
`check.sh all` in the background, and say how to run the pinned CLI.
- Scope the tracker-ID rule to the public model files.
- Note that quint-execute-spec is not vendored.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
tobyhede
pushed a commit
that referenced
this pull request
Oct 26, 2026
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Requested by Toby
This is the base of a stack: #485, the Quint model of statement routing, builds on this PR, which adds the agent skills and tooling for it.
Merge this one first.
Agent skills
quint-langandquint-modelingfrom quint-co/quint-llm-kit into.claude/skills/. They are pinned to commitcc75369and keep their Apache-2.0 licence..claude/skills/VENDORED.mdexplains how to update them.proxy-quintskill with the rules specific to Proxy:Context::begin_*/finish_*hook.AGENTS.md, whichCLAUDE.mdlinks to.Tooling
quint:installandquint:checkmise tasks.specs/quint/node_modules/.binonPATH, so Quint Connect, which runs barequint, will use the pinned CLI.DEVELOPMENT.md, including the Rust-backend download gotcha.specs/quint/itself arrives with #485, so until #485 merges the skill and the mise tasks refer to files that don't exist yet.The witness enforcement and the source-file correspondence table that used to be in this PR are now in #485.
Testing
Acknowledgment
By submitting this pull request, I confirm that CipherStash can use, modify, copy, and redistribute this contribution, under the terms of CipherStash's choice.
🤖 Generated with Claude Code