Verification run: thirdshift creates and maintains a repository's verification skills unattended #883

This was generated by AI during triage.

Idea

Add a new Pass: thirdshift verify, shaped like thirdshift architect. Where an Architect run reviews the Base branch's architecture and acts on its plan, a Verification run would run one of these skills unattended and open a pull request:

• create-formal-verification-skill: pick the code where a bug costs the most and tests reach the least, and model-check one property of it.
• maintain-formal-verification-skill: bring the existing checks back in line with commits that skipped them. Each check comes out in sync, updated, bug or blocked.
• Possibly create-verification-skill and maintain-verification-skill as well, for repositories whose user surface an agent can drive (a web UI, an API), where scripted proof of behavior is the gap.

At that point these skills move into the Factory skills (skills/thirdshift-*) as headless adaptations, like thirdshift-improve-codebase-architecture.

Follows from

#881 adds the first formal check to thirdshift itself as a repository skill. A Verification run generalizes that to any repository thirdshift runs on.

Questions to shape before this is ready

• Choosing the mode. Create when no verify skill exists and maintain when one does? Or pick from commits to covered code since the recorded sync commit, and skip when none touched it, so the pass is quiet when it has nothing to do (ADR-0009)?
• Where a finding goes. A bug outcome is a finding about product code, and these skills never edit product code. Should it become an issue for the Day shift, possibly private like Security findings (ADR-0015)? The verification update itself goes in its own pull request.
• Skips. Should it skip the way an Architect run does: while a Ready issue exists, while its own pull request is open, or under another Pass?
• Driving the real app. Driving a target app's real user surface means launching servers and browsers unattended on the user's machine. What should a Run be allowed to start (ADR-0013)?
• Tool setup. Installing a checker (a JVM for TLC, and so on) on the user's machine is outside what Setup does today.