[caelaxie]

synced to d457567. later commits on upstream main through ddf824a do not touch pstack/. version is 0.15.28 in plugin.json, .devin-plugin/plugin.json, and the readme marker.

ported:

• 6b78e9f (#721) create-formal-verification-skill: tla+ is the default for event-order questions in any language, and when no verifier runs on the language the agent says so and tests the real code with generated inputs.
• 7b353f7 (#716) add maintain-formal-verification-skill. create-formal-verification-skill records covered code and the sync commit. poteto-help routing table, guide pages 6 and 9, and recipes mention it. slash commands keep the /pstack: prefix. disable-model-invocation: true stays triggers: [user].
• d457567 (#724) guide page 6 matches the create-formal-verification-skill tool choice, and the version bumps to 0.15.28. the same bump is in .devin-plugin/plugin.json and the readme marker, which is where this repo records the version.

skipped:

• harness/pstack/claude-code/ copies in #721, #716, and #724. this port does not carry the generated claude code tree.
• #724 pstack/.cursor-plugin/plugin.json. cursor packaging. the version bump lands in .devin-plugin/plugin.json instead.
• #716 upstream readme skill-table row for /maintain-formal-verification-skill. this port's readme is a pointer, not a copy of the upstream catalog. the version marker is bumped. the skill is indexed in poteto-help, the guide, and recipes.

  

[caelaxie]

verdict: changes requested (comment review, same-account limit).

content is clean. diffed every changed file against upstream d457567: both formal-verification skills match byte for byte except /pstack: prefixes and disable-model-invocation: true → triggers: [user]. poteto-help, recipes, guide 06 and 09 lines are upstream verbatim modulo prefix, and the 09 anchor resolves to ## Prove a property with a formal verification skill. #716/#721/#724 touched nothing else under pstack/ outside harness/, readme row, and .cursor-plugin/; skips are justified. d457567 is still the latest upstream commit on pstack/. versions 0.15.28 in plugin.json, .devin-plugin/plugin.json, readme. ci green. no issue to link.

blocking: no harness proof. need, on head e63d618:

• devin plugins install (a --local wrapper pinned to the full head sha is fine; symlink-only is not) + devin plugins list showing pstack 0.15.28
• the installed copy showing maintain-formal-verification-skill registered and the changed create-formal-verification-skill / poteto-help text, or a real devin turn invoking them

post it as a comment or in the body and i'll re-review.

[caelaxie]

harness proof

Real Devin CLI on a local box (no cloud agent, no git clone). PR head e63d6180d2bea58fb58c5763ae738106a89c727e (cursor/port-pstack-0.15.28-cae6), expected version 0.15.28.

• CLI: devin 3000.11.92 (7f4e64980e22)
• devin auth status → Logged in (via Devin).
• scratch dir: /workspace/devin-harness/scratch
• model used by every run: swe-2-high
• permissions: the same read-only project allowlist as port upstream pstack through 0.15.27 #10/state ~/.devin as the only pstack-models source #11. Writes and edits are denied, and I did not use bypass/dangerous.

#	step	result
0	clean removal of the #11 wrapper + pstack	✅ PASS
1	install via a wrapper pinned to the full head sha	✅ PASS
2	devin plugins list shows pstack v0.15.28	✅ PASS
3	installed copy matches e63d618 (new and changed files)	✅ PASS
4	/pstack:create-formal-verification-skill (describe-only)	✅ PASS
5	/pstack:maintain-formal-verification-skill (describe-only)	✅ PASS
6	/pstack:poteto-help	✅ PASS (see note)

None of the three skill runs hit a permission rejection. Afterwards, ~/.devin/rules and ~/.config/devin/agents still do not exist, and the scratch dir contains only .devin/.

0. clean slate

$ devin plugins list
  • pstack-harness-pr11 v0.0.0
  • pstack v0.15.26 (required)
$ devin plugins remove pstack-harness-pr11 --local
✓ Removed pstack-harness-pr11.
  note: auto-installed required plugins were left in place: pstack
$ devin plugins remove pstack --local
✓ Removed pstack.
$ devin plugins list
No plugins installed.
$ ls ~/.local/share/devin/cli/plugins/cache/*
ls: cannot access '/home/box/.local/share/devin/cli/plugins/cache/*': No such file or directory

1–2. install + list

$ cat /workspace/devin-harness/wrap-pr12/.devin-plugin/plugin.json
{ "name": "pstack-harness-pr12", "version": "0.0.0",
  "requiredPlugins": [ { "source": "github", "repo": "pstack-ports/devin-pstack",
                         "sha": "e63d6180d2bea58fb58c5763ae738106a89c727e" } ] }
$ devin plugins install --local -y /workspace/devin-harness/wrap-pr12
  ...
✓ Installed pstack-harness-pr12.
  auto-installed required plugins: pstack
$ devin plugins list
Installed plugins

  • pstack-harness-pr12 v0.0.0
  • pstack v0.15.28 (required)
$ devin plugins info pstack | head -3
Plugin: pstack
  version: 0.15.28
  source: https://github.com/pstack-ports/devin-pstack

3. installed copy (~/.local/share/devin/cli/plugins/cache/github.com_pstack-ports_devin-pstack-816793bb/0.15.28)

These are sha256 prefixes of each installed file, compared with raw.githubusercontent at e63d618 and at main. The main=e3b0c442… value is the hash of an empty file: the new skill does not exist on main.

$ grep -n "\"version\"" .devin-plugin/plugin.json plugin.json
.devin-plugin/plugin.json:3:  "version": "0.15.28",
plugin.json:4:  "version": "0.15.28",
# sha256 prefix: installed vs raw @e63d618 vs raw @main
skills/maintain-formal-verification-skill/SKILL.md installed=076f7ff038af0134 pr12=076f7ff038af0134 main=e3b0c44298fc1c14
skills/create-formal-verification-skill/SKILL.md installed=db78eb6bfb5c46c3 pr12=db78eb6bfb5c46c3 main=94f05a20768ff477
skills/poteto-help/SKILL.md installed=916f073676babe46 pr12=916f073676babe46 main=a174dfbde399ecc4
skills/poteto-help/references/recipes.md installed=778848f84af1004c pr12=778848f84af1004c main=0053c965f6161025

The new maintain-formal-verification-skill/SKILL.md exists in the installed copy:

$ ls -l skills/maintain-formal-verification-skill/SKILL.md
-rw-r--r-- 7019 skills/maintain-formal-verification-skill/SKILL.md
$ head -8 skills/maintain-formal-verification-skill/SKILL.md
---
name: maintain-formal-verification-skill
description: "Bring a project's formal verification back in line with the code after the code changes: find the commits that touched verified code, update the model, harness, or properties to describe the code as it is now, rerun, and say whether each failure 
triggers: [user]
---

# Maintain a formal verification skill

Changed lines in the installed create-formal-verification-skill/SKILL.md (TLA+ default, the fallback when no verifier exists, and the pointer to maintain):

$ grep -n -o -E ".{0,60}TLA\+ is th.{0,160}|.{0,40}no verifier.{0,160}|.{0,30}maintain-formal-verification.{0,80}" skills/create-formal-verification-skill/SKILL.md
19:suits a model checker over a small model of the design, and TLA+ is the default for that in any language. Whether the code itself behaves for every input, as with memory safety, overflow, or a data-structure invariant, usually sui
19:ts a verifier that runs on the code. If no verifier runs on this language, say so, and test the real code with generated inputs, not a hand model of the function. A property that must hold at every size, where a
41:e. Point the user at `/pstack:maintain-formal-verification-skill` for bringing the verification back in line after changes that did not re

New lines in the installed poteto-help: the bullet, the maintain-formal-verification table row, and the recipe:

$ grep -n maintain-formal-verification skills/poteto-help/SKILL.md skills/poteto-help/references/recipes.md
skills/poteto-help/SKILL.md:29:- No formal verification skill in the project means no property is checked past what tests reach. Mention `/pstack:create-formal-verification-skill` when the question is about a race, an invariant, or another case tests rarely hit. When one exists and the code it covers changed after the commit it 
skills/poteto-help/SKILL.md:86:| Bring a formal verification back in line after the code it covers changed, and learn whether a failure is drift or a bug | [`/pstack:maintain-formal-verification-skill`](../maintain-formal-verification-skill/SKILL.md) |
skills/poteto-help/references/recipes.md:37:- `/pstack:create-formal-verification-skill prove <property> holds in <module>, even when <steps> interleave or retry.` After merges or refactors in that code: `/pstack:maintain-formal-verification-skill`.

4. create-formal-verification-skill

$ devin -p --respect-workspace-trust false --export ../logs/pr12-create.export -- '/pstack:create-formal-verification-skill DESCRIBE ONLY: do not write, edit, or create any files, and do not install anything. This scratch dir has no code. In a few short lines, say which tool you would default to for checking that two retrying workers never both commit the same job, what you would do if no verifier ran on the language, and what you would record so the check stays in step with the code. Then stop.'
USER-MSG head (skill body injected): # Create a formal verification skill | | A test checks the cases that someone thought to write. ...

**Tool default:** TLA+ with TLC. "Two retrying workers must never both commit the same job" is a question about event orderings under retries — exactly what a model checker over a small design model answers. ...
**If no verifier ran on the language:** I'd say so plainly rather than build a hand model of the function and pretend it checks the code. I'd test the real code with generated inputs — e.g. property-based tests ... and report that as bounded empirical evidence, not verification.
**Keeping it in step with the code:** Record in the skill the exact files/functions each modeled step covers, the atomic-step mapping ..., and the git commit where I last confirmed the model still describes that code. ...
exit=0

5. maintain-formal-verification-skill

$ devin -p --respect-workspace-trust false --export ../logs/pr12-maintain.export -- '/pstack:maintain-formal-verification-skill DESCRIBE ONLY: do not write, edit, or create any files. Look for formal verification checks in this directory (read-only), report what you find, then in a few short lines list the outcomes you would assign a check and the steps of a pass. Then stop.'
USER-MSG head (skill body injected): # Maintain a formal verification skill | | A formal check proves a property of what it describes. ...
TOOL: exec ls/find (read-only)   TOOL: skill {"command": "search", ...}

- No verify skill exists here (searched skills across all providers; nothing found).
- No formal checks: no TLA+/Alloy/Dafny/P models, no harnesses, no property files, no test specs.
Per step 1 of the pass: with no verify skill present, the correct move is to stop and point at `/pstack:create-formal-verification-skill` rather than invent checks.
**Outcomes I'd assign to a check**
- `in sync` ... - `updated` ... - `bug` — ... a finding about code, not drift. (Can coincide with `updated`.) - `blocked` — ... don't advance the sync commit.
**Steps of a pass**
1. Find the check(s) ... 2. Run each check unchanged ... 3. Diff covered code from sync commit to HEAD; classify each change ...
4. Update the model or harness from the code, not from the result ... 5. Rerun: on pass, break the code ... on fail, replay the counterexample ...
6. Update the verify skill's coverage, commands, bounds, and sync commit (never for a blocked check) ...
Nothing was written or edited.
exit=0

6. poteto-help

$ devin -p --respect-workspace-trust false --export ../logs/pr12-help.export -- '/pstack:poteto-help my formal verification check still passes after a big refactor of the code it covers; which pstack skill should I use? keep it short'
TOOL: read {"file_path": ".../0.15.28/skills/maintain-formal-verification-skill/SKILL.md"}

`/pstack:maintain-formal-verification-skill` — and yours is exactly the case it's for. A check that keeps passing after a refactor may be proving a property of code that no longer exists. ...
    /pstack:maintain-formal-verification-skill — the code under the check was just refactored; confirm the pass is still a real proof
https://github.com/pstack-ports/devin-pstack/blob/main/skills/maintain-formal-verification-skill/SKILL.md
exit=0

Note: the link it gives points at main, where this file doesn't exist until this PR merges, so it 404s for now. This is expected for a pre-merge run, not a defect in the port.

No code was changed and no secrets appear in this comment.

[caelaxie]

verdict: approved (comment review, same-account limit).

harness proof in #12 (comment) holds on head e63d618:

• devin plugins install --local via a wrapper pinned to the full head sha e63d6180d2bea58fb58c5763ae738106a89c727e, with devin fetching from github (not a symlink). it started from a clean slate after removing the #11 wrapper.
• devin plugins list / info show pstack v0.15.28.
• the installed cache copy has maintain-formal-verification-skill/SKILL.md with triggers: [user], and the changed create-formal-verification-skill lines (tla+ default, the no-verifier fallback, the maintain pointer) plus the poteto-help bullet, table row, and recipe. the sha256 of each installed file matches raw @ e63d618 and differs from main.
• all three skills ran in real devin turns with exit 0. there were no permission rejections and nothing was written.

content was already verified against upstream d457567, and ci (Validate plugin) is green on the head. squash-merging pinned to e63d618.