@import url('https://fonts.googleapis.com/css2?family=Inter:wght@300;400;500;600;700;800;900&family=JetBrains+Mono:wght@400;500;600;700&display=swap');

/* ═══════════════════════════════════════════════════════
   LLM for Formal Methods — "Mathematical Precision"
   Clean, geometric, proof-assistant inspired.
   ═══════════════════════════════════════════════════════ */

:root {
  --primary: #0d9488;
  --primary-soft: #14b8a6;
  --primary-deep: #0f766e;
  --primary-06: rgba(13,148,136,0.06);
  --primary-10: rgba(13,148,136,0.10);
  --primary-20: rgba(13,148,136,0.18);

  --gray-50: #f6f8f9;
  --gray-100: #eef1f3;
  --gray-200: #dfe4e8;
  --gray-300: #a6afb8;
  --gray-400: #78828d;
  --gray-500: #576069;
  --gray-700: #2b333b;
  --gray-900: #10161b;
  --white: #ffffff;

  --me: #e11d48;

  /* verification status */
  --proved: #15803d;
  --proved-bg: rgba(21,128,61,0.10);
  --failed: #dc2626;
  --failed-bg: rgba(220,38,38,0.10);
  --pending: #b45309;
  --pending-bg: rgba(180,83,9,0.10);

  /* code / proof panels — "gray code, green annotations" */
  --code-bg: #f4f7f8;
  --code-fg: #384049;
  --code-border: #e2e8ec;

  /* grid + geometry */
  --grid-line: rgba(13,148,136,0.09);
  --ring-line: rgba(13,148,136,0.14);

  /* syntax (restrained, IDE-like) */
  --syn-kw: #7c3aed;
  --syn-fn: #2563eb;
  --syn-str: #b45309;
  --syn-num: #be123c;
  --syn-cm: #94a3b8;
  --syn-type: #0e7490;
  --syn-op: #0d9488;
  --syn-acsl: #15803d;
}

[data-theme="dark"] {
  --primary: #5eead4;
  --primary-soft: #2dd4bf;
  --primary-deep: #99f6e4;
  --primary-06: rgba(94,234,212,0.06);
  --primary-10: rgba(94,234,212,0.10);
  --primary-20: rgba(94,234,212,0.18);

  --gray-50: #10151a;
  --gray-100: #161c22;
  --gray-200: #263038;
  --gray-300: #4c5964;
  --gray-400: #8794a0;
  --gray-500: #97a4b0;
  --gray-700: #cdd6de;
  --gray-900: #eef3f6;
  --white: #0a0e12;

  --me: #fb7185;

  --proved: #4ade80;
  --proved-bg: rgba(74,222,128,0.12);
  --failed: #f87171;
  --failed-bg: rgba(248,113,113,0.12);
  --pending: #fbbf24;
  --pending-bg: rgba(251,191,36,0.12);

  --code-bg: #0e141a;
  --code-fg: #c3ccd4;
  --code-border: #1f2a33;

  --grid-line: rgba(94,234,212,0.07);
  --ring-line: rgba(94,234,212,0.12);

  --syn-kw: #c4b5fd;
  --syn-fn: #7dd3fc;
  --syn-str: #fcd34d;
  --syn-num: #fda4af;
  --syn-cm: #64748b;
  --syn-type: #67e8f9;
  --syn-op: #5eead4;
  --syn-acsl: #4ade80;
}

* { margin: 0; padding: 0; box-sizing: border-box; }
html { scroll-behavior: smooth; }
body {
  font-family: 'Inter', -apple-system, sans-serif;
  color: var(--gray-700); background: var(--white);
  line-height: 1.6; -webkit-font-smoothing: antialiased;
}
a { color: var(--primary-deep); text-decoration: none; }
[data-theme="dark"] a { color: var(--primary); }
a:hover { text-decoration: underline; }

