MVP alpha.11: Performance baselines and verification gates v0

[ZebulonRouseFrantzich]

This pull request introduces significant improvements to the CI workflow, formal model checking, and the handling of runtime evidence and attestation posture in the codebase. The main changes include a new dedicated TLA+ security kernel check in CI, refined logic for authoritative provisioning posture, and expanded documentation and commands for formal model checking. These updates improve the reliability of security checks, clarify posture transitions, and ensure that the system's security model is consistently enforced and well-documented.

CI Workflow and Formal Model Checking Enhancements:

• Added a dedicated formal-security-kernel job to the CI workflow (.github/workflows/ci.yml) that automatically determines when to run full or core TLA+ model checks based on the scope of changes in a pull request, preventing unnecessary runs and ensuring coverage for security-critical changes. Also, introduced workflow concurrency controls to avoid duplicate runs. [1] [2]
• Updated documentation and command references in README.md, CONTRIBUTING.md, and formal/tla/security-kernel/README.md to include new model check commands (just model-check-core, just model-check-replay) and to clarify the CI model checking strategy. [1] [2] [3] [4] [5]

Runtime Evidence and Attestation Posture Logic:

• Refined the process for normalizing and reconciling runtime evidence and attestation posture in internal/artifacts/store_runtime_facts.go and related files. The code now ensures that the attested provisioning posture is only projected after secure-session validation, post-handshake evidence collection, and trusted verification, preventing premature or incorrect posture assignment. [1] [2] [3] [4] [5]
• Added logic to consistently update both RuntimeFactsSnapshot and RuntimeEvidenceSnapshot with authoritative provisioning posture, and to handle lifecycle state updates more robustly, including fallback handling for missing facts. [1] [2]

Attestation Verification Handling:

• Improved the logic for applying cached attestation verification and detecting replay placeholders in internal/artifacts/store_runtime_attestation_cache.go, ensuring that only valid or specifically marked placeholder records are accepted. [1] [2]

Documentation Updates:

• Updated various sections in README.md to clarify the security model, including the requirements for projecting attested posture and the linkage of audit events to persisted evidence, reflecting the improved posture transition logic. [1] [2]

These changes collectively strengthen the project's security posture, streamline CI runs, and improve clarity for contributors and reviewers.

[Copilot]

Pull request overview

This PR adds the first Linux-first performance-contract/gating slice, introduces path-aware formal TLA checking in CI, and tightens runtime attestation/provisioning-posture projection in the trusted Go path. The main review blockers are in performance-gate enforcement and measurement correctness, so the PR is not approval-ready yet.

Changes:

• Adds new CI/formal-check entrypoints and supporting CLI tooling (tlccheck, perf harness wrappers, shared-Linux perf gate flow).
• Introduces performance contract inventory/docs for broker, runner, TUI, gateway/secrets, launcher, dependency/audit, and attestation surfaces.
• Refines trusted runtime evidence handling so attested posture is projected from verified post-handshake evidence instead of launch-time claims alone.

Reviewed changes

Copilot reviewed 183 out of 183 changed files in this pull request and generated 8 comments.

Show a summary per file

File	Description
.github/workflows/ci.yml	Adds dedicated shared-Linux perf lane and formal security-kernel job.
justfile	Adds new CI recipes for model-check variants and shared-Linux perf enforcement.
README.md	Documents new model-check and CI/perf verification surfaces.
CONTRIBUTING.md	Updates contributor workflow guidance around CI/model-check commands.
formal/tla/security-kernel/README.md	Documents the new TLC mode split (all, core, replay).
internal/artifacts/store_runtime_facts.go	Reconciles authoritative provisioning posture into persisted facts/evidence.
internal/artifacts/store_runtime_attestation_cache.go	Tightens cached attestation verification / replay-placeholder handling.
internal/brokerapi/service_runtime_facts.go	Projects authoritative runtime posture when reading runtime facts/evidence.
internal/brokerapi/perf_phase5_gateway.go	Adds phase-5 gateway/secrets performance measurements.
internal/perfcontracts/evaluate.go	Implements contract evaluation against measurements/baselines.
tools/perfcontracts/README.md	Adds governance and statistical-policy docs for performance contracts.
tools/perfcontracts/manifest.json	Registers the checked-in performance contract/baseline inventory.
tools/tlccheck/main.go	Adds CLI mode selection for full/core/replay TLC runs.
tools/tlccheck/modes.go	Maps TLC modes to config subsets.
tools/tlccheck/main_test.go	Adds coverage for TLC mode selection.
tools/perfseedwait/main.go	Adds deterministic fixture seeding mode and trims emitted session summary.
tools/tuiperf/args.go	Adds CLI parsing for TUI perf modes and sampling parameters.
tools/tuiperf/main.go	Adds the Linux-only TUI perf CLI entrypoint.
tools/tuiperf/types.go	Defines TUI perf config/envelope types.
tools/tuiperf/util.go	Adds marker wait, fixture seeding, and envelope helpers for TUI perf runs.
tools/runnerworkflowperf/main.go	Adds CLI wrapper for runner workflow performance harness output.
tools/phase5perf/main.go	Adds CLI wrapper for phase-5 broker/gateway performance harness output.

[Copilot]

Pull request overview

Copilot reviewed 194 out of 194 changed files in this pull request and generated 12 comments.

[Copilot]

Pull request overview

Copilot reviewed 124 out of 124 changed files in this pull request and generated 3 comments.

[Copilot]

Pull request overview

Copilot reviewed 125 out of 125 changed files in this pull request and generated 4 comments.