/* Formal uses the existing paper, signal and failure inks in every theme. */
.formal-figure { padding:var(--s5); background:var(--paper-2); border:1px solid var(--rule-strong); border-radius:var(--r-ctl); }
.formal-figure .figure-title { font:650 var(--fs-lg)/1.3 var(--sans); color:var(--ink); }
.formal-strip { display:flex; overflow-x:auto; gap:0; padding:12px 0; list-style:none; }
.formal-frame { position:relative; flex:1 0 160px; max-width:220px; padding:12px 20px 12px 12px; border:1px solid var(--rule-strong); background:var(--card); }
.formal-frame + .formal-frame::before { content:'→'; position:absolute; left:-10px; top:48%; padding:0 3px; color:var(--ink); background:var(--paper-2); z-index:1; }
.formal-frame button { border:0; border-bottom:2px solid var(--rule-strong); color:var(--ink); background:transparent; font:600 var(--fs-base)/1.5 var(--sans); cursor:pointer; padding:4px; }
.formal-frame p,.formal-selection { font-size:var(--fs-sm); }
.formal-frame strong { font:600 var(--fs-sm)/1.5 var(--mono); }
.formal-input { border-left:3px solid var(--flow-call); padding-left:8px; }
.formal-frame.is-fail { border:2px solid var(--bad); background:var(--bad-soft); }
.formal-frame.is-assumed { border-style:dashed; }
.formal-check { color:var(--good); font-weight:650; }
.formal-frame.is-fail .formal-check { color:var(--bad); }
.formal-frame.is-unchecked .formal-check,.formal-frame.is-assumed .formal-check { color:var(--ink-2); }
.formal-frame:has([aria-pressed="true"]) { outline:3px solid var(--focus); outline-offset:-4px; }
.formal-map-scroll { overflow:auto; }
.formal-map-scroll svg { width:100%; min-width:560px; display:block; font:14px var(--sans); color:var(--ink); }
.formal-map-scroll text { fill:var(--ink); }
.formal-reachable-set { fill:var(--card); stroke:var(--flow-data); stroke-width:2; }
.formal-edge { fill:none; stroke:var(--flow-call); stroke-width:2; }
.formal-arrow { fill:var(--flow-call); }.formal-arrow.is-induction { fill:var(--bad); }
.formal-edge.is-induction { stroke-dasharray:6 5; stroke:var(--bad); }
.formal-state circle { fill:var(--paper); stroke:var(--flow-data); stroke-width:2; }
.formal-state.is-bad circle { fill:var(--bad-soft); stroke:var(--bad); stroke-width:3; }
.formal-state.is-unreachable circle { stroke:var(--ink); stroke-dasharray:4 3; }
.formal-depth { height:30px; position:relative; background:var(--card); border:1px solid var(--rule-strong); margin:30px 0 20px; }
.formal-depth-fill { height:100%; background:var(--good); }
.formal-depth-required { position:absolute; top:-10px; bottom:-10px; border-left:3px dashed var(--ink); }
.formal-depth-bug { position:absolute; top:-26px; color:var(--bad); transform:translateX(-50%); font:bold 28px/1 var(--mono); }
.formal-depth-key { display:flex; flex-wrap:wrap; gap:16px 32px; }.formal-depth-key dt { color:var(--ink-2); font-size:var(--fs-sm); }.formal-depth-key dd { margin:4px 0; color:var(--ink); font-weight:650; }
.formal-workbench { container-type:inline-size; container-name:formal-lab; padding:var(--s5); border:1px solid var(--rule-strong); border-radius:var(--r-case); background:var(--case); color:var(--case-ink); }
.formal-controls { display:flex; flex-wrap:wrap; align-items:end; gap:12px; margin:0 0 18px; }
.formal-controls label { display:grid; gap:4px; font-size:var(--fs-sm); }
.formal-controls input,.formal-controls select { min-height:42px; max-width:210px; border:1px solid var(--rule-strong); border-radius:var(--r-chip); padding:7px; color:var(--ink); background:var(--card); }
.formal-editors { display:grid; grid-template-columns:minmax(0,1.6fr) minmax(0,1fr); gap:16px; }.formal-editors>div { min-width:0; }
@container formal-lab (max-width:900px) { .formal-editors { grid-template-columns:minmax(0,1fr); } }
.formal-editors h3 { font:600 var(--fs-base)/1.5 var(--sans); margin:0 0 6px; }
.formal-editors .editor { background:var(--screen); color:var(--screen-ink); border-radius:var(--r-chip); }
.formal-editors textarea,.formal-editors pre { min-height:320px; max-height:480px; }
.formal-result { margin:18px 0 8px; padding:12px; background:var(--card); border-left:4px solid var(--rule-strong); font-weight:600; }
.formal-result[data-verdict="FAIL"] { border-color:var(--bad); }.formal-result[data-verdict="PASS"] { border-color:var(--good); }
.formal-log { background:var(--screen); color:var(--screen-ink); max-height:280px; overflow:auto; padding:16px; white-space:pre-wrap; font:13px/1.5 var(--mono); }
.formal-table { overflow:auto; }.formal-table table { font:13px/1.5 var(--mono); }.formal-table th,.formal-table td { padding:6px 10px; white-space:nowrap; }.formal-table .is-failure { background:var(--bad-soft); color:var(--bad); }
.formal-workbench button:focus-visible,.formal-figure button:focus-visible { outline:var(--focus-w) solid var(--focus); outline-offset:3px; }
[data-path="formal"],.track-formal { --track:var(--ch-sva); --channel:var(--ch-sva); }
@media(max-width:700px) { .formal-editors { grid-template-columns:1fr; }.formal-workbench,.formal-figure { padding:14px; }.formal-editors textarea,.formal-editors pre { min-height:240px; }.formal-controls>* { flex:1 1 100px; }.formal-controls input,.formal-controls select { width:100%; } }