/* ═══════════ TOP NAV ═══════════ */
.topnav {
  position: fixed; top: 0; left: 0; right: 0; z-index: 50;
  display: flex; align-items: center; justify-content: space-between;
  padding: 0.6rem 2rem;
  background: rgba(255,255,255,0.82); backdrop-filter: blur(14px) saturate(1.4);
  border-bottom: 1px solid var(--gray-100);
  transition: background 0.3s, border-color 0.3s;
}
[data-theme="dark"] .topnav { background: rgba(10,14,18,0.82); }
.nav-back {
  font-size: 0.82rem; font-weight: 500; color: var(--gray-400);
  display: flex; align-items: center; gap: 0.4rem;
}
.nav-back:hover { color: var(--primary-deep); text-decoration: none; }
[data-theme="dark"] .nav-back:hover { color: var(--primary); }
.nav-title {
  font-size: 0.82rem; font-weight: 700; color: var(--gray-900);
  letter-spacing: -0.2px; display: flex; align-items: center; gap: 0.5rem;
}
.nav-title .nav-glyph { color: var(--primary); font-weight: 700; }
.nav-right { display: flex; align-items: center; gap: 1rem; }
.nav-links { display: flex; gap: 0.35rem; }
.nav-link {
  font-size: 0.72rem; font-weight: 500; color: var(--gray-400);
  padding: 0.3rem 0.7rem; border-radius: 6px;
  transition: color 0.15s, background 0.15s;
}
.nav-link:hover, .nav-link.active {
  color: var(--primary-deep); background: var(--primary-10); text-decoration: none;
}
[data-theme="dark"] .nav-link:hover, [data-theme="dark"] .nav-link.active { color: var(--primary); }
.theme-btn {
  font-size: 0.75rem; font-weight: 600; color: var(--primary-deep);
  background: var(--primary-10); border: 1.5px solid var(--primary-20);
  padding: 0.3rem 0.85rem; border-radius: 20px; cursor: pointer;
  transition: opacity 0.25s, transform 0.25s; font-family: inherit;
}
[data-theme="dark"] .theme-btn { color: var(--primary); }
.theme-btn:hover { opacity: 0.85; transform: translateY(-1px); }

