docs: drop braggy tone, rename SEL4_REVIEW -> SYSTEMS_REVIEW

DEVELOPMENT.md

@@ -44,6 +44,6 @@ validation.
 
 ## Review posture
 
-- treat `docs/SEL4_REVIEW.md` as the main current gap register
+- treat `docs/SYSTEMS_REVIEW.md` as the main current gap register
 - keep bounded loops / static configuration / no dynamic allocation posture
 - prefer explicit hardening over feature growth

README.md

@@ -5,8 +5,8 @@
 
 A small C coordination runtime (~7100 lines) implementing decaying shared fields,
 k=7 topological neighbor election, heartbeat-based failure detection, and threshold
-consensus. Written with seL4-grade coding discipline: no dynamic allocation, no
-recursion, bounded loops, static configuration. Includes an Isabelle/AutoCorres
+consensus. The code avoids dynamic allocation and recursion, keeps loops
+bounded, and uses static configuration. Includes an Isabelle/AutoCorres
 verification session: the ballot evaluation core is machine-checked against a
 pure HOL spec (phase B2), and a TLA+ model checks the consensus protocol's
 safety invariants above it (bounded model checking — see docs/tla/).
@@ -27,7 +27,7 @@ cmake --build build
 ctest --test-dir build --output-on-failure
 ```
 
-This is the shortest trustworthy proof that the repo is alive.
+This is the shortest check that the repo builds and passes its tests.
 
 ## Components
 
@@ -41,7 +41,7 @@ This is the shortest trustworthy proof that the repo is alive.
 
 - `docs/README.md` - documentation entrypoint
 - `docs/KEY_COMPONENTS.md` - subsystem map
-- `docs/SEL4_REVIEW.md` - current correctness and hardening gaps
+- `docs/SYSTEMS_REVIEW.md` - current correctness and hardening gaps
 - `docs/VERIFICATION_PLAN.md` - proof-track scope and milestones
 
 ## Verification
@@ -74,7 +74,7 @@ Replace `<isabelle>` and `<l4v>` with paths to your local installations.
 
 ## Known Issues
 
-See [docs/SEL4_REVIEW.md](docs/SEL4_REVIEW.md) for a detailed systems review
+See [docs/SYSTEMS_REVIEW.md](docs/SYSTEMS_REVIEW.md) for a detailed systems review
 covering correctness defects, undefined-behaviour paths, and verification-readiness
 gaps.
 

docs/README.md

@@ -9,7 +9,7 @@ Use this directory as the documentation entrypoint for `ekk-runtime`.
 
 - `KEY_COMPONENTS.md` - quickest subsystem map for the runtime
 - `SECURITY.md` - threat-model artifact pointer and deployment assumptions
-- `SEL4_REVIEW.md` - current correctness and hardening gap register
+- `SYSTEMS_REVIEW.md` - current correctness and hardening gap register
 - `MILESTONE_RUNTIME_HARDENING.md` - implementation hardening sequence
 
 ## Verification Track
@@ -22,5 +22,5 @@ Use this directory as the documentation entrypoint for `ekk-runtime`.
 
 1. Read the root `README.md`.
 2. Read `KEY_COMPONENTS.md`.
-3. Read `SEL4_REVIEW.md`.
+3. Read `SYSTEMS_REVIEW.md`.
 4. Only then dive into the verification track if you need proof-layer detail.

docs/SEL4_REVIEW.md → docs/SYSTEMS_REVIEW.md

@@ -1,6 +1,6 @@
 <!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
 <!-- Copyright (c) 2026 mamut-studio.com -->
-# EK-KOR v2 — seL4 Systems Review
+# EK-KOR v2 — Systems Review
 
 **Reviewer:** sel4-systems-reviewer agent
 **Date:** 2026-03-18
@@ -262,7 +262,7 @@ Any caller of `ekk_hal_recv` drains messages regardless of `dest_id`. In a multi
 
 ---
 
-## 6. Things Done Right
+## 6. Strengths
 
 The following properties are explicitly confirmed and should be preserved: