| <!DOCTYPE html> |
| <html lang="en"> |
| <head> |
| <meta charset="utf-8"> |
| <meta name="viewport" content="width=device-width, initial-scale=1"> |
| <title>AProver workbench</title> |
| <link rel="icon" href="/assets/logo-icon.svg"> |
| <link rel="preconnect" href="https://rsms.me/" /> |
| <link rel="stylesheet" href="https://rsms.me/inter/inter.css" /> |
| <link rel="preconnect" href="https://fonts.googleapis.com" /> |
| <link rel="preconnect" href="https://fonts.gstatic.com" crossorigin /> |
| <link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=JetBrains+Mono:wght@400;500;600;700&display=swap" /> |
| |
| <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/styles/github.min.css" /> |
| <script defer src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/highlight.min.js"></script> |
| <script defer src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/languages/c.min.js"></script> |
| <script defer src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/languages/rust.min.js"></script> |
| <script defer src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/languages/java.min.js"></script> |
| <link rel="stylesheet" href="/static/workbench.css" /> |
| </head> |
| <body> |
|
|
| <div class="stage"> |
| |
| <div class="screen" id="screen-connect"> |
| <div class="scr-head"> |
| <div class="brand"> |
| <a href="/" title="Home" style="display:flex;align-items:center;"><img src="/assets/logo.svg" alt="AProver" /></a> |
| <span class="vrule"></span> |
| <span class="pill"><span class="dot"></span><span id="connect-status">new run · not started</span></span> |
| </div> |
| <div class="right"> |
| <span class="modeltag" data-modeltag>anthropic · claude-sonnet-4-6</span> |
| <button class="iconbtn" data-open-settings title="Settings — keys & model">⚙</button> |
| </div> |
| </div> |
| <div class="connect-body"> |
| <div class="connect-card"> |
| <div class="section-label"><span class="num">1</span><span class="txt">source</span></div> |
| <div class="segment" id="source-seg"> |
| <button class="seg on" data-src="github">GitHub</button> |
| <button class="seg" data-src="git">Git URL</button> |
| <button class="seg" data-src="local">Local path</button> |
| </div> |
| |
| <div id="remote-block"> |
| <div class="fld-label" id="repo-fld-label">repository</div> |
| <div class="input focusy" id="repo-input-wrap"> |
| <span class="prefix" id="repo-prefix">github.com/</span> |
| <input id="repo-input" placeholder="owner/repo" autocomplete="off" spellcheck="false" /> |
| </div> |
| <div class="row" style="margin:14px 0 6px;"> |
| <span class="fld-label" style="margin:0;">ref</span> |
| <span class="hint">optional · branch, tag, or commit — defaults to HEAD</span> |
| </div> |
| <div class="row"> |
| <div class="input" style="flex:1;"> |
| <input id="ref-input" placeholder="HEAD" autocomplete="off" spellcheck="false" /> |
| </div> |
| <button class="btn" id="clone-btn"><span class="gly">⤓</span> Clone</button> |
| </div> |
| </div> |
|
|
| |
| <div id="local-block" class="hidden"> |
| <div class="fld-label">folder</div> |
| <div class="row"> |
| <button class="btn ghost" id="pick-folder-btn"><span class="gly">📂</span> Choose folder…</button> |
| <span class="mono" id="local-folder-name" style="font:600 13px/1 var(--mono);color:var(--faint);">no folder selected</span> |
| </div> |
| <div class="hint" style="margin-top:10px;">Reads the directory listing locally — nothing leaves your machine until you pick a scope and run. Only the selected source files are then uploaded for verification. <b>Chromium browsers only.</b></div> |
| </div> |
|
|
| <div class="hint" id="connect-hint" style="margin-top:14px;">After cloning, you choose what to verify →</div> |
| </div> |
| </div> |
| </div> |
|
|
| |
| <div class="screen hidden" id="screen-scope"> |
| <div class="scr-head"> |
| <div class="brand"> |
| <a href="/" title="Home" style="display:flex;align-items:center;"><img src="/assets/logo.svg" alt="AProver" /></a> |
| <span class="vrule"></span> |
| <span class="pill"><span class="dot"></span>new run · not started</span> |
| </div> |
| <div class="right"> |
| <span class="modeltag" data-modeltag>anthropic · claude-sonnet-4-6</span> |
| <button class="iconbtn" data-open-settings title="Settings">⚙</button> |
| </div> |
| </div> |
| <div class="repo-banner"> |
| <span class="chk">✓</span> |
| <span class="mono" id="scope-repo" style="font-weight:600;">—</span> |
| <span class="tag" id="scope-ref">ref HEAD</span> |
| <span class="hint" id="scope-cloned">cloned</span> |
| <span style="flex:1;"></span> |
| <button class="btn ghost sm" id="change-source">change source</button> |
| </div> |
| <div class="scope-pick"> |
| <div class="row" style="justify-content:space-between;margin-bottom:13px;"> |
| <div class="section-label" style="margin:0;"><span class="num">2</span><span class="txt">scope</span></div> |
| <span class="hint">what should this run verify?</span> |
| </div> |
| <div class="scope-cards" id="scope-cards"> |
| <div class="scope-card on" data-mode="whole"> |
| <div class="top"><span class="radio"></span><span class="lbl">Whole project</span></div> |
| <div class="sub">every code file in the repo</div> |
| </div> |
| <div class="scope-card" data-mode="subdir"> |
| <div class="top"><span class="radio"></span><span class="lbl">Subdirectory</span></div> |
| <div class="sub">pick a folder in the tree below</div> |
| </div> |
| <div class="scope-card" data-mode="file"> |
| <div class="top"><span class="radio"></span><span class="lbl">Single file</span></div> |
| <div class="sub">pick a file in the tree below</div> |
| </div> |
| </div> |
| </div> |
| <div class="scope-scroll"> |
| <div class="tree-head"> |
| <span class="t">project tree</span> |
| <span class="h" id="tree-hint">whole project selected</span> |
| </div> |
| <div class="tree" id="tree"></div> |
| |
| |
| |
| <div class="fnpick hidden" id="fnpick"> |
| <div class="tree-head"> |
| <span class="t">functions</span> |
| <span style="flex:1;"></span> |
| <button class="fnpick-toggle" id="fnpick-toggle" type="button">deselect all</button> |
| <span class="h" id="fnpick-hint">all selected</span> |
| </div> |
| <input id="fnpick-search" class="fnpick-search hidden" type="text" |
| placeholder="filter functions…" autocomplete="off" spellcheck="false" /> |
| <div class="fnpick-list" id="fnpick-list"></div> |
| </div> |
| |
| <div class="domain"> |
| <div class="tree-head"> |
| <span class="t">domain knowledge</span> |
| <span class="h">optional — guides spec generation</span> |
| </div> |
| <textarea id="domain-input" class="domain-input" rows="3" |
| placeholder="Context for spec generation — e.g. invariants the caller guarantees, units, or which inputs are attacker-controlled."></textarea> |
| </div> |
| |
| |
| |
| <div class="runset" id="runset"> |
| <button class="runset-head" id="runset-toggle" type="button"> |
| <span class="rs-chev">▸</span> |
| <span class="rs-title">Run settings</span> |
| <span class="rs-count" id="runset-count"></span> |
| <span style="flex:1;"></span> |
| <span class="rs-reset hidden" id="runset-reset" title="Reset all to defaults">reset</span> |
| </button> |
| <div class="runset-body hidden" id="runset-body"></div> |
| </div> |
| </div> |
| <div class="scope-foot"> |
| <div class="info"> |
| <div class="a">Run scope · <b id="scope-label">Whole project</b> — <span id="scope-detail">—</span></div> |
| <div class="b" id="scope-est">est. — · budget <span id="scope-budget">unlimited</span></div> |
| </div> |
| <button class="btn" id="run-btn"><span class="gly">▶</span> Run verification</button> |
| </div> |
| </div> |
|
|
| |
| <div class="screen hidden" id="screen-run"> |
| <div class="scr-head"> |
| <div class="brand"> |
| <a href="/" title="Home" style="display:flex;align-items:center;"><img src="/assets/logo.svg" alt="AProver" /></a> |
| <span class="vrule"></span> |
| <span class="pill live" id="run-pill"><span class="dot"></span><span id="run-status">verifying</span></span> |
| </div> |
| <div class="right"> |
| <span class="rel" id="rel-badge" title="API reliability — no calls yet"><span class="reldot"></span><span class="lbl">API</span> <span id="rel-pct">—</span> <span class="lbl" id="rel-lat"></span></span> |
| <span class="spend" id="spend"><span class="lbl">spent</span> <span id="spend-usd">$0.00</span> · <span id="spend-tok" class="lbl">0 tok</span></span> |
| <button class="minibtn" id="pause-btn">❚❚ pause</button> |
| <button class="minibtn" id="cancel-btn">⨯ stop</button> |
| </div> |
| </div> |
|
|
| <div class="recovery-banner hidden" id="recovery-banner"> |
| <span class="ic">!</span> |
| <div class="msg"> |
| <div class="a" id="recovery-title">Run halted.</div> |
| <div class="b" id="recovery-sub">Completed work is preserved — recovery won't re-spend on it.</div> |
| </div> |
| <div class="acts" id="recovery-acts"></div> |
| </div> |
|
|
| <div class="run-grid"> |
| |
| <div class="col"> |
| <div class="col-head"> |
| <div class="row" style="gap:8px;min-width:0;"> |
| <button class="minibtn" id="src-browse-btn" title="Browse in-scope files">📁 files</button> |
| <span class="mono" id="src-name" style="font-weight:600;color:var(--ink);font-size:12px;overflow:hidden;text-overflow:ellipsis;white-space:nowrap;">—</span> |
| <span class="tag" id="src-lang">C</span> |
| </div> |
| <span class="h mono" id="src-meta" style="color:var(--fainter);font-size:10px;"></span> |
| </div> |
| <div class="run-tree hidden" id="run-tree"></div> |
| <div class="src" id="src"></div> |
| </div> |
| |
| <div class="col mid"> |
| <div class="col-head"><span class="t">pipeline</span><span class="eta" id="eta-wrap"><span class="u">eta</span> <span id="eta">—</span></span><span class="elapsed"><span class="u">elapsed</span> <span id="elapsed">0s</span></span></div> |
| <div class="ftree" id="pipeline"></div> |
| <div class="cache-strip"><span class="g">⤓</span><span class="t" id="cache-strip">specs + harnesses cache to disk · safe to pause or close</span></div> |
| <div class="activity hidden" id="activity"><span class="dot"></span><span class="t" id="activity-text">starting…</span><span class="sweep"></span></div> |
| <details class="logwrap"><summary>run log</summary><div class="logbox" id="logbox"></div></details> |
| </div> |
| |
| <div class="col"> |
| <div class="col-head"><span class="t" id="findings-title">findings</span><span id="findings-count" class="tag">0 confirmed</span> |
| <div class="export-wrap" id="export-wrap" hidden> |
| <button class="btn ghost sm" id="export-btn" type="button">⤓ export</button> |
| <div class="export-menu hidden" id="export-menu"> |
| <button type="button" data-export="pdf">PDF</button> |
| <button type="button" data-export="csv">CSV</button> |
| </div> |
| </div> |
| </div> |
| <div class="findings" id="findings"></div> |
| </div> |
| </div> |
| </div> |
| </div> |
|
|
| |
| <div class="overlay hidden" id="settings-overlay"> |
| <div class="scrim" data-close-settings></div> |
| <div class="modal"> |
| <div class="mhead"> |
| <div> |
| <div class="t" id="set-title">Settings</div> |
| <div class="s" id="set-subtitle">choose a provider · keys stay in your browser</div> |
| </div> |
| <button class="x" data-close-settings>✕</button> |
| </div> |
|
|
| |
| <div class="mbody" id="settings-chooser"></div> |
|
|
| |
| <div class="mbody hidden" id="settings-detail"> |
| <button class="backlink" id="set-back"><span class="mono">‹</span> All providers</button> |
| <div class="fld-label">api key <a id="set-keylink" href="#" target="_blank" rel="noopener" style="text-transform:none;color:var(--blue);text-decoration:none;float:right;">get a key ↗</a></div> |
| <input class="field mono" id="set-key" type="password" placeholder="sk-ant-…" autocomplete="off" /> |
| <div class="hint" style="margin:6px 0 16px;">stored in your browser (localStorage) · sent only with your own requests, never written to artifacts</div> |
| <div id="set-model-wrap"> |
| <div class="fld-label">model</div> |
| <select class="field mono" id="set-model-select"></select> |
| <input class="field mono hidden" id="set-model" placeholder="any model id this provider supports" autocomplete="off" style="margin-top:8px;" /> |
| <div class="hint" id="set-model-hint" style="margin:6px 0 16px;">presets include a cost estimate · pick Custom for any other model id (no estimate)</div> |
| </div> |
| <div id="set-baseurl-wrap"> |
| <div class="fld-label">base url</div> |
| <input class="field mono" id="set-baseurl" placeholder="https://openrouter.ai/api/v1" autocomplete="off" /> |
| <div class="hint" id="set-baseurl-hint" style="margin:6px 0 16px;">leave blank for the provider default</div> |
| </div> |
| <div id="set-k2backend-wrap" class="hidden"> |
| <div class="fld-label">inference backend</div> |
| <select class="field mono" id="set-k2-backend"> |
| <option value="auto">auto — fastest, with fallback</option> |
| <option value="cerebras">cerebras — fastest</option> |
| <option value="nvidia">nvidia</option> |
| </select> |
| <div class="hint" style="margin:6px 0 16px;">auto routes each call to the faster backend and falls back if one stalls</div> |
| </div> |
| <div class="fld-label">budget cap (usd)</div> |
| <input class="field mono" id="set-budget" placeholder="unlimited" autocomplete="off" inputmode="decimal" /> |
| <div class="hint" style="margin:6px 0 16px;">stops the run cleanly once estimated spend crosses the cap · blank = unlimited</div> |
| <div class="fld-label">max files (directory sweep)</div> |
| <input class="field mono" id="set-maxfiles" placeholder="server default" autocomplete="off" inputmode="numeric" /> |
| <div class="hint" style="margin:6px 0 0;">cap on files verified in a whole-project / folder run · blank = server default</div> |
| <div class="errline hidden" id="set-error"></div> |
| </div> |
|
|
| <div class="mfoot"> |
| <span class="note" id="set-note">keys stay in your browser, sent only with your requests</span> |
| <button class="btn ghost sm" data-close-settings>Close</button> |
| <button class="btn sm hidden" id="set-save">Save settings</button> |
| </div> |
| </div> |
| </div> |
|
|
| |
| <div class="overlay hidden" id="confirm-overlay"> |
| <div class="scrim" id="confirm-scrim"></div> |
| <div class="modal"> |
| <div class="mhead"> |
| <div> |
| <div class="t">Start verification?</div> |
| <div class="s" id="confirm-sub">review the estimate before spending</div> |
| </div> |
| <button class="x" id="confirm-x">✕</button> |
| </div> |
| <div class="mbody" id="confirm-body"></div> |
| <div class="mfoot"> |
| <span class="note" id="confirm-note">estimates are approximate · the budget cap stops the run mid-flight</span> |
| <button class="btn ghost sm" id="confirm-cancel">Cancel</button> |
| <button class="btn sm" id="confirm-go"><span class="gly">▶</span> Run verification</button> |
| </div> |
| </div> |
| </div> |
|
|
| <div class="toast hidden" id="toast"></div> |
|
|
| <script src="/static/workbench.js"></script> |
| </body> |
| </html> |
|
|
