From developer
This skill should be used when the user asks to "formalize" a requirement, "convert this into spec", "write a Quint spec", "specify X formally", "translate this into Quint", or wants to produce a Quint model from informal inputs (user stories, PDFs, pseudocode, Python prototype, or existing implementation code such as Rust). Also AUTO-TRIGGER proactively whenever the user is writing, modifying, or reviewing a smart contract on Sui (Move — `.move` files, `Move.toml`), Solana (Rust programs — `solana_program`, `anchor_lang`, `#[program]` modules), or Ethereum / EVM chains (Solidity — `.sol` files, Vyper — `.vy` files) — formal specification in Quint is the expected workflow for these contracts and the skill should surface even when formalization is not explicitly requested. Guides a three-phase workflow — draft spec, negotiate invariants with the user, write comprehensive tests — targeting the Quint language (https://quint.sh).
npx claudepluginhub phi-labs-ltd/claude --plugin developerThis skill uses the workspace's default tool permissions.
Translate informal requirements into a Quint specification, agree on invariants with the user, and write comprehensive Quint tests that exercise them. Target language: Quint (https://quint.sh).
Searches, retrieves, and installs Agent Skills from prompts.chat registry using MCP tools like search_skills and get_skill. Activates for finding skills, browsing catalogs, or extending Claude.
Searches prompts.chat for AI prompt templates by keyword or category, retrieves by ID with variable handling, and improves prompts via AI. Use for discovering or enhancing prompts.
Checks Next.js compilation errors using a running Turbopack dev server after code edits. Fixes actionable issues before reporting complete. Replaces `next build`.
Translate informal requirements into a Quint specification, agree on invariants with the user, and write comprehensive Quint tests that exercise them. Target language: Quint (https://quint.sh).
Invoke this skill whenever the user wants to produce a Quint spec from any of:
Trigger phrases: "formalize", "convert this into spec", "write a Quint spec", "translate this to Quint", "specify this formally", "model this in Quint".
This skill is expected to activate proactively — not only on explicit formalization requests — whenever the user is authoring, modifying, or reviewing a smart contract on any of the following platforms:
| Platform | Languages / markers |
|---|---|
| Sui | Move (.move), Move.toml, module <addr>::<name> { ... } |
| Solana | Rust programs using solana_program, anchor_lang, #[program], #[account], declare_id! |
| Ethereum / EVM | Solidity (.sol), Vyper (.vy), pragma solidity, contract X { ... } |
When this trigger fires:
Not every edit warrants a spec — trivial renames, comment fixes, dependency bumps, and test-only changes are out of scope. Trigger when the edit changes contract behaviour (new function, new branch, new state variable, modified formula, modified access check).
The work proceeds in three phases. Do not skip ahead — pause between phases for the user to review.
spec/types.qnt (shared across modules in the project) and the spec itself in spec/<module>.qnt. See references/spec-structure.md for the full module anatomy.init_with / init, actions, and step. Leave the invariants section empty or with a // TODO marker.Do not invent behaviour the source does not specify. When the source is ambiguous, surface the ambiguity to the user rather than picking silently.
Structured requirement documents (Linear tickets, product specs, RFCs) typically contain sections such as Problem, Solution, User Stories with acceptance criteria, Current Behavior, Implementation, and Testing. Apply these rules:
admin_register_pair, feeder_update_price).actions. If the story refers to multiple related operations, each typically becomes its own action.Invariants are the highest-value part of the spec and the user's expertise matters most here. Drive the conversation with targeted questions, not a dump of suggestions.
Run this loop:
references/invariant-patterns.md for the catalogue). Typical starters:
price_outlier.)"val in the module, using match over the result type so error branches are handled vacuously (FilterErr(_) => true). See the invariant catalogue in references/invariant-patterns.md.result variable, because result lags prices between action steps. The inv_hedging_venue_preserved pattern in the example shows the fresh-recompute idiom — apply it whenever an invariant must hold across partial sequences.Continue until the user is satisfied with coverage.
Once the spec and invariants are agreed, write deterministic tests in spec/<module>.tests.qnt. Use init_with(...) to pin parameters; reserve the nondet init for quint run simulation. Drive the state machine with .then(action(...)) chains.
Aim for these categories — propose each and confirm coverage is enough:
FilterErr branch of the spec.NoHedging).Name tests after the behaviour they assert, not the input: test_hedging_venue_exempt_from_outlier over test_case_3.
After drafting, run quint test spec/<module>.tests.qnt and quint run spec/<module>.qnt --invariant inv_<name> for each invariant. Fix any failures before handing back.
spec/types.qnt. Re-use them across spec modules. Mirror existing implementation types field-for-field and add a one-line // Mirrors <path> comment.spec/types.qnt, spec/<module>.qnt, spec/<module>.tests.qnt.pure def should be — state machines should only orchestrate it.Ok(...) variant and a domain-specific error variant (e.g., FilterErr(str)). Invariants pattern-match on the result type and return true vacuously for the error branch.quint-connect hooksquint-connect replays spec traces against a live implementation. Include the integration hooks only when mirroring an existing implementation and trace replay is intended:
ActionTaken ADT and a var action_taken.action_taken' to a concrete variant.bid == ask if the implementation uses microprice).For PDF / user-story / prose inputs where no implementation exists, omit ActionTaken and these constraints. See references/quint-connect.md.
| Command | Purpose |
|---|---|
quint test spec/<module>.tests.qnt | Run deterministic run tests. |
quint run spec/<module>.qnt --invariant <name> | Randomised simulation checking an invariant. |
quint verify spec/<module>.qnt --invariant <name> | Bounded model check via Apalache. |
quint typecheck spec/<module>.qnt | Type-check without running. |
references/quint-cheatsheet.md — syntax primer (types, actions, pure defs, list/set ops, pattern matching, nondet, .then, run).references/spec-structure.md — detailed module anatomy and section ordering.references/invariant-patterns.md — catalogue of invariant shapes with the fresh-recompute idiom.references/quint-connect.md — Rust trace-replay integration details.