/* ═══════════ HERO ═══════════ */
.hero {
  min-height: 78vh; display: flex; align-items: center; justify-content: center;
  position: relative; overflow: hidden; margin-top: 46px;
  background: var(--white);
}
.hero-geo { position: absolute; inset: 0; pointer-events: none; overflow: hidden; }
/* subtle line grid */
.hero-grid {
  position: absolute; inset: -2px;
  background-image:
    linear-gradient(var(--grid-line) 1px, transparent 1px),
    linear-gradient(90deg, var(--grid-line) 1px, transparent 1px);
  background-size: 44px 44px;
  -webkit-mask-image: radial-gradient(ellipse 75% 70% at 50% 42%, #000 30%, transparent 82%);
          mask-image: radial-gradient(ellipse 75% 70% at 50% 42%, #000 30%, transparent 82%);
}
.hero-rings { position: absolute; left: 50%; top: 42%; transform: translate(-50%,-50%); }
.hero-rings circle { fill: none; stroke: var(--ring-line); stroke-width: 1.2; transform-origin: center; }
.hero-ring-pulse { animation: ringPulse 7s ease-out infinite; }
@keyframes ringPulse {
  0%   { transform: scale(0.35); opacity: 0; }
  18%  { opacity: 0.9; }
  100% { transform: scale(1.25); opacity: 0; }
}
.hero-nodes { position: absolute; inset: 0; }
.hero-nodes .hn { fill: var(--primary); opacity: 0; animation: nodeGlow 6s ease-in-out infinite; }
.hero-nodes .he { stroke: var(--ring-line); stroke-width: 1; }
@keyframes nodeGlow { 0%,100% { opacity: 0.12; } 50% { opacity: 0.5; } }

.hero-inner { text-align: center; position: relative; z-index: 1; max-width: 720px; padding: 2rem; }
.hero-badge {
  display: inline-flex; align-items: center; gap: 0.5rem;
  font-family: 'JetBrains Mono', monospace;
  font-size: 0.68rem; font-weight: 600; text-transform: uppercase; letter-spacing: 2px;
  color: var(--primary-deep); padding: 0.4rem 1rem; border-radius: 6px;
  background: var(--primary-10); border: 1px solid var(--primary-20);
  margin-bottom: 1.5rem;
}
[data-theme="dark"] .hero-badge { color: var(--primary); }
.hero h1 {
  font-size: 3.1rem; font-weight: 800; letter-spacing: -1.6px;
  line-height: 1.08; color: var(--gray-900); margin-bottom: 1.1rem;
}
.hero h1 .hl { color: var(--primary-deep); position: relative; }
[data-theme="dark"] .hero h1 .hl { color: var(--primary); }
.hero h1 .hl::after {
  content: ''; position: absolute; left: 0; right: 0; bottom: 4px; height: 8px;
  background: var(--primary-10); z-index: -1; border-radius: 2px;
}
.hero-sub { font-size: 1.08rem; color: var(--gray-500); max-width: 560px; margin: 0 auto 2rem; }
.hero-formula {
  font-family: 'JetBrains Mono', monospace; font-size: 0.9rem;
  color: var(--gray-400); margin: 0 auto 2rem; letter-spacing: 0.3px;
}
.hero-formula .hf-op { color: var(--primary); font-weight: 600; }
.hero-stats { display: flex; gap: 2.75rem; justify-content: center; flex-wrap: wrap; }
.hero-stat-num {
  font-size: 2rem; font-weight: 700; color: var(--primary-deep);
  font-family: 'JetBrains Mono', monospace;
}
[data-theme="dark"] .hero-stat-num { color: var(--primary); }
.hero-stat-label {
  font-size: 0.7rem; color: var(--gray-400); text-transform: uppercase; letter-spacing: 0.6px;
}
.hero-scroll {
  position: absolute; bottom: 1.8rem; left: 50%; transform: translateX(-50%);
  font-size: 0.7rem; color: var(--gray-400); z-index: 1;
  display: flex; flex-direction: column; align-items: center; gap: 0.3rem;
  animation: scrollPulse 2.4s ease-in-out infinite;
}
@keyframes scrollPulse {
  0%,100% { opacity: 0.45; transform: translateX(-50%) translateY(0); }
  50% { opacity: 1; transform: translateX(-50%) translateY(5px); }
}

/* ═══════════ SHOWCASE SECTION ═══════════ */
.showcase {
  padding: 5.5rem 2rem; border-bottom: 1px solid var(--gray-100);
  position: relative; overflow: hidden;
}
.showcase.alt { background: var(--gray-50); }
.showcase.alt::before {
  content: ''; position: absolute; inset: 0; pointer-events: none;
  background-image:
    linear-gradient(var(--grid-line) 1px, transparent 1px),
    linear-gradient(90deg, var(--grid-line) 1px, transparent 1px);
  background-size: 44px 44px; opacity: 0.5;
  -webkit-mask-image: radial-gradient(ellipse 60% 60% at 80% 10%, #000, transparent 70%);
          mask-image: radial-gradient(ellipse 60% 60% at 80% 10%, #000, transparent 70%);
}
.showcase-inner { max-width: 980px; margin: 0 auto; position: relative; z-index: 1; }

.sc-eyebrow {
  font-family: 'JetBrains Mono', monospace;
  font-size: 0.64rem; font-weight: 600; letter-spacing: 2.5px;
  text-transform: uppercase; color: var(--primary);
  margin-bottom: 0.6rem; display: flex; align-items: center; gap: 0.5rem;
}
.sc-eyebrow::before { content: '⊢'; font-size: 0.85rem; }
.sc-venue {
  font-family: 'JetBrains Mono', monospace;
  font-size: 0.7rem; font-weight: 600; padding: 3px 10px;
  border-radius: 5px; background: var(--primary-10);
  color: var(--primary-deep); display: inline-block; margin-bottom: 0.75rem;
}
[data-theme="dark"] .sc-venue { color: var(--primary); }
.sc-title {
  font-size: 1.7rem; font-weight: 800; letter-spacing: -0.6px;
  color: var(--gray-900); line-height: 1.24; margin-bottom: 0.55rem;
}
.sc-authors { font-size: 0.82rem; color: var(--gray-500); margin-bottom: 0.3rem; }
.sc-authors .me { color: var(--me); font-weight: 600; }
.sc-desc { font-size: 0.9rem; color: var(--gray-500); line-height: 1.65; margin-bottom: 1.1rem; max-width: 640px; }
.sc-links { display: flex; gap: 6px; margin-bottom: 2.25rem; flex-wrap: wrap; }
.sc-link {
  font-size: 0.72rem; font-weight: 600; padding: 0.38rem 1rem;
  border-radius: 6px; border: 1.5px solid var(--gray-200);
  color: var(--primary-deep); background: var(--white); transition: border-color 0.2s, color 0.2s;
}
[data-theme="dark"] .sc-link { background: var(--gray-100); color: var(--primary); }
.sc-link:hover { border-color: var(--primary); text-decoration: none; }
.sc-impact {
  display: inline-flex; flex-wrap: wrap; gap: 0.5rem 1rem; margin-bottom: 2rem;
  font-family: 'JetBrains Mono', monospace; font-size: 0.72rem; color: var(--gray-500);
}
.sc-impact b { color: var(--primary-deep); font-weight: 700; }
[data-theme="dark"] .sc-impact b { color: var(--primary); }

/* ═══════════ shared: code / proof panels ═══════════ */
.proof-panel {
  background: var(--code-bg); border: 1px solid var(--code-border);
  border-radius: 12px; overflow: hidden;
}
.proof-panel-head {
  display: flex; align-items: center; gap: 8px;
  padding: 8px 14px; border-bottom: 1px solid var(--code-border);
  font-family: 'JetBrains Mono', monospace; font-size: 0.68rem; font-weight: 600;
  color: var(--gray-500); background: var(--gray-50);
}
[data-theme="dark"] .proof-panel-head { background: var(--gray-100); }
.proof-dot { width: 8px; height: 8px; border-radius: 50%; flex-shrink: 0; }
.proof-code {
  font-family: 'JetBrains Mono', monospace; font-size: 12px; line-height: 1.85;
  color: var(--code-fg); padding: 14px 16px; min-height: 250px;
  white-space: pre-wrap; word-break: break-word;
}
.proof-code .cursor {
  display: inline-block; width: 7px; height: 13px; background: var(--primary);
  animation: blink 0.85s step-end infinite; vertical-align: middle; margin-left: 1px;
}
@keyframes blink { 0%,100% { opacity: 1; } 50% { opacity: 0; } }

/* syntax */
.s-kw { color: var(--syn-kw); }
.s-fn { color: var(--syn-fn); }
.s-str { color: var(--syn-str); }
.s-num { color: var(--syn-num); }
.s-cm { color: var(--syn-cm); font-style: italic; }
.s-type { color: var(--syn-type); }
.s-op { color: var(--syn-op); }
.s-acsl { color: var(--syn-acsl); font-weight: 500; }

/* verification status pills */
.vstatus {
  display: inline-flex; align-items: center; gap: 5px;
  font-family: 'JetBrains Mono', monospace; font-size: 0.68rem; font-weight: 600;
  padding: 3px 9px; border-radius: 20px;
}
.vstatus .vsym { font-size: 0.78rem; line-height: 1; }
.vstatus.proved { color: var(--proved); background: var(--proved-bg); }
.vstatus.failed { color: var(--failed); background: var(--failed-bg); }
.vstatus.pending { color: var(--pending); background: var(--pending-bg); }
.vstatus.pending .vsym { animation: spin 1.1s linear infinite; display: inline-block; }
@keyframes spin { to { transform: rotate(360deg); } }

/* ═══════════ F1: NL → Formal pipeline ═══════════ */
.nl2f {
  display: grid; grid-template-columns: 1fr 74px 1fr; gap: 0; align-items: stretch;
}
.nl2f-panel { display: flex; flex-direction: column; }
.nl-text {
  font-size: 0.9rem; line-height: 1.7; color: var(--gray-700);
  padding: 16px 18px; min-height: 250px;
}
.nl-text .cursor {
  display: inline-block; width: 7px; height: 15px; background: var(--primary);
  animation: blink 0.85s step-end infinite; vertical-align: middle; margin-left: 1px;
}
.nl-text .nl-req { display: block; margin-bottom: 10px; }
.nl-text .nl-tag {
  font-family: 'JetBrains Mono', monospace; font-size: 0.62rem; font-weight: 600;
  color: var(--primary-deep); text-transform: uppercase; letter-spacing: 1px;
}
[data-theme="dark"] .nl-text .nl-tag { color: var(--primary); }
.nl2f-mid {
  display: flex; flex-direction: column; align-items: center; justify-content: center; gap: 8px;
}
.llm-core {
  width: 52px; height: 52px; border-radius: 14px; position: relative;
  background: var(--primary-10); border: 1.5px solid var(--primary-20);
  display: flex; align-items: center; justify-content: center;
  font-family: 'JetBrains Mono', monospace; font-size: 0.6rem; font-weight: 700;
  color: var(--primary-deep); transition: box-shadow 0.4s, border-color 0.4s;
}
[data-theme="dark"] .llm-core { color: var(--primary); }
.llm-core.active { box-shadow: 0 0 0 6px var(--primary-06), 0 0 22px var(--primary-20); border-color: var(--primary); }
.llm-core .llm-ring {
  position: absolute; inset: -8px; border-radius: 18px;
  border: 1.5px dashed var(--primary-20); opacity: 0;
}
.llm-core.active .llm-ring { opacity: 1; animation: spin 4.5s linear infinite; }
.nl2f-flow { width: 2px; flex: 1; background: var(--gray-200); position: relative; min-height: 30px; }
.nl2f-flow.h { width: 100%; height: 2px; }
.nl2f-flow .pkt {
  position: absolute; width: 7px; height: 7px; border-radius: 50%;
  background: var(--primary); left: -2.5px; top: 0; opacity: 0;
}
.nl2f-flow.active .pkt { animation: pktDown 1.1s ease-in-out infinite; }
@keyframes pktDown { 0% { top: 0; opacity: 0; } 20% { opacity: 1; } 80% { opacity: 1; } 100% { top: 100%; opacity: 0; } }
.nl2f-arrow-label {
  font-family: 'JetBrains Mono', monospace; font-size: 0.58rem; font-weight: 600;
  color: var(--gray-400); text-align: center; letter-spacing: 0.5px;
}

.lemma-status {
  margin-top: 14px; border-radius: 12px; border: 1px solid var(--code-border);
  background: var(--gray-50); padding: 12px 16px;
}
[data-theme="dark"] .lemma-status { background: var(--gray-100); }
.lemma-status-head {
  display: flex; align-items: center; justify-content: space-between;
  font-family: 'JetBrains Mono', monospace; font-size: 0.7rem; font-weight: 700;
  color: var(--gray-700); margin-bottom: 10px;
}
.lemma-row {
  display: flex; align-items: center; gap: 10px; padding: 5px 0;
  font-family: 'JetBrains Mono', monospace; font-size: 0.74rem; color: var(--gray-500);
  opacity: 0; transform: translateX(-6px); transition: opacity 0.4s, transform 0.4s;
}
.lemma-row.show { opacity: 1; transform: translateX(0); }
.lemma-row .lemma-name { flex: 1; }

/* ═══════════ F2: AutoSpec — C + ACSL ═══════════ */
.autospec-pipe {
  display: flex; align-items: center; justify-content: center; flex-wrap: wrap;
  gap: 8px; margin-bottom: 1.75rem;
}
.autospec-stage {
  font-family: 'JetBrains Mono', monospace; font-size: 0.68rem; font-weight: 600;
  padding: 6px 12px; border-radius: 8px; border: 1.5px solid var(--gray-200);
  color: var(--gray-500); background: var(--white); transition: all 0.4s; white-space: nowrap;
}
[data-theme="dark"] .autospec-stage { background: var(--gray-100); }
.autospec-stage.active { border-color: var(--primary); color: var(--primary-deep); background: var(--primary-10); }
[data-theme="dark"] .autospec-stage.active { color: var(--primary); }
.autospec-stage.done { border-color: var(--proved); color: var(--proved); background: var(--proved-bg); }
.autospec-sep { color: var(--gray-300); font-size: 0.8rem; }

.autospec-grid { display: grid; grid-template-columns: 1fr 1fr; gap: 1.25rem; align-items: start; }
.acsl-code { counter-reset: none; }
.acsl-line {
  display: block; opacity: 0; transform: translateY(4px);
  transition: opacity 0.4s ease, transform 0.4s ease, background 0.4s;
  border-radius: 4px; padding: 0 4px; margin: 0 -4px;
}
.acsl-line.show { opacity: 1; transform: translateY(0); }
.acsl-line.anno { color: var(--syn-acsl); }
.acsl-line.anno.glow { background: var(--proved-bg); box-shadow: inset 3px 0 0 var(--proved); }

.verify-badges { display: flex; flex-direction: column; gap: 8px; margin-top: 14px; }
.verify-badge {
  display: flex; align-items: center; gap: 10px; padding: 9px 13px;
  border-radius: 10px; border: 1px solid var(--code-border); background: var(--gray-50);
  font-family: 'JetBrains Mono', monospace; font-size: 0.74rem; color: var(--gray-700);
  opacity: 0; transform: translateX(14px); transition: opacity 0.45s, transform 0.45s;
}
[data-theme="dark"] .verify-badge { background: var(--gray-100); }
.verify-badge.show { opacity: 1; transform: translateX(0); }
.verify-badge .vb-fn { flex: 1; }

/* ═══════════ F3: ModelWisdom — TLA+ state machine ═══════════ */
.tla-wrap { display: grid; grid-template-columns: 1.4fr 1fr; gap: 1.5rem; align-items: center; }
@media (max-width: 820px) { .tla-wrap { grid-template-columns: 1fr; } }
.tla-stage {
  border-radius: 14px; border: 1px solid var(--code-border);
  background: var(--gray-50); padding: 10px;
}
[data-theme="dark"] .tla-stage { background: var(--gray-100); }
.tla-svg { width: 100%; height: auto; display: block; }
.tla-node circle {
  fill: var(--white); stroke: var(--gray-300); stroke-width: 2; transition: all 0.5s;
}
[data-theme="dark"] .tla-node circle { fill: var(--gray-200); }
.tla-node text { font-family: 'JetBrains Mono', monospace; font-size: 12px; font-weight: 600; fill: var(--gray-500); transition: fill 0.5s; }
.tla-node.active circle { fill: var(--primary); stroke: var(--primary); filter: drop-shadow(0 0 8px var(--primary-20)); }
.tla-node.active text { fill: var(--white); }
[data-theme="dark"] .tla-node.active text { fill: var(--white-0, #0a0e12); fill: #0a0e12; }
.tla-node.bug circle { fill: var(--failed); stroke: var(--failed); filter: drop-shadow(0 0 10px var(--failed-bg)); }
.tla-node.bug text { fill: #fff; }
.tla-node.fixed circle { fill: var(--proved); stroke: var(--proved); filter: drop-shadow(0 0 8px var(--proved-bg)); }
.tla-node.fixed text { fill: #fff; }
.tla-edge { stroke: var(--gray-300); stroke-width: 2; fill: none; transition: stroke 0.4s, stroke-width 0.4s, opacity 0.5s; }
.tla-edge.active { stroke: var(--primary); stroke-width: 3; }
.tla-edge.bug { stroke: var(--failed); stroke-width: 3; stroke-dasharray: 5 4; }
.tla-edge.removed { opacity: 0; }
.tla-edge.repair { stroke: var(--proved); stroke-width: 3; opacity: 0; }
.tla-edge.repair.show { opacity: 1; }

.tla-log { display: flex; flex-direction: column; gap: 8px; }
.tla-log-title {
  font-family: 'JetBrains Mono', monospace; font-size: 0.7rem; font-weight: 700;
  color: var(--gray-700); text-transform: uppercase; letter-spacing: 1px; margin-bottom: 2px;
}
.tla-log-item {
  display: flex; align-items: flex-start; gap: 9px; padding: 8px 12px;
  border-radius: 9px; border: 1px solid var(--code-border); background: var(--gray-50);
  font-size: 0.76rem; color: var(--gray-500);
  opacity: 0; transform: translateY(6px); transition: opacity 0.4s, transform 0.4s;
}
[data-theme="dark"] .tla-log-item { background: var(--gray-100); }
.tla-log-item.show { opacity: 1; transform: translateY(0); }
.tla-log-item .tli-glyph { font-family: 'JetBrains Mono', monospace; font-weight: 700; flex-shrink: 0; }
.tla-log-item.trace .tli-glyph { color: var(--primary-deep); }
[data-theme="dark"] .tla-log-item.trace .tli-glyph { color: var(--primary); }
.tla-log-item.bug .tli-glyph { color: var(--failed); }
.tla-log-item.fix .tli-glyph { color: var(--proved); }

/* ═══════════ F4: Can LLMs Model — flip cards + radar ═══════════ */
.model-layout { display: grid; grid-template-columns: 1.1fr 0.9fr; gap: 2rem; align-items: center; }
@media (max-width: 860px) { .model-layout { grid-template-columns: 1fr; } }
.flip-grid { display: grid; grid-template-columns: 1fr 1fr; gap: 14px; }
.flip-card { perspective: 1000px; height: 130px; }
.flip-inner {
  position: relative; width: 100%; height: 100%;
  transition: transform 0.7s cubic-bezier(0.22,1,0.36,1); transform-style: preserve-3d;
}
.flip-card.flipped .flip-inner { transform: rotateY(180deg); }
.flip-face {
  position: absolute; inset: 0; backface-visibility: hidden;
  border-radius: 12px; border: 1px solid var(--code-border);
  padding: 14px; display: flex; flex-direction: column; justify-content: center;
}
.flip-front { background: var(--gray-50); }
[data-theme="dark"] .flip-front { background: var(--gray-100); }
.flip-front .fc-glyph {
  font-family: 'JetBrains Mono', monospace; font-size: 1.3rem; color: var(--primary);
  margin-bottom: 8px;
}
.flip-front .fc-name { font-size: 0.82rem; font-weight: 700; color: var(--gray-900); line-height: 1.3; }
.flip-back {
  background: var(--primary-10); border-color: var(--primary-20);
  transform: rotateY(180deg); align-items: flex-start;
}
.flip-back .fc-score {
  font-family: 'JetBrains Mono', monospace; font-size: 1.5rem; font-weight: 700; color: var(--primary-deep);
}
[data-theme="dark"] .flip-back .fc-score { color: var(--primary); }
.flip-back .fc-metric { font-size: 0.66rem; color: var(--gray-500); text-transform: uppercase; letter-spacing: 0.5px; margin-bottom: 6px; }
.flip-back .fc-note { font-size: 0.72rem; color: var(--gray-500); line-height: 1.4; }

.radar-wrap {
  border-radius: 16px; border: 1px solid var(--code-border); background: var(--gray-50);
  padding: 16px; text-align: center;
}
[data-theme="dark"] .radar-wrap { background: var(--gray-100); }
.radar-title {
  font-family: 'JetBrains Mono', monospace; font-size: 0.68rem; font-weight: 600;
  color: var(--gray-500); text-transform: uppercase; letter-spacing: 1px; margin-bottom: 8px;
}
.radar-svg { width: 100%; height: auto; }
.radar-grid-poly { fill: none; stroke: var(--gray-200); stroke-width: 1; }
.radar-axis { stroke: var(--gray-200); stroke-width: 1; }
.radar-data {
  fill: var(--primary-20); stroke: var(--primary); stroke-width: 2; stroke-linejoin: round;
  transform: scale(0); transform-box: view-box; transform-origin: 130px 130px;
  transition: transform 1.1s cubic-bezier(0.22,1,0.36,1);
}
.radar-data.show { transform: scale(1); }
.radar-dot { fill: var(--primary); opacity: 0; transition: opacity 0.5s 0.6s; }
.radar-dot.show { opacity: 1; }
.radar-label { font-family: 'JetBrains Mono', monospace; font-size: 8.5px; fill: var(--gray-400); }

/* ═══════════ ALL PAPERS ═══════════ */
.papers-sec { padding: 4.5rem 2rem; background: var(--gray-50); }
.papers-inner { max-width: 980px; margin: 0 auto; }
.papers-sec-title {
  font-size: 1.15rem; font-weight: 700; color: var(--gray-900);
  margin-bottom: 1.25rem; display: flex; align-items: center; gap: 0.6rem;
}
.papers-sec-bar { width: 4px; height: 20px; border-radius: 2px; background: var(--primary); }
.mini-card {
  display: flex; gap: 12px; padding: 13px 15px;
  border-radius: 10px; background: var(--white);
  border: 1px solid var(--gray-100); margin-bottom: 7px;
  transition: border-color 0.2s, transform 0.2s;
}
[data-theme="dark"] .mini-card { background: var(--gray-100); border-color: var(--gray-200); }
.mini-card:hover { border-color: var(--primary-20); transform: translateX(3px); }
.mini-venue {
  font-family: 'JetBrains Mono', monospace;
  font-size: 0.62rem; font-weight: 600; color: var(--primary-deep);
  min-width: 62px; flex-shrink: 0; padding-top: 3px;
}
[data-theme="dark"] .mini-venue { color: var(--primary); }
.mini-title { font-size: 0.84rem; font-weight: 600; color: var(--gray-900); line-height: 1.4; }
.mini-authors { font-size: 0.72rem; color: var(--gray-500); margin-top: 1px; }
.mini-authors .me { color: var(--me); font-weight: 600; }
.mini-links { display: flex; gap: 5px; margin-top: 5px; flex-wrap: wrap; }
.mini-link {
  font-size: 0.62rem; color: var(--primary-deep); padding: 2px 8px;
  border-radius: 4px; background: var(--gray-50);
  border: 1px solid var(--gray-100); transition: border-color 0.15s;
}
[data-theme="dark"] .mini-link { background: var(--gray-200); color: var(--primary); }
.mini-link:hover { border-color: var(--primary); text-decoration: none; }

/* ═══════════ FOOTER ═══════════ */
.footer {
  padding: 1.75rem 2rem; border-top: 1px solid var(--gray-100);
  font-size: 0.75rem; color: var(--gray-400); text-align: center;
}
.footer .foot-glyph { color: var(--primary); }

/* ═══════════ GSAP targets ═══════════ */
.gsap-fade { opacity: 0; transform: translateY(22px); }

/* ═══════════ TAKEAWAY + COMPACT ANIMATIONS ═══════════ */
.sc-takeaway {
  margin-top: 1rem; padding: 0.8rem 1.2rem; border-radius: 10px;
  background: linear-gradient(135deg, var(--primary-10), var(--gray-50));
  border-left: 3px solid var(--primary-deep);
  font-size: 0.82rem; color: var(--gray-700); line-height: 1.5;
  display: flex; align-items: flex-start; gap: 0.6rem;
  transition: transform 0.2s, box-shadow 0.2s;
}
.sc-takeaway:hover { transform: translateX(4px); box-shadow: 0 2px 8px rgba(0,0,0,0.06); }
.takeaway-icon { font-size: 1.1rem; flex-shrink: 0; }
.compact-anim {
  margin-top: 1.4rem; padding: 1.2rem; border-radius: 12px;
  background: var(--panel, var(--gray-50)); border: 1px solid var(--gray-100);
  min-height: 80px; overflow: hidden;
}
.mini-pipe { display: flex; align-items: center; gap: 0.5rem; flex-wrap: wrap; margin-bottom: 1rem; }
.mini-pipe-stage {
  padding: 0.5rem 0.9rem; border-radius: 8px; font-size: 0.74rem; font-weight: 600;
  background: var(--gray-50); border: 1px solid var(--gray-100); color: var(--gray-400);
  opacity: 0; transition: all 0.4s; cursor: default;
}
.mini-pipe-stage.on { opacity: 1; background: var(--primary-10); border-color: var(--primary-20); color: var(--primary-deep); }
.mini-pipe-stage:hover { transform: scale(1.05); }
.mini-pipe-sep { color: var(--gray-300); font-weight: 700; opacity: 0; transition: opacity 0.3s; }
.mini-pipe-sep.on { opacity: 1; }
.mini-warning { margin-top: 0.8rem; font-size: 0.74rem; color: var(--warn, #d97706); font-weight: 600; opacity: 0; transition: opacity 0.5s; display: flex; align-items: center; gap: 0.4rem; }
.mini-warning.on { opacity: 1; }
.mini-result { margin-top: 0.6rem; font-size: 0.82rem; font-weight: 700; color: var(--proved); opacity: 0; transition: opacity 0.5s; }
.mini-result.on { opacity: 1; }

/* ═══════════ INTERACTIVITY ═══════════ */
.autospec-stage { transition: all 0.25s; cursor: default; }
.autospec-stage:hover { transform: translateY(-2px) scale(1.05); box-shadow: 0 4px 12px var(--primary-20); }
.autospec-stage:active { transform: scale(0.95); }
.autospec-stage.active { cursor: default; }

.tla-node circle { transition: all 0.3s; cursor: pointer; }
.tla-node:hover circle { filter: brightness(1.2); stroke-width: 3; }
.tla-node:hover text { font-weight: 700; }

.tla-log-item { transition: all 0.2s; cursor: default; border-radius: 6px; padding: 4px 8px; }
.tla-log-item:hover { background: var(--primary-10); transform: translateX(4px); }

.lemma-row { transition: all 0.2s; cursor: default; border-radius: 6px; }
.lemma-row:hover { background: var(--primary-10); transform: translateX(4px); }

.verify-badge { transition: all 0.25s; cursor: default; }
.verify-badge:hover { transform: translateY(-2px) scale(1.04); box-shadow: 0 4px 10px rgba(0,0,0,0.1); }
.verify-badge:active { transform: scale(0.96); }

.sc-link { transition: all 0.2s; }
.sc-link:hover { transform: translateY(-2px); box-shadow: 0 4px 10px var(--primary-20); text-decoration: none; }
.sc-link:active { transform: translateY(0) scale(0.95); }

.sc-impact span { transition: transform 0.2s; display: inline-block; cursor: default; }
.sc-impact span:hover { transform: scale(1.05); }

.llm-core { transition: transform 0.3s, box-shadow 0.3s; cursor: pointer; }
.llm-core:hover { transform: scale(1.1); box-shadow: 0 0 20px var(--primary-20); }

/* ═══════════ RESPONSIVE ═══════════ */
@media (max-width: 900px) {
  .hero h1 { font-size: 2.1rem; }
  .hero-sub { font-size: 0.94rem; }
  .hero-stats { gap: 1.6rem; }
  .hero-stat-num { font-size: 1.5rem; }
  .showcase { padding: 3.5rem 1.25rem; }
  .sc-title { font-size: 1.3rem; }
  .nl2f { grid-template-columns: 1fr; }
  .nl2f-mid { flex-direction: row; padding: 14px 0; }
  .nl2f-flow { width: 100%; height: 2px; flex: 1; min-height: 0; }
  .nl2f-flow.h { width: 2px; }
  .autospec-grid { grid-template-columns: 1fr; }
  .nav-links { display: none; }
}
@media (max-width: 480px) {
  .hero h1 { font-size: 1.7rem; }
  .hero { min-height: 68vh; }
  .proof-code { font-size: 10.5px; padding: 12px; min-height: 180px; }
  .flip-grid { grid-template-columns: 1fr; }
  .topnav { padding: 0.5rem 1rem; }
  .sc-title { font-size: 1.15rem; }
}