[athul-ramesh]

What changed upstream

Upstream pstack 99743e9...e73df47 (0.15.25 to 0.15.32 plus follow-ups). I read all 32 commits that touch pstack/. Tip covered: e73df471cd4bd918367e99f3dd9c51bd53ddf5f0.

Branched from current main (28917b5). #8 and #9 are merged.

Ported

• TypeScript brands (#700): the Branded types row and the AgentId example now use an isAgentId type guard, not as.
• Sharpen (#712, #729): ported in its final form. The skill uses the four numbered asks and returns only the rewritten prompt. Help, recipes, README, and the usage guide are updated to match.

Adapted for Devin

• Ketchup (#692, #708): the story stays under 100 words. Each waiting item gets about 30 words with its link, user change, evidence, risk, and pick. Items are never cut to meet a word count. Pictures still render only when the Devin host renders them, and the text fallback stays.
• Formal verification (#709, #721, #716, #724, #715): this adds two explicit-user skills, /pstack:create-formal-verification-skill and /pstack:maintain-formal-verification-skill. Generated skills go under .devin/skills/. The plugin bundles no verifier. Before using a tool, the agent checks that it runs with exec and records its version. It asks before installing a toolchain, and a check that could not run is reported as blocked, never as passed. The TLA+ default and the fallback to testing the real code with generated inputs are kept. Maintenance stops at merge-ready. The help state check, routing rows, recipes, README, and usage guide are updated.
• Reflect (#800): reflect no longer edits a skill inside an installed plugin. devin plugins update re-fetches remote plugins, and a --local plugin is linked to its checkout. Reflect shows each edit's destination before approval, then copies the skill to .devin/skills/<skill>/ or ~/.config/devin/skills/<skill>/ and edits the copy. It opens no PR and does not push. The copy is a separate /<skill>, and /pstack:<skill> stays unchanged.
• Skill names (#702): this port already met the rule. A new contract test enforces folder-named skills.
• Version 0.7.0, release notes, README, docs/pstack-0.15.32-port-audit.md, and new contract tests.

Devin compatibility checks

• Creating skills: triggers: [user], name, and the directory as the identifier. Frontmatter is optional, so the generated-skill wording no longer says a skill without frontmatter never registers.
• Skills overview: the project and global skill paths used by formal verification and reflect.
• Plugins: devin plugins info, devin plugins update re-fetch, and --local folder links (used by the reflect adaptation).
• CLI changelog: it documents image attachments as input but no inline image, video, or Mermaid output in the CLI. That is why ketchup keeps its fallback and statechart and ketchup-video are left out.
• None of these changes touches profiles, pins, hooks, run_subagent contracts, or delivery authority.

Skipped or uncertain

• Statechart (#741, #776, #779, #791) and #794's /statechart hook: uncertain. This is about 12k lines of Node scripts and tests. It installs TLC and Java through mise (about 305 MB), renders PNGs with Pele and resvg, and expects the agent to look at each PNG. Devin documents no inline image output. It needs its own port with a native test.
• ketchup-video (#797): uncertain. It needs a video renderer and inline video. Devin documents neither, and this plugin ships no renderer.
• Setup offer for formal verification (#715): skipped. This port's setup only writes the role sheet and has no verification-offer step to extend.
• watch-pr and orch (#801, #802, #804): not applicable because those Bun scripts are not shipped. worktree-audit.sh already prefers an open PR.
• check-plan inline code (#803): not applicable because this port's validator has no prose lint.
• worktree-audit GNU stat (#805): not applicable because this port reads no transcript mtimes.
• Swarm numbering (#807): this port already meets it.
• Claude Code only (#637, #705, #806) and the Cursor docs refresh with its docs-vs-tree script (#704): skipped.
• Version bumps (#710, #713, #792, #798): the plugin is bumped independently to 0.7.0.

Verification

node --test tests/*.test.mjs: 53 pass, 0 fail. The new folder-name test fails as expected when a skill name is changed. git diff --check is clean. These are static checks. Native activation of 0.7.0 in Devin, a real TLA+ or other verifier run through the new skills, and inline rendering are untested.