diff --git a/.kiro/specs/raft-sim-conformance/design.md b/.kiro/specs/raft-sim-conformance/design.md
index 43c9f410..ce31de25 100644
--- a/.kiro/specs/raft-sim-conformance/design.md
+++ b/.kiro/specs/raft-sim-conformance/design.md
@@ -158,14 +158,14 @@ flowchart TB
     end
     subgraph ADAPT["In-memory adapter callbacks (raft_sim.c = the adapter)"]
         A1["on_persist_entry -> node.log[]"]
-        A2["on_get_entry_term -> node.log[idx].term | 0"]
+        A2["on_get_entry_term -> node.log[idx].term | 0"]
         A3["on_send_append_entries -> bag.push(AE req)"]
         A4["on_truncate_from -> node.log truncate"]
         A5["on_commit_advanced -> node.commit_index + apply()"]
         A6["on_send_vote_request -> bag.push(vote req)"]
     end
     subgraph BAG["Message bag (cluster.bag[]) — mirrors raft.tla messages"]
-        B["vote/AE requests + responses;<br/>Drop/Duplicate/Reorder live here"]
+        B["vote/AE requests + responses,<br/>Drop/Duplicate/Reorder live here"]
     end
     subgraph CHK["Invariant checkers (after every step, R3)"]
         I1["Election Safety"]
@@ -266,7 +266,7 @@ sequenceDiagram
         L->>A: on_send_append_entries -> bag.push(AE req)
     else AdvanceCommitIndex
         S->>L: raft_advance_commit()
-        L->>A: on_commit_advanced -> commit_index += ; apply()
+        L->>A: on_commit_advanced -> commit_index advanced, apply()
     else Receive (deliver one bag message)
         S->>B: pop selected message
         S->>L: route to handler (on_vote_request / on_append_entries_request / *_reply)
@@ -278,7 +278,7 @@ sequenceDiagram
     end
     S->>C: raft_sim_check_all() (R3)
     alt any invariant violated
-        C-->>S: fail -> dump seed + trace + invariant (R5); halt
+        C-->>S: fail -> dump seed + trace + invariant (R5), then halt
     else ok
         C-->>S: continue
     end
@@ -308,7 +308,7 @@ flowchart LR
         CM["node.commit_index"]
         AP["node.applied[]"]
     end
-    R --> ES["Election Safety: |{i: role==LEADER, term==t}| <= 1, all t (R3.1)"]
+    R --> ES["Election Safety: &#124;{i: role==LEADER, term==t}&#124; <= 1, all t (R3.1)"]
     LG --> LM["Log Matching: pairwise, shared (idx,term) => identical prefix (R3.2)"]
     LG --> LC["Leader Completeness: committed entry in every higher-term leader log (R3.3)"]
     CM --> LC