Skip to content

MVP alpha.11: Close gaps for beta - #67

Merged
ZebulonRouseFrantzich merged 10 commits into
mainfrom
mvp/beta_close_gaps_and_polish
May 8, 2026
Merged

MVP alpha.11: Close gaps for beta#67
ZebulonRouseFrantzich merged 10 commits into
mainfrom
mvp/beta_close_gaps_and_polish

Conversation

@ZebulonRouseFrantzich

Copy link
Copy Markdown
Contributor

This pull request introduces several significant improvements to the CI pipeline and documentation, with a focus on formal security model checking, performance contract enforcement, and updated project status. The CI workflow now includes a dedicated formal security kernel job that conditionally runs TLA+ model checks based on PR changes, and a required shared-Linux performance contract gate. Documentation has been updated to reflect these new CI lanes, clarify the supported product surface, and provide more detail on security and attestation flows.

CI/CD Pipeline Enhancements:

  • Added a formal-security-kernel job to the GitHub Actions workflow (.github/workflows/ci.yml) that conditionally runs TLA+ model checks (just model-check, just model-check-core) based on which files are changed in a PR, improving efficiency and ensuring formal verification coverage where needed.
  • Introduced a required shared-Linux performance contract gate by renaming and updating the canonical Linux CI lane to ci-required-shared-linux, and clarified the matrix labels for CI jobs.
  • Enabled workflow concurrency controls to prevent duplicate runs and cancel in-progress runs for PRs.

Documentation Updates:

  • Updated README.md and CONTRIBUTING.md to document the new CI lanes (ci-required-shared-linux, ci-fast, model-check-core, model-check-replay), clarify that only the required shared-Linux performance contract subset is enforced on CI, and describe the new formal security kernel check. [1] [2] [3]
  • Revised project status and component descriptions to reflect the current supported surface, more accurate attestation and evidence flows, and the addition of performance contracts and TLA+ model checking. [1] [2] [3] [4]

Minor Improvements:

  • Added a new help output line for change_draft to the broker CLI core test, reflecting the default low-level start command.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>
Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>
Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>
…ges: things to implement pre-MVP and post-MVP.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>
Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>
* Implements Runtime Attestation Post-Handshake Gating v0

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates to close gaps found between implementation and change documents.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates based on PR comments

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates based on PR comments and to fix failing checks.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates README and standards.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

---------

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>
* Updates and enhances change documents for this branch.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates downstream changes from branch's change.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* More refinements of the change documents.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Implements performance baselines verification gates v0

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates things so long running TLA runs in merge queue, but focused TLA runs every pull request.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates based on PR comments.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates based on PR comments.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates based on PR comments.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates based on more PR comments.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates to fix failing checks.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Another fix for another check failure.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates to help failing checks.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates so 'runectx validate' succeeds.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates to fix the failing performance check.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates to fix more failures.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates again to fix check

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates to fix performance check issues in job

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

---------

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>
* Updates and enhances CHG-2026-060-c1a4-beta-readiness-hardening-product-polish change docs

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates and refines downstream changes.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Implements beta-readiness-hardening-product-polish (except for the TUI polish).

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates to close gaps found between implementation and change docs.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Fixes testing gaps.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Fixes PR comments and failing checks

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* More changes for PR comments and check fixes.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* More updates from PR comments.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Fixes comments and failing checks.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Fixes failing checks.

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

* Updates to README and standards

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>

---------

Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>
Comment thread runner/src/runner-identifiers.ts Fixed
Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>
@ZebulonRouseFrantzich
ZebulonRouseFrantzich added this pull request to the merge queue May 8, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to no response for status checks May 8, 2026
Signed-off-by: Zebulon Rouse-Frantzich <zeb@runecode.org>
@ZebulonRouseFrantzich
ZebulonRouseFrantzich added this pull request to the merge queue May 8, 2026
Merged via the queue into main with commit 800ccc2 May 8, 2026
11 checks passed
@ZebulonRouseFrantzich
ZebulonRouseFrantzich deleted the mvp/beta_close_gaps_and_polish branch May 8, 2026 19:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants