FormalOS VP Creator for VS Code

Your verification plan, where the work actually happens.

Formal verification lives in the editor — writing SVA, running proofs, triaging counterexamples. But the plan that says what to verify and whether you're on track usually lives in a browser tab you keep forgetting to update. So it goes stale, and status meetings turn into guesswork.

FormalOS VP Creator closes that gap. Your whole verification plan comes into VS Code — goals, requirements, tasks, milestones, the lot — and every change you make flows straight back to the team's single source of truth in FormalOS. No copy-paste, no browser round-trips, no end-of-week status archaeology.

Sign in with your FormalOS account and your projects are right there in the sidebar: live, editable, and always in sync.

Why you'll like it

📋 The plan, in your sidebar

Every project you can access — organized by customer and customer-project — one click away. Open a plan and its goals, requirements, tasks, assertions and milestones populate instantly, with coverage and progress computed exactly the way the web app computes them. What you see here is what the team sees.

✅ Task management that fits how you actually work

A My Tasks panel that puts the focus on the work: filter to your open tasks, a milestone, or a single requirement with one tap. Group by status, expand subtasks, drag to reorder, and add a task inline — no dialogs in your face. Open any task to edit it in place: status, effort in days and hours (1d 4h), milestones, the owning requirement, shared requirements, a description, subtasks, duplicate, delete. Mark something done and the burndown updates itself.

✍️ Build the plan, not just track it

Add goals and requirements right from the editor — name a goal, give it a shortcut, drop in requirements (their IDs are minted for you), rename or remove with a double-click. The plan grows as your understanding does, without ever leaving your RTL.

📊 Know exactly where you stand

A branded dashboard with an animated coverage donut, a requirement status wall, per-goal coverage rings, a Needs attention panel (failing proofs, uncovered requirements, slipping milestones), and a milestone timeline with a today line. Milestone health — on track / at risk / behind — also rides along in the status bar, so you always have a read at a glance.

💬 Talk to your team, in context

Comment on any task or requirement, reply, resolve, and @mention teammates — the same threads the web app shows, anchored to the same items. A bell badge keeps your unread mentions in view, and an inbox jumps you straight to them.

🔗 From requirement to RTL in one jump

Commit a small .formalos.map.json and Open Related File takes you from a requirement or assertion straight to the SystemVerilog that implements it.

🛟 Always current, even off the grid

The plan is the single source of truth — the extension reads it and writes your status changes back, role-gated, optimistically, then reconciled. Lost your connection? The last good plan stays cached with a clear "stale" badge. And new versions arrive automatically.

Getting started

1. Install the extension (you're here).
2. Click the FormalOS icon in the Activity Bar.
3. Sign in with your FormalOS account — zero setup, the extension configures itself.
4. Pick your project and start working.

That's it. Everyone with a FormalOS login can see their own plans immediately.

Good to know

• Built for the LUBIS EDA FormalOS platform. You'll need a FormalOS account; the extension talks to your team's FormalOS instance.
• Your role is respected. Viewers see everything read-only; editors can change the plan. The extension never lets you do something the web app wouldn't.
• Pointing at a self-hosted instance? Set FormalOS VP: Api Base Url in Settings. Everything else is automatic.

On the roadmap

We're building toward closing the entire loop without leaving the editor:

• Run proofs from VS Code — a tool-agnostic runner (JasperGold, VC Formal, SymbiYosys, or your own flow) launched as a task.
• Results that update the plan for you — convergence and counterexamples flow back into assertion status and burndown automatically.
• In-editor triage — SVA ↔ assertion CodeLens and counterexample inspection right where you write the code.

FormalOS VP Creator is an internal tool by LUBIS EDA.