.tr-free-input { fill:var(--wave-alt); }.tr-free-label { fill:var(--wave-muted); font:10px var(--mono); }

.formal-table .formal-free { background:var(--paper-2); color:var(--ink); }
.formal-diagnosis-card { margin:24px 0; padding:16px; border:1px solid var(--rule-strong); border-radius:var(--r-ctl); background:var(--paper-2); }
.formal-diagnosis-card pre { overflow:auto; max-height:440px; font:13px/1.6 var(--mono); }
.formal-record-summary { font:600 var(--fs-sm)/1.5 var(--mono); }
.formal-diagnosis { min-width:0; width:100%; padding:12px; border:1px solid var(--rule-strong); border-radius:var(--r-ctl); }
.formal-diagnosis legend { font-weight:650; }
.formal-diagnosis label { margin:8px 0; }
.formal-diagnosis select { width:100%; max-width:100%; }

/* Formal has two panes and no simulator divider/console rows. */
.formal-workspace { grid-template-columns:minmax(0,1fr) minmax(320px,1fr); gap:16px; }
.formal-workspace [hidden] { display:none; }
.formal-workspace > .formal-workbench { display:flex; flex-direction:column; gap:12px; overflow:auto; }
.formal-workspace .formal-workbench > * { flex-shrink:0; }
.formal-workspace .formal-workbench h2 { margin:0; }
.formal-workspace .controls { display:flex; flex-wrap:wrap; gap:8px; }
.formal-workspace #test-status { max-width:none; }
.formal-signoff { padding:16px; border:1px solid var(--rule-strong); border-radius:var(--r-ctl); }
.formal-signoff dt { margin-top:12px; font-weight:650; }
.formal-signoff dd { margin:4px 0 0; overflow-wrap:anywhere; }
.formal-workspace #formal-submission-editor { min-width:0; border-radius:var(--r-ctl); overflow:hidden; }
.formal-workspace .editor-area { min-height:320px; }
@media(max-width:760px) {
  .formal-workspace { grid-template-columns:minmax(0,1fr); }
  .formal-workspace .editor-area { min-height:260px; }
}