From eeb98d6a0c1825a0b975fee631922a9fdd5fac73 Mon Sep 17 00:00:00 2001 From: mamut-studio Date: Sat, 4 Jul 2026 14:11:31 +0200 Subject: [PATCH] docs: drop braggy tone, rename SEL4_REVIEW -> SYSTEMS_REVIEW Remove self-promotional phrasing from the docs and stop using seL4 as a quality badge. seL4/l4v now appears only where load-bearing (the l4v dependency for AutoCorres, a methodology contrast, review provenance). - README: state the coding discipline as plain facts instead of "seL4-grade coding discipline"; plainer smoke-path wording - rename docs/SEL4_REVIEW.md -> docs/SYSTEMS_REVIEW.md and update all references (README, DEVELOPMENT, docs/README); retitle the doc and its strengths section Co-Authored-By: Claude Opus 4.8 --- DEVELOPMENT.md | 2 +- README.md | 10 +++++----- docs/README.md | 4 ++-- docs/{SEL4_REVIEW.md => SYSTEMS_REVIEW.md} | 4 ++-- 4 files changed, 10 insertions(+), 10 deletions(-) rename docs/{SEL4_REVIEW.md => SYSTEMS_REVIEW.md} (99%) diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md index e7cf505..43a5c9b 100644 --- a/DEVELOPMENT.md +++ b/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 diff --git a/README.md b/README.md index 18a214a..80019cc 100644 --- a/README.md +++ b/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 `` and `` 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. diff --git a/docs/README.md b/docs/README.md index 475a518..4f124b5 100644 --- a/docs/README.md +++ b/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. diff --git a/docs/SEL4_REVIEW.md b/docs/SYSTEMS_REVIEW.md similarity index 99% rename from docs/SEL4_REVIEW.md rename to docs/SYSTEMS_REVIEW.md index 94224a4..6a7ebda 100644 --- a/docs/SEL4_REVIEW.md +++ b/docs/SYSTEMS_REVIEW.md @@ -1,6 +1,6 @@ -# 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: