More edits

dstebila · dstebila · commit 0a533f897fe4 · 2026-04-11T16:04:56.000-04:00
diff --git a/assets/diagram.svg b/assets/diagram.svg
@@ -177,10 +177,10 @@
   <line x1="600" y1="1000" x2="600" y2="1030" class="connector"/>
 
   <!-- Canonical form boxes -->
-  <rect x="120" y="1030" width="200" height="35" class="box-green"/>
+  <rect x="120" y="1030" width="200" height="35" class="box"/>
   <text x="220" y="1053" text-anchor="middle" class="label">Canonical form A</text>
 
-  <rect x="500" y="1030" width="200" height="35" class="box-green"/>
+  <rect x="500" y="1030" width="200" height="35" class="box"/>
   <text x="600" y="1053" text-anchor="middle" class="label">Canonical form B</text>
 
   <!-- Both canonical forms converge into comparison diamond -->
diff --git a/researchers/index.md b/researchers/index.md
@@ -3,6 +3,7 @@ title: For Researchers
 layout: default
 nav_order: 4
 has_children: true
+has_toc: false
 permalink: /researchers/
 ---
 
@@ -12,7 +13,7 @@ This area of the site is for people who want to *understand* ProofFrog's design,
 
 If you are learning provable security or are new to ProofFrog, we recommend starting with the [manual]({% link manual/index.md %}).
 
-- [Scientific Background]({% link researchers/scientific-background.md %}) — motivation, the three tasks of a game-hopping proof, design choices, positioning relative to other tools, and what ProofFrog is and isn't.
+- [Scientific Background]({% link researchers/scientific-background.md %}) —  ProofFrog's design choices and positioning relative to other tools.
 - [Engine Internals]({% link researchers/engine-internals.md %}) — high-level architecture, core modules, the transformation pipeline by category, diagnostics and near-miss matching, the engine-introspection CLI commands, and the LSP and MCP servers.
 - [Soundness]({% link researchers/soundness.md %}) — what ProofFrog claims, what is in the trust base, what is *not* claimed, mitigations a careful user can apply, and the comparison framing relative to EasyCrypt and CryptoVerif.
 - [GenAI & Proving]({% link researchers/gen-ai.md %}) — using LLM-based coding assistants to draft and iterate on proofs (a research-and-experimentation tool, not a recommended student workflow).
diff --git a/researchers/scientific-background.md b/researchers/scientific-background.md
