Formalos Verification Plan — VS Code Extension

Brings your Formalos verification plan into the editor: navigate goals → requirements → tasks/assertions, see milestone health, and update task status & burndown without leaving VS Code. The plan in formalos-vp-creator (Postgres) is the single source of truth — the extension reads it and writes status changes back.

Features (Phase 1)

Bind a workspace to a plan — Formalos: Bind Workspace to Plan picks from the plans you can see and stores the binding in workspace settings.
Plan view — Milestones (with on-track / at-risk / behind health), Requirements grouped by goal (with checked / no proof / progress badges), their Tasks and connected Assertions, plus plan-level tasks.
My Tasks view — your open tasks for the active milestone.
Status bar — milestone health at a glance; click to focus the plan.
Write-back — right-click a task to Start, Mark in review, Mark done, or Set remaining days. Changes PATCH straight to the plan (gated by your edit role) and the rollup/burndown update. Optimistic, then reconciled.
Offline tolerant — the last good plan is cached; a banner shows when you're seeing cached data.
Jump to code — with a committed .formalos.map.json, Open Related File on a requirement/assertion opens the mapped RTL/SVA file (see .formalos.map.example.json).

Coverage, progress and burndown are computed with the same logic as the web app (ported in src/model.ts), so the editor and dashboard always agree.

Settings

Setting	Purpose
`formalosVp.apiBaseUrl`	vp-creator base URL (no trailing slash).
`formalosVp.clerkPublishableKey`	Clerk publishable key — OAuth endpoints are derived from it.
`formalosVp.oauthClientId`	Clerk OAuth Application client id for sign-in.
`formalosVp.planId`	The bound plan (set via the bind command; per-workspace).

Backend API (in formalos-vp-creator)

The extension talks to additive, Bearer-authenticated routes:

GET /api/v1/plans — plans the caller can see (bind picker).
GET /api/v1/plans/:id — goals, requirements, execTasks, assertions, milestones, plus the computed rollup. Visibility-gated.
PATCH /api/v1/tasks/:id — update task status / remainingDays (editor role required).

Develop

npm install
npm run compile        # esbuild bundle → dist/extension.js
npm run watch          # rebuild on save
npm run typecheck
npm test               # vitest (model selectors + health)

Launch the Extension Development Host:

"/Applications/Visual Studio Code-5.app/Contents/Resources/app/bin/code" \
  --extensionDevelopmentPath="$PWD" --new-window

(or open this folder in VS Code and press F5).

End-to-end (local)

Run vp-creator locally with DEV_AUTH_BYPASS=1 (skips Clerk).
In the dev host, run Formalos: Bind Workspace to Plan and pick a plan.
The Plan / My Tasks views populate from the real DB; the status bar shows milestone health.
Right-click a task → Mark done and confirm it persists in the web app's Execution view (and the burndown updates).

For a live (non-bypass) instance, create a Clerk OAuth Application with redirect URI vscode://formalos.vp-creator/auth-callback (scopes openid/profile/email), set formalosVp.oauthClientId, and sign in via the Sign in to load your plan prompt.

Roadmap

Phase 2 — tool-agnostic proof runner (JasperGold / VC Formal / SymbiYosys / custom) run as a VS Code Task.
Phase 3 — close the loop: proof results auto-update assertion status + burndown.
Phase 4 — SVA ↔ assertion CodeLens and counterexample triage in-editor.

FormalOS VP Creator

formalos