⌘K for palette
All 0
CWEs 0
Scans 0
Proofs 0
Pages 0
🔎
Search across everything
CWE catalog · Scan history · Rocq proofs · App pages
●
v1.20 · AI Autofix + Project Mode
Formally-verified
Python security analysis
Every safe verdict carries a machine-checked proof you can re-check yourself.
No credit card required
Self-hosted analysis engine · runs on your own server
app.py
CWE-89 SQL InjectionCWE-79 XSSCWE-502 DeserializationCWE-78 Command InjectionCWE-22 Path TraversalCWE-918 SSRFCWE-327 Weak CryptoCWE-798 Hardcoded CredsCWE-611 XXECWE-601 Open RedirectCWE-90 LDAP InjectionCWE-94 Eval/Code ExecCWE-117 Log InjectionCWE-862 Missing Auth
CWE-89 SQL InjectionCWE-79 XSSCWE-502 DeserializationCWE-78 Command InjectionCWE-22 Path TraversalCWE-918 SSRFCWE-327 Weak CryptoCWE-798 Hardcoded CredsCWE-611 XXECWE-601 Open RedirectCWE-90 LDAP InjectionCWE-94 Eval/Code ExecCWE-117 Log InjectionCWE-862 Missing Auth
98
CWE classes
0
FP · 222-file + Ext-174
<10ms
Avg scan time
125
machine-checked proofs
Proof-carrying analysis pipeline
Every scan flows through five stages. Watch the pulse trace the path.
Parse
AST + alias map
Trace
Inter-proc taint
Solve
Z3 witness search
Certify
Rocq theorem match
Decide
4-way verdict
Built for developers who ship
Every finding comes with machine-checked proof. One false alarm across 1,626 benchmark files — and it's documented.
Proof certificates
Unlike statistical SAST, every SAFE verdict is backed by a machine-checked proof, produced with the Rocq proof assistant. Audit-ready.
AI auto-fix
One-click before/after diff for 8 common CWEs (SQLi, XSS, pickle, path traversal, cmd, eval, weak crypto).
Sub-10ms analysis
AST + Z3 symbolic execution. Scan on every keystroke. No cloud round-trip.
Near-zero false positives
99.8% precision on OWASP 1,230 (a single FP); 100% precision with zero FP on the 222-file and Ext-174 curated sets. F1 96.5% vs Bandit 56%, Semgrep 40%, CodeQL 34%.
Repository-scale scans
Select many files at once in the browser, or send a whole repository to the project API and get new-vs-closed against the previous scan.
Verified security badge
Earn README-embeddable SVG badges on clean scans. Show customers you care about code quality.
Head-to-head
F1 across three Python benchmarks (paper v41, Table 1). Higher is better.
| Tool | OWASP | 222-file | Ext-174 |
|---|---|---|---|
| Prove v1 | 96.5% | 100.0% | 100.0% |
| Bandit | 55.7% | 74.6% | 76.1% |
| Semgrep | 40.4% | 44.6% | 46.3% |
| CodeQL | 34.4% | 18.0% | 20.0% |
Prove precision is 100% on all sets except OWASP (99.8%, 1 FP). On the out-of-distribution SecurityEval set Prove attains F1 0.554 vs Bandit 0.370 / Semgrep 0.364.
Talk to us about a pilot
Prove is adopted through a conversation, not a checkout. Tell us what you are shipping and we will set up an evaluation on your codebase.
Free, no account needed
60 scans/min, one file at a time
- ✓ 98 CWE classes, full verdict set
- ✓ Machine-checked certificates — the part nobody else has, not paywalled
- ✓ 125 Rocq proofs, browsable
- ✓ AI autofix on a single file
- ✓ Audit report export
Pro — arranged with us
For teams putting this in front of a real repository
- ✓ Whole-repository scans over the project API, with new-vs-closed against your last scan
- ✓ Scoped API tokens for CI and other machine-to-machine use
- ✓ Shared defect tracking — stable identity across scans, status, assignee, comments, append-only history (API today; no web UI for it yet)
- ✓ Project-wide AI autofix across every affected file
- ✓ On-premise install and support terms, agreed in the contract
Frequently asked questions
If you can't find your answer, message woohyunchoi@provelabs.co.kr.
Does my code leave my machine?
No. In local mode, scanning happens entirely in your browser's connected Python backend. Even Agent Mode uses a local LLM (Ollama via OpenCode) — your code never crosses a network boundary unless you explicitly opt into a remote provider.
How is this different from Bandit or Semgrep?
Bandit and Semgrep are pattern-based. They miss 40-70% of real CVEs. Prove uses symbolic execution (Z3) plus formal Rocq proofs — every SAFE_WITH_CERT verdict is mathematically certified. On the OWASP Python benchmark, Prove scores F1=96.5% (99.8% precision, 1 FP), vs Bandit 55.7% / Semgrep 40.4% / CodeQL 34.4%.
What does the AI Agent actually do?
It runs an autonomous loop: scan → generate patch → re-scan to verify → escalate to a stronger model if vulns remain. Up to 3 iterations. Cross-engine verification means the AI can't claim it fixed something the real analyzer still flags.
Which CWEs are supported?
98 classes across data-flow (CWE-89, 78, 79, 502, 918) and structural (CWE-327, 798, 22, 502, 611, 754, 862, 295, 614, 532). All OWASP Top 10 (2021) covered. Browse the full CWE Catalog.
Can I integrate this into CI/CD?
Yes. Use the REST API (POST /api/analyze) from any GitHub Action, GitLab pipeline, or pre-commit hook — one file per call, no token required. Pro adds /api/v1: a scoped API token, whole-repository scans in one call, and defects that persist between runs so a pipeline can fail on what is new. There is no packaged Action yet — you call the endpoint yourself.
What languages are supported?
Python today (full coverage). JavaScript/TypeScript and Go on the roadmap.
Start scanning in under 10 seconds
No signup. No credit card. Just paste code and go.
Privacy
Terms of Service
Security
Privacy Policy
Effective 2026-04-24 · Last updated 2026-04-24
Prove is a developer tool for security analysis. We respect your privacy and collect only what's necessary to operate the service.
1. What we collect
Client-side (browser localStorage)
- Scan history — your analyzed code stays in your browser in local mode.
- Settings — theme, density, API keys, notification preferences
Server-side (hosted deployments only)
- Code submissions — sent via
/api/analyze, processed in-memory, NOT persisted - IP addresses — rate limiting only (60 req/min); discarded after 60s
2. How we use it
Data is used exclusively to (a) execute requested analysis, (b) prevent abuse, (c) improve detection rules. We do not train AI models on your code.
3. Sharing
We do not sell, rent, or share your code with third parties.
4. Your rights
- Access — Settings → Backup & Restore → Export
- Deletion — Settings → Danger Zone
- Data protection enquiries —
woohyunchoi@provelabs.co.kr
404
Page not found
This page doesn't exist, or was moved. Check your URL or use the navigation.
Activity Log
Recent actions you've taken in this browser — handy for retracing your own steps.
Stored locally in this browser only. It is not tamper-evident and is not an
audit trail — clearing site data or switching browsers loses it, and it is
not suitable as evidence for compliance.
Welcome back
Your security analysis workspace.
Total scans
0
Start scanning to see data
Findings
0
Across all scans
Open vulnerabilities
0
Needs attention
Scans this hour
0
Free tier · 60 scans/min
Quick start
Analyze Python for 98 CWE classes with machine-checked Rocq proofs. Pick a workflow to begin.
SQL Injection
Sample with CWE-89 detection.
Pickle Deserialization
CWE-502 with Rocq proof.
Command Injection
Sample with CWE-78 detection.
CWE Catalog
Browse 98 supported classes.
Benchmarks
Prove vs Bandit / Semgrep / CodeQL.
Rocq Proofs
Machine-checked Qed proofs.
Recent activityView all →
No scans yet. Run your first scan →
Analytics
Scan trends, top CWEs, and verdict breakdown.
Scans
0
Vulns found
0
Certified safe
0
Rocq proven
Avg latency
0ms
Basic mode
Scans over timeLast 30 days
Top CWEs
Verdict breakdown
Security Scanner
Analyze Python code with AST-based taint tracking, Z3 symbolic execution, and Rocq proof verification.
mode: single
—flows
—defended
—exploit
—certified
Source
input.py
1
Auto-scan
Analysis
🔍
Ready to scan
Paste code or upload a file, then click Analyze — or press ⌘↵.
Benchmarks
Head-to-head performance against industry-standard SAST tools on OWASP, 222-file, and cross-validation benchmarks.
Precision
99.8%
OWASP: 1 FP · curated sets: 0 FP
OWASP F1
96.5%
+40.8pp vs Bandit · +56.1pp vs Semgrep
Validated Files
1,626
3 in-dist benchmarks + OOD
Avg. Scan
<10ms
AST mode
Competitive Comparison
F1 across three Python benchmarks (paper v41, Table 1)
| Tool | OWASP | 222-file | Ext-174 |
|---|
CWE Catalog
98 supported CWEs sourced from CVE databases, OWASP, and MITRE. Each entry includes detection patterns, taint specs, and Rocq proof links.
Loading…
📚
Select a CWE
Pick an entry from the list to view full detection pattern, sinks, sanitizers, and code examples.
Rocq Proof Library
Machine-checked safety proofs backing each defense kind. 125 Qed proofs · 0 admitted.
📜
Select a proof
Browse machine-checked Rocq proofs backing each defense kind.
Talk to us about a pilot
Prove is adopted through a conversation. Tell us what you are shipping and we will set up an evaluation on your codebase.
Free
No account, nothing to arrange.
- Single-file analysis, full verdict set
- Machine-checked certificates — not paywalled
- 98 CWE classes
- 60 scans/min
- AI autofix on a single file
- Audit report export
By arrangement
Pro
For teams pointing this at a real repository.
- Everything in Free
- Whole-repository scans over the project API
- New-vs-closed against your previous scan
- Scoped API tokens for CI
- Defects that persist across scans — status, assignee, comments, append-only history (API only; no web UI yet)
- Project-wide AI autofix
- On-premise install and support terms, by contract
Scan History
Previous analyses saved to your workspace. Click a row to view findings.
What's New
Product updates, new features, and improvements.
v1.22Invite-only accounts · metered autofix · calmer results2026-07-27
- 🔒 Sign-up closes automatically on a public instance — registration was open to anyone who knew the URL, so pointing a domain at this app would have made it a public service by accident.
PROVE_SIGNUPnow defaults to closed wheneverPROVE_PUBLICis set, tying the decision to the deployment rather than to someone remembering a second switch. Local development stays open;PROVE_SIGNUP=open|closedoverrides either way. The server refuses the request, not just the form — a newGET /auth/configlets the sign-in screen hide the sign-up affordances instead of offering a form the server was always going to reject - 🔑 Operator account management —
admin.py create-userandadmin.py reset-password. There is no mail delivery yet, so no self-service reset link exists; without an operator path, a customer who forgot their password was locked out permanently. A reset revokes every active session, because a reset usually means the old credential is no longer trusted - 🔓 GitHub and Google sign-in — implemented and dormant: every OAuth route answers 404 and the buttons stay hidden until
PROVE_GITHUB_CLIENT_ID/SECRETor the Google pair are set, so this ships safely before the provider apps are registered. Callback URLs are<base>/auth/oauth/{github,google}/callback. Configuring one provider enables that provider alone.
Two decisions worth recording. Linking by email requires the provider to say the address is verified — otherwise anyone able to set an email on a throwaway provider account could claim the matching local account; an unverified address is refused rather than linked. And OAuth is not a way around a closed sign-up: on an invite-only instance an existing user signs in normally, but an unknown person is refused, so the provider button cannot become a side door. State is a random value held in a short-lived HttpOnly cookie and compared with the value the provider echoes back, and the provider's own error text is never forwarded to the browser — it can carry the authorization code. Not yet exercised against a live provider; the token exchange and profile fetch were tested with stand-in credentials only - 📊 AI autofix is metered; analysis is not — an autofix holds a GPU for seconds, an analysis costs milliseconds. Metering the analysis would throttle the cheap thing that demonstrates the product while leaving the expensive thing uncapped, so only AI calls count against a monthly allowance (
PROVE_AI_FREE_MONTHLY, default 20; paid plans unlimited but still recorded). Counted per organisation, and per file for project-wide fixes. The counter is one conditionalUPDATE: read-then-write admitted 25 of 25 concurrent requests against a limit of 10 and left the count at 3 - 🔕 Results stopped shouting — a single safe finding rendered five stat tiles (four of them zero), six filter chips (four of them zero) and four pipeline cards before the finding itself. Empty tiles and chips are hidden, and the pipeline collapses to one line naming the stages and the outcome, expandable on click. The stages stay: they are what makes this a proof pipeline rather than a scanner
- ✂️ The landing page says one thing — the hero subtitle carried three claims, five figures and a three-way competitor comparison that the Head-to-head section already makes. It now states the one thing that distinguishes the product. The
60 scans/minbadge left the first screen; it is still on the contact and terms pages, where someone is actually asking - 📮 Contact no longer depends on a mail client — the only path to a paid plan ended in a
mailto:link, which does nothing on a machine with no desktop mail app registered: no error, no feedback, and the visitor concludes the button is broken. The address is now always visible and copyable, with the mail app offered as a convenience. A clipboard failure falls back to selecting the text - 🧹 Claims we could not keep — the security page advertised "bug bounties up to $5,000" for a programme that does not exist; it now states the disclosure window and that there is no paid bounty. Three
prove.devplaceholder addresses replaced with the real contact
v1.21Dead navigation repaired2026-07-27
- 🔗 Three nav targets went nowhere — the v1.19 surface reduction dropped the
status,integrationsandauditpages but left their links in the topbar, the footer, the ⌘K palette and the onboarding checklist.nav()resolvespage-*by id, so each was a link that led nowhere. Resolved one at a time rather than restoring all three by reflex - 🗑 System Status deleted, not restored — the page reported "All systems operational", 99.98% / 99.95% / 100% uptime, two dated incidents and a "Subscribe to updates: RSS · email · Slack webhook" line. There is no hosted service behind this UI to report on, and the 30-day sparklines were
Math.random()redrawn on every visit. Invented reliability figures are worse than no status page, so the link is gone instead - 🗑 Integrations deleted — same call as the v1.20 fake API key panel. None of the connectors existed: GitHub, GitLab and Slack "Connect" only raised a toast reading "OAuth flow would open in production", Jira and VS Code were permanently "Coming soon", and the Prove CLI card offered to copy
pip install prove-clifor a package that has never been published.connectIntegrationis deleted rather than left unreachable - 🐞 Onboarding could never reach 100% — "Connect an integration" was one of five checklist items, and it could only be completed from the deleted Integrations page. Every user has been stuck at 4/5 since v1.19; the item is now gone and the checklist completes and dismisses itself again
- 📋 Audit Log restored as Activity Log — this one had real data behind it: scans, ignored findings and workspace switches have been recorded to
localStorageall along, with no surviving page to read them. Restored, but not under the old name. Entries are browser-local, user-clearable and editable from devtools — that is a convenience history, not an audit trail, and the page now says so rather than offering itself for "compliance". Oldauditpermalinks redirect toactivity
v1.20Joern retired · honest Pro2026-07-27
- 🗑 Joern CPG retired — measured, not guessed. On the 222-file benchmark in
data/ablation_222.json,ast_taintallandast_joern_taintallreturn identical results (F1 0.912, TP 88, FN 17) — but 4 s versus 3,179 s, a 795x cost for zero extra detections (0.02 s → 14.3 s per file). The cause is structural: since the v1.18.2 AST-authoritative rule, a Joern flow is dropped whenever the AST pass examined that sink and chose not to flag it, which is most of what Joern had to offer on single-file input. The code path is intact and comes back withPROVE_ENABLE_JOERN=1, for a codebase where genuine cross-file tracking proves its worth — the ablation used single-file cases and cannot speak to that - ⚖️
proon/api/analyzeis deprecated and ignored — Joern was the only thing it changed, so single-file analysis is now the same work and the same findings on every plan. The field is still accepted so existing clients keep working, and a request that sends it gets anoticein the response saying it did nothing.modeis now always"standard"instead of"basic"/"pro". The scanner's Pro toggle is gone rather than left as decoration - 🔒 Pro is now gated where it is actually sold —
/api/v1(projects, whole-repository scans, persistent defects) checks the token's org plan, and/api/ai/autofix_projectchecksrequire_pro. Both were previously guarded only by a browser-side toast, which is not a guard. Nothing else changed about auth, rate limits, CORS or headers - 💬 Pricing replaced with a contact block — there is no self-serve signup and the plan is set by an operator (
admin.py set-plan), so a published $29/month tier described a purchase flow that does not exist. The pricing page is now a contact page (pricingstill routes there); the checkout modal,startCheckoutandcompleteCheckoutare deleted rather than left unreachable - 🧹 Pro copy now matches what Pro gates — removed the claims for cross-function analysis, ZIP upload (the file input never accepted archives), Rocq PDFs (report export is HTML, client-side, and free), Agent Mode as a paid feature (it was never gated), and unmetered scans. Pro is described as what it is: repository-scale scans, scoped API tokens, defects that persist across scans, project-wide autofix, on-prem and support terms. Single-file analysis including the machine-checked certificate stays free — that is the demonstration, not the upsell
- 🧹 Fake API key panel removed — Settings showed a hardcoded
prv_live_free_…string with working Reveal and Copy buttons and a Regenerate that only raised a toast. Copying it got you a 401. Replaced with how tokens are actually issued. The webhook field went too: its Save button had no handler and no receiver exists - 📦 Docker and requirements corrected — both claimed Joern was a separate JVM install needed for Pro mode. The image has never contained a JVM or the Joern CLI; it now says so, and
PROVE_ENABLE_JOERNis documented in.env.example. Enabling it without a working Joern logs one warning and falls back to AST instead of failing silently
v1.19Stability, layout, and a smaller surface2026-07-26
- 🗑 AI Security Assistant removed — the floating chat panel overlapped the help widget and was not earning its place. Gone with it: the
⌘Ishortcut, the tour step, the command-palette entry, the drawer's "Ask AI" button, the in-panel model switcher, slash commands, SSE streaming chat, and conversation export. 796 lines of markup, script, and CSS deleted (11,802 → 11,006). AI Autofix is a separate feature and is unaffected - 🐞 Critical:
/api/uploadreturned 500 for every file —upload_file()calledanalyze(req)while the handler signature requiredanalyze(req, request). File upload had been failing outright; now verified end-to-end - 🔒 Critical: concurrent scans could crash the server — Z3's native library is not thread-safe across simultaneous solver use, and parallel
/api/analyzerequests aborted the whole process (ast.cpp:383 UNEXPECTED CODE WAS REACHED, Z3 4.16.0). Analysis is now serialized behind a process-wide lock shared with/api/v1scan ingestion. 50 concurrent requests: 0 crashes, 0 wrong verdicts - 🧪 Verdict integrity under load —
FlowAnalyzerkeeps per-analysis state on the instance (_current_taint_dict,_const_map,_sanitized_vars), so the shared singleton could leak one file's taint state into another's verdict. Each request now gets its own analyzer (~4 ms after warm-up) - 📐 Proportional shrink for narrow windows — below the 1100 px design width the whole interface now scales by a single ratio instead of squeezing fixed-column grids into overlap. Confined to ≥961 px so it never fights the responsive rules below it
- 📱 Layout no longer clips when narrow —
bodyhasoverflow-x:hidden, so anything that didn't fit was silently cut off rather than wrapping. Grid and flex children getmin-width:0; dashboard KPIs, OWASP coverage, policy stats, and charts reflow at 860 px and 620 px; wide tables and the activity heatmap scroll inside their own card. Verified clean at 8 widths from 1280 px down to 375 px across 7 pages - 🧹 Agent fix reported the wrong iteration count — the
finalSSE event always echoedmax_iterationsinstead of how many passes actually ran - 🧹
/api/catalog—has_detection_patternwas computed with abool(...).__and__(...)expression that calledget_detection_pattern()three times per CWE; now a single lookup (98 CWEs, 92 with patterns)
v1.18.2Engine — AST checks + AST/Joern reconciliation2026-04-29
- 🧠 AST-authoritative verdict (rule_ir_engine.py) — when AST examines a sink and decides not to flag it (constant-folded source, sanitizer wrap, etc.), Joern's CPG flow on the same sink is now suppressed. New
FlowAnalyzer._examined_sinksset tracks every sink AST processed - 🆕 5 new strict AST checks (ast_checks_registry.py +181):
check_xxe_safe_sax_parser— recognizesxml.sax.make_parser()as default-safe in modern Python; only flags when external entities are explicitly re-enabled viasetFeature(...feature_external_ges, True)check_dead_code_strict(CWE-561) — same-block code after unconditional exit, replaces fragile regexcheck_meta_char_to_sink(CWE-150) — metacharacter-to-sink AST detectioncheck_cookie_trust_decision(CWE-565) — cookie used in trust decision without validationcheck_route_no_auth_mutation(CWE-841) — route with state-mutating sink and no auth decorator / permission check
- 🛡 XSS format-dict sanitizer awareness —
check_xss_format_dictnow skips whenhtml.escape,markupsafe.escape,escape_for_html,escape_html, orcgi.escapeappears anywhere in scope - 🎯 CWE-200 tightened — sensitive-in-response regex now requires
return jsonify/Response/JSONResponse/HttpResponse/make_response/render_template/render(...)wrapper;context_presentgate added - 🧹 Removed 3 loose regex rules (
561_dead_code,565_cookie_no_validation,841_missing_workflow) replaced by the new strict AST helpers - 📐 XSS web-view gate bypassed in
taint_all_paramsmode (CVEfixes-style snippet benchmarks where parameters are the taint source) /api/healthreportsengine_build: 2026-04-29with full notes
v1.18Polish Pass + Engine Tuning2026-04-28
- 🧠 Engine precision tuning (rule_ir_engine.py) — four FP-reduction patches:
- FQN-strict sink lookup — removed short-name fallback.
os.popenno longer matches sinks ending inpopenfrom other CWEs (e.g.subprocess.Popen) - Import alias resolution — new
_build_import_map+_resolve_namewalkImport/ImportFromAST and canonicalize call names.from os import popen as p; p(cmd)now resolvesp→os.popenbefore catalog lookup - XSS web-view gating —
_check_xss_response_patternonly fires inside Flask/FastAPI/Bottle route decorators (@app.route,@router.get, etc). Helper functions returning tainted f-strings no longer flagged - Cleaner structural finding markers —
sink_callshows<structural:CWE-XXX>instead of multi-line regex match text; raw match preserved inwitness
- FQN-strict sink lookup — removed short-name fallback.
- Health endpoint now returns
engine_build+engine_notes; sidebar shows build date with hover tooltip listing improvements - 🐞 Critical: duplicate DOM IDs removed — old
signinOverlayandautofixOverlaywere defined twice;getElementByIdhit the older copies, so the v1.13 LLM diff modal and v1.16 sign-in modal never actually opened. Cleaned up legacyAUTOFIX_PATCHEStemplate system +mockSignIn+ duplicateopenSignIn - 👤 Dynamic user identity —
refreshUserUI()derives name/avatar/initials fromprove_auth.email; user chip, user menu header, and dashboard "Welcome back" all update on sign-in/sign-out - 📋 Landing depth — added 3-tier pricing block (Free $0 / Pro $29 / Enterprise) with feature lists + 6-question FAQ (
<details>) covering local-first, vs Bandit/Semgrep, Agent behavior, supported CWEs, CI/CD, languages - 🦴 Loading skeletons — pulse-animated skeletons replace "Loading…" text on catalog (6 rows), proofs (4 rows), benchmarks (3 cards). Reduces apparent wait time
- 📱 Mobile responsive — sidebar now slides in with translateX + backdrop overlay (click outside closes); tablet breakpoint 961-1180px shrinks sidebar to 200px; modals get 10px margin and viewport-fit on small screens;
toggleMobileNav(force)syncs aria-expanded - ♿ Accessibility — all 13
.modal-closebuttons getaria-label="Close dialog" - 🔗 Footer social links — github / twitter / linkedin now have real
href+rel="noopener"+ cursor pointer - 📊 Dashboard analytics hierarchy — sub-section divider style (h2 + bottom border) instead of a duplicate page-head with same h1 visual weight; Export CSV trimmed to icon + "CSV"
v1.17Agent Mode2026-04-25
- 🤖 Agent Mode — autonomous loop that scans, patches, re-scans, escalates models, and retries until the code is safe or max iterations hit
- New backend
POST /api/ai/agent/fix(SSE) — max 3 iterations, emitsstep/iteration_done/final/errorevents - 🎚 Auto-escalation — if weaker model produces identical code or can't close all VULNs, agent swaps to qwen3-coder:30b (or gemma4:31b) mid-run
- 🧠 Cross-engine verification — every iteration re-analyzes with the real Prove engine (not just LLM self-check), so false claims of "fixed" can't slip through
- Live SSE log — frontend reads stream via
fetch().body.getReader(), shows per-step status (running spinner / check / warn / error) + per-iteration summary cards - Final verdict banner — big colored banner (green: all resolved, yellow: partial, red: failed) + side-by-side before/after diff
- Apply & Re-scan — one-click overwrite of scanner code; uses existing patch-history snapshot system so Undo still works
- Agent button — cyan/purple gradient in findings toolbar; visible when ≥1 VULN
v1.16Landing + Project Autofix2026-04-25
- 🏠 Public landing + auth gate — logged-out visitors land on
#/landing; logged-in go to dashboard. Boot flow + popstate handler both respect auth state - 🎯 Public topbar — new
.public-topbarshown only whenbody.logged-out; brand, nav (Home/Features/Pricing/Docs/Changelog/Status), Sign in / Start free CTAs - 🔐 Sign-in modal — email+password form, GitHub/Google placeholder buttons;
doSignIn()setsprove_authlocalStorage and redirects to dashboard - 🚀 Start free —
signUpAndEnter()creates trial session and drops user into the scanner workspace - 👋 Sign out — user menu button now clears auth flag and returns to landing
- 🧹 Cleanup — dead "Free" workspace-switch chip removed from sidebar brand area
- 📦 Project Mode Autofix — new backend
POST /api/ai/autofix_projecttakes{files: [{path, code, findings}]}and iterates OpenCode calls per-file with CWE-specific prompts - Fix Project button — visible in project scanner toolbar when ≥1 vulnerable file; launches multi-file diff modal with expandable per-file panes
- Apply All & Re-scan — overwrites
projectFiles[path].content, re-renders tree, triggers full project scan
v1.15Streaming & Polish2026-04-25
- ⚡ SSE token streaming — new backend
POST /api/ai/chat_streamreturnstext/event-stream. Subscribes to OpenCode's global/eventSSE, filters by sessionID + assistant messageID (so user's echoed prompt doesn't leak), emitsdelta/replace/done/errorevents - 🔌 Frontend SSE consumer —
aiSendStreaming()usesfetch().body.getReader(), parses SSE frames, updates the last bot bubble in real time. Graceful fallback to non-streaming on error - 📋 / 🔄 / ✏️ Per-message actions — hover any message to reveal Copy / Regenerate / Edit&Resend buttons. Regenerate drops the bot reply and re-runs the preceding user question; Edit pulls user message back into the input
- ⬇ Export conversation — new download icon in AI panel header; Markdown (with role headers + divider) or JSON (structured, tooling-ready). Filename:
prove-chat-<timestamp>.{md,json} - 💬 Slash commands bypass streaming — keep deterministic behavior for
/help,/models, etc. - 🔁 Placeholder bubble — shows typing indicator until first delta arrives, then morphs into formatted reply
v1.14Autofix Complete2026-04-25
- ⚡ Batch autofix — "Fix All" button on findings toolbar (visible when ≥2 VULN). One LLM call returns unified diff covering all findings
- Backend
POST /api/ai/autofix_batchtakes{code, findings[]}, feeds CWE list + code → OpenCode, returns patched_code - 🔄 Iterative retry — after Apply, if VULN count doesn't drop, auto-reverts and retries once with a stronger model (qwen3-coder:30b / gemma4:31b)
- ↶ Patch history + undo — 10-deep localStorage stack; every Apply pushes a snapshot; Undo button in scanner toolbar restores the previous code
- 🎚 Model switcher — dropdown appears in AI panel header after first open;
/api/ai/modelslists configured models from OpenCode config; selection persists in localStorage - ⌘ Slash commands in AI chat —
/fix·/explain·/review·/audit·/models·/help. Parsed client-side, rewritten into structured prompts for OpenCode - 🛡 Snapshot-before-apply — every patch application first captures current code so Undo always works
- VULN delta detection via
_lastScan._tsto wait for NEXT scan before verifying
v1.13AI Autofix MVP2026-04-25
- 🛠 AI-generated patches — Finding Drawer "Generate Patch" button (gradient) wires to new
/api/ai/autofixbackend endpoint - Backend crafts a CWE-specific fix prompt, calls OpenCode (
gemma4:26bdefault), strips code fences, validates non-empty non-identical output - 📝 Side-by-side diff viewer — new modal with Original (red) / Patched (green) panes, LCS-style line diff, +/- counts
- ✅ Apply & Re-analyze flow — patch replaces scanner code, triggers highlight refresh, input event, re-runs analysis. Toast reports VULN delta. Zero VULNs → confetti
- 🔄 Regenerate button — appears when patch is empty/identical or after failure; kicks off a fresh LLM call
- 💬 Ask AI (drawer) — new button in Finding Drawer; auto-composes "Explain this finding…" and opens AI panel with the pre-filled question
- 🎯 CWE-specific system prompt — fix templates for CWE-89, 79, 78, 502, 22, 918, 327, 798, 611 (parameterized queries, escape_html, shlex, json, path guards, allowlists, sha256, env vars, defusedxml)
- 🛡 Unlimited on localhost —
/api/ai/autofixskips rate limits for 127.0.0.1 (same as/api/ai/chat)
v1.12Consolidation2026-04-25
- 📊 Scan Diff → Scan Compare (Matrix) — old 2-scan diff page removed; Matrix handles N=2 through N=5 natively
#/diffauto-redirects to#/matrix; sidebar item renamed "Scan Compare"- 📋 Legal consolidated — Privacy / Terms / Security merged into single
#/legalpage with tab switcher; old routes redirect + pre-select the right tab - 📈 Analytics absorbed by Dashboard — stats, line chart, top CWEs, verdict bars all render on Dashboard;
#/analyticsredirects - 👥 Team → Settings → Team tab — invite, member list, seat stats all live in Settings now
- 🧹 Sidebar decluttered — hidden: landing, pricing, workspaces, analytics, team, audit nav clutter. Available via ⌘K palette or contextual entry points (upgrade modal, footer, etc.)
- 🛡 Routing safety — new
PAGE_REDIRECTSmap in the router so permalinks/bookmarks to removed pages still work - 🗑 Dead code removed — renderDiffPage, computeDiff, duplicate legal markup, standalone page-analytics/page-team sections
v1.11Major2026-04-25
- 🤖 AI Security Assistant — floating chat panel with suggestion chips; answers pattern-matched questions about CWEs, verdicts, Rocq proofs, and your scan history
⌘Itoggles the panel · suggestion chips for common questions · typing indicator · recalls your last scan- 🎯 Interactive Product Tour — 5-step spotlight onboarding with animated clip-path backdrop
- Auto-starts once per new user (localStorage flag) · Settings → Replay tour · keyboard navigation
- 🛠 Custom Rule Builder — 4-step wizard (Identity → Pattern → Severity → Review) with live JSON preview
- Rules persist to localStorage · saved rules show in Settings → Custom Rules
- 📊 Multi-Scan Comparison Matrix — new `/matrix` page; select ≥2 scans → table of CWE × scan with V/S/– cells
- Highlights CWEs that appeared or disappeared across runs · Select all / Clear
- ⌨️ Keyboard Cheatsheet — visual 4-section grid (Navigation / Scanner / General / Editor); press
? - Replaces old plain-list shortcuts modal · groups shortcuts logically · styled key caps
- 🧩 Dashboard widget reorder — drag-and-drop Dashboard stat cards; order persists in localStorage
v1.10Organization2026-04-24
- 🔍 Global Search page — dedicated `/search` with 5 category chips (All/CWE/Scan/Proof/Page)
- Search highlights matched text with <mark> tags · groups results by type · clickable navigation
/keyboard shortcut jumps straight to search- 📂 Workspaces page — project switcher → real workspace grid with stats (scans/members/pinned)
- Create new workspace (Pro-gated) · switch active · visual card selection
- ⭐ Pinned items — sidebar section with quick access, pin button on CWE detail
- Pins persist across sessions · Clear all · max 8 shown in sidebar
- 🎯 OWASP Top 10 coverage heatmap — Dashboard widget with A01-A10 grid
- Cell color by finding count · red if vuln · clickable to filter Catalog
- 🔔 Actionable notifications — click notif → navigate to related scan/CWE
- Actionable notifs get accent left-border + hover highlight
v1.9Commercial2026-04-24
- 🏠 Landing page — marketing hero + 6-feature grid + competitive comparison + testimonial + CTA band
- 📜 Legal pages — Privacy Policy, Terms of Service, Security (with compliance badges)
- 📊 System Status — 4-engine health with 30-day sparklines + incidents
- 🍪 Cookie consent banner — GDPR-aware with Essential only / Got it
- 📋 Audit Log — tracks scan creates, finding ignores, settings changes (200 entries, localStorage)
- 🚫 Real 404 page — giant 404 gradient + back/dashboard/search actions
- 🔍 Enhanced ⌘K — now searches recent scans AND CWEs
- 🎨 SEO meta tags — og:title, og:image (SVG data URI), twitter:card, theme-color
- ⬇ Global footer — 5-column (Brand/Product/Company/Legal/Support) + social + compliance badges
- Sidebar audit log nav item added dynamically
v1.8Reliability2026-04-24
- 🛡 Error Boundary — global catch for runtime errors with friendly retry dialog (not white-screen)
- 📡 Offline Detection — top-bar banner when engine disconnects + 30s auto-retry loop
- Sidebar connection indicator (green/red dot)
- 📱 PWA Install — beforeinstallprompt + 30s engaged prompt + dismiss
- ☑ Bulk finding actions — checkbox per finding, sticky bottom bar with Ignore/Copy CSV
- 📦 Backup & Restore — Export all localStorage as JSON, Import to restore (12 data keys)
- ♿ A11y live region — screen readers hear all toasts and page navigations
- ↩️ Undo/Redo (⌘Z) in editor syncs overlay, line numbers, statusbar
- 🎨 System theme detection (prefers-color-scheme)
- 🔒 Unhandled rejection handler — no silent failures
v1.7Project+AI2026-04-24
- 📁 Project Mode — upload multiple Python files, VSCode-style file tree, scan all with one click, aggregated findings per file
- ✨ AI Auto-fix — one-click patch preview for CWE-22/78/79/89/94/327/502/798 with before/after diff viewer
- Apply fix directly to editor · copy fix code · rescan to verify
- 🛡 Verified Security Badge — SVG generator with 3 styles (Default/Flat/Dark)
- Markdown / HTML / URL embed tabs · standalone SVG download
- Badge unlocks on clean scan (0 vulnerabilities)
- 🎉 Confetti animation on A-grade security score
- Compact density mode — toggle in Settings → Appearance (25% tighter spacing)
- Scanner mode switcher (Single file ↔ Project) with Pro badge on Project
- Comfortable / Compact density cards in Appearance settings
v1.6Scanner2026-04-23
- Security Score — A/B/C/D/F grade with circular gauge + context-aware description
- Inline verdict-colored line highlights (red/yellow/green) in editor
- Red squiggly underlines on vulnerable lines (VSCode-style)
- Numbered gutter badges (1, 2, 3 ...) clickable to open finding drawer
- Minimap on right side of editor with vulnerability markers
- Auto-scan toggle — analyzes code 1.5s after you stop typing
- Findings toolbar: verdict filter chips (All / Vuln / Review / Safe / Cert)
- Sort dropdown: by severity / line / verdict / CWE
- Group by CWE toggle (collapsible groups with counts)
- Jump to line button on each finding
- n / N keyboard shortcuts to cycle findings
- Editor statusbar: cursor Ln/Col, current function, char/line count, save state
- Auto-save draft to localStorage — restored on page reload
- "Why this matters" plain-English explanations in drawer (10 CWEs)
- Share scan — copy state-encoded URL
- Scan report shortcut from score card
v1.5New2026-04-23
- Analytics page with 7/30/90/365-day range selector, line chart, top CWEs, verdict breakdown
- URL hash routing — every page now has shareable deep links (#/scanner, #/catalog)
- Drag & drop anywhere on window to load a .py file into Scanner
- CSV export for all findings (for spreadsheet analysis)
- Ignore finding with reason + expiry (false positive, won't fix, in progress, etc.)
- CWE favorites — ★ button, dedicated filter chip
- OWASP Top-10 category filter in Catalog
- Editor: Tab indent (4 spaces), multi-line selection indent, syntax scroll sync
- Right-click context menu on findings (view / copy CWE / ignore)
- Top progress bar animates on every API call
- Mobile hamburger menu for small screens
- Settings persistence (highlight, markers, taint) across sessions
- Breadcrumb now clickable
- 404 fallback when navigating to unknown page
v1.4New2026-04-23
- Activity heatmap on Dashboard showing scan history over the last year
- Team page with member management and invite flow
- PDF report export for audit trails
- Floating help widget with contextual FAQs
- j/k keyboard navigation through findings
- CWE relationship hints in catalog
v1.3New2026-04-23
- Python syntax highlighting in code editor
- Inline severity markers on vulnerable lines
- Scan Diff viewer (compare any two scans)
- CWE Rules management in Settings (enable/disable per-CWE)
- Theme system: Dark / Midnight / High Contrast
- Project switcher in sidebar (Pro gate)
v1.2Improved2026-04-23
- Command palette (⌘K) with fuzzy search across CWEs and commands
- Finding detail drawer with fix suggestions for 6 CWE classes
- Onboarding checklist on Dashboard
- History filters (vulnerable/certified/clean) + export all
- Quality gate indicator (pass/fail)
- Trend sparkline + severity distribution donut
v1.1Engine2026-04-22
- OWASP FP=0 achieved across 1,230 benchmark files (96.3% F1)
- 222-file benchmark: 100% F1, 0 FP
- CWE-754 (Improper Exception Check) detection added
- List-position taint model for OWASP list-pop patterns
- Catalog v2.1 accessors wired into analysis pipeline
v1.0Launch2026-04-20
- 98 CWE supported with Rule IR engine
- 125 Rocq proofs (0 admitted)
- AST + Z3 + Rocq 4-step pipeline
- Initial benchmarks vs Bandit/Semgrep
Settings
Manage your profile, API access, and notification preferences.
Profile
API Keys
Notifications
Analyzer
CWE Rules
Appearance
Backup & Restore
Danger Zone
Profile
Your account information.
API tokens
The /api/v1 endpoints — projects, whole-repository scans, persistent defects — authenticate with an X-Api-Key token scoped to scan, triage or admin. They are available to organisations on the Pro plan.
There is no self-service token management yet: we issue tokens for you when your organisation is set up. Email woohyunchoi@provelabs.co.kr to have one issued or revoked.
Email notifications
Choose which events trigger an email.
Critical vulnerability detected
Immediate email when CWE-89/78/502 fires
Weekly scan summary
Every Monday morning
Product updates
New features, blog posts
Analyzer defaults
Configure how scans run by default.
Taint all parameters
Treat all function params as tainted (good for snippets)
Show NEEDS_REVIEW verdicts
When Z3 can't decide, mark as review
CWE Rules
Toggle which CWE classes are enforced on your scans. Disabled rules won't produce findings.
Theme
Choose how Prove looks in your browser.
Light
White background (default)
Dark
Low-light friendly
Midnight
Deep blue accent
High Contrast
Accessibility optimized
Editor preferences
Syntax highlighting
Color Python tokens in editor and findings
Inline severity markers
Red dots on vulnerable lines in gutter
Backup & Restore
Export all your local data (history, settings, team, favorites, notifications) as a single JSON file.
Useful for moving to a new device, backup before updates, or sharing team settings.
Delete all scan history
Permanently remove all stored scans. This cannot be undone.
Delete account
Permanently remove your account and all data.
API Docs
REST API for integrating Prove into CI/CD, editors, and custom tooling. All endpoints return JSON.
Quick Start — cURL
curl -X POST http://localhost:1677/api/analyze \
-H "Content-Type: application/json" \
-d '{
"code": "from flask import request\nimport pickle\ndef f():\n return pickle.loads(request.data)"
}'
Python Client
import requests
# The "pro" field is deprecated. It is still accepted, but it is ignored and
# the response carries a "notice" saying so — single-file analysis is the
# same work and the same findings on every plan.
r = requests.post("http://localhost:1677/api/analyze", json={
"code": open("app.py").read(),
})
for f in r.json()["findings"]:
print(f"{f['cwe_id']} ({f['verdict']}) at line {f['sink_line']}")
Endpoints
POST
/api/analyze — submit code for analysis
POST/api/upload — multipart file upload
GET/api/catalog — list all 98 CWEs
GET/api/catalog/{cwe_id} — full CWE details
GET/api/benchmarks — benchmark stats
GET/api/proofs — Rocq proof library
GET/api/proofs/{name} — proof source
GET/api/health — health check
Repository-scale endpoints live under /api/v1 — projects, whole-repo scans, and persistent defects. They need an X-Api-Key token issued to a Pro org; full schema at /docs.