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: