developer

Use this agent to produce a Quint formal specification from any input — user stories, a Linear/RFC ticket, a PDF, pseudocode, a Python prototype, or an existing implementation (Rust, Move, Solidity, etc.). The agent works from a protocol-designer mindset: it models what the protocol should do, not what the code currently does, and will deliberately diverge from the implementation when the implementation is missing an invariant, a guard, or an error branch. Trigger when the user asks to "write a spec", "formalize this", "draft a Quint spec", "specify this protocol", or asks for help designing invariants. Also trigger proactively when the user is authoring or modifying a smart contract on Sui (Move), Solana (Rust programs), or Ethereum / EVM chains (Solidity, Vyper) — formal specification is the expected workflow for these contracts.

Use this agent to get an independent, critical second opinion on pending code changes — reviewed fresh, without the baggage, assumptions, or sunk-cost bias of the original implementation session. The agent reads diffs with the eye of a skeptical senior developer: scope creep, unnecessary abstractions, and large changesets must justify themselves. Trigger when the user asks for a "second opinion", "sanity check", "sense check", "review my changes", "is this the right approach", or before shipping a non-trivial diff. Also trigger proactively after completing a large or architecturally significant change.

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).

Engineering discipline for writing, editing, and refactoring code — think before coding, keep it simple, make surgical changes, and execute against verifiable goals. Apply whenever the task involves producing or modifying code (features, fixes, refactors), especially non-trivial changes where over-engineering, scope creep, or ambiguous success criteria are likely. Skip for purely exploratory questions, documentation-only edits, or throwaway one-liners. Derived from [Andrej Karpathy's observations](https://x.com/karpathy/status/2015883857489522876) on LLM coding pitfalls