Proof Portal

Project overview

Omarchy

ProbeLabsviewing a historical run

A proof layer — requirements, tests and verified fixes — for two of Omarchy's subsystems: the application menu (launcher scripts, QML model, JSONC config, search and selection) and the lock screen (lock scripts, QML, PAM authentication). Scope is deliberately limited to those components of omacom/omarchy; the rest of the distribution is not covered.

Viewing historical run 20d4e6aOct 2, 2026, 05:32 PMquattro-proofBack to current
All requirements
RequirementSW-REQ-260922-N3RMSoftwareReview

When a route resolves to an action item with a non-empty action, the action runs directly and no menu opens.

This requirement changed after its last recorded review, so approval is stale. Automated checks pass.
PriorityshallTypeguaranteeCategoryfunctionalComponentmenuAssuranceCFindingsLowworst open

Specification

The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.

Description

When a route resolves to an action item with a non-empty action, the action runs directly and no menu opens.

FRETish formula
when resolved_kind_action the menu_router shall eventually satisfy action_runs_directly & menu_not_opened
View full formal model

Rationale & tags

Why this requirement exists, and how it is categorised.

Menu.qml openRoute lines 895-905; opening an action as a submenu would show an empty list.

Verification & provenance

How this requirement was checked: the review trail, edit history, and the machine-analysis status terms (each ⓘ explains what it means).

Assurance levelC
Formalizationvalid
Realizabilityrealizable
Vacuitychecked_ok
Strategyfretish

Review

Status
in_review
Reviewer
Kimi Zero Warnings · AI agent
Reviewed
Sep 27, 2026, 21:10 UTC

History

Created
Sep 22, 2026, 13:34 UTC · Kimi Dogfood · AI agent
Modified
Sep 30, 2026, 07:35 UTC · Leonid Bugaev

Hazard review

Reviewed Oct 1, 2026, 21:26 UTCby agent:claude-baseline-passcatalog v1.11.0
  • scenarioreviewedboundaryedge_caseerror_handling

    Worst case: a route resolves to an action item, the menu closes, and the action silently never runs (execDetached is fire-and-forget) - the user loses the interaction with no reopen path in this slice; consequence is a lost launch, not a wrong one. boundary: the zero cases are pinned - empty id cancels, empty action no-ops, and applySelected closes the menu before dispatch so a failed action cannot leave the menu half-open. edge_case: the summonAction fast path passes the single-quoted payload literally to the in-process summon while the bash path would have shell-expanded it - same user authority, different expansion timing; the divergence is owned by SW-REQ-260928-8VJQ which pins the fast path, and N3RM only requires that a resolved action runs directly without opening a menu. Catalog 1.11.0 re-review: input_domain not applicable, it reads no external text input. concurrency_scale not applicable, a pure function of its arguments, recomputed on each load or keystroke: no state across calls, no process, timer or lock.

  • propertyreviewedtotality

    Every resolved (kind, action) ending is defined: action item with non-empty action runs directly with no menu open, empty action no-ops, empty id cancels - no route ends with the menu reopening or the action firing twice.

  • structuralnot applicable

    The fast-path regex is bounded ([A-Za-z0-9._-]+ for the id, single-quote-delimited payload), the action string dispatches as one argv to execDetached, and no payload is string-built or evald in QML.

  • domainnot applicable

    Actions are user-authored commands from user-owned config executing with the user own privileges; the fast path only changes spawn plumbing (in-process summon vs bash), not authority, and the traced files carry no network, crypto, or privilege surface.

Change history

Every recorded revision of this requirement's source file — newest first, each with its commit message and the diff for that change.

Review history

Human and AI-agent approvals of this requirement — the 'why was this approved' lineage, each with the reviewer's justification and the code it cites.

  1. Kimi Zero Warnings · AI agentApprovedSpec conformanceSep 27, 2026 · 5 days agoREVIEW-29

    Read openRoute (Menu.qml:954-970) and runAction (Menu.qml:143-148). A resolved action entry with non-empty action triggers root.cancel() then runAction(entry.action) -> Util.execDetached, returning ok without opening a menu. Link entries follow target; menu entries open normally. The formula (action item with non-empty action -> action runs directly, no menu opens) matches both branches; the empty-action guard in runAction is the silent precondition.

    Cited code (2)

Open known issues

Findings currently open against this requirement — issues its verification surfaced that are not resolved yet. Each links to the full finding.

Obligations

What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.

The tests that discharge each obligation aren't available for a historical run

The evidence matrix behind each obligation comes from the live audit index, which can't be rebuilt for a past commit. Nothing here means unknown — not that the requirement has no obligations.

Formula evidence

The formal formula behind this requirement, the variables it is written over, and the tests that exercise it (each term is explained inline).

FRETish formula

when resolved_kind_action the menu_router shall eventually satisfy action_runs_directly & menu_not_opened

Witnesses· 2 scenarios total

  • menu-test.sh:1
    exercises 2 condition scenarios

MC/DC truth table· 5 rows

Each row assigns the formula's conditions (T/F) and shows the Result— the formula's value for that input row, not a test pass/fail. A row proves a condition when flipping only that condition flips the outcome. The test that covers each row is linked.

Covereda test exercises this rowExempteda reviewed mcdc:ignoreNo-actionfalse-result row satisfied by designUncoveredneeds a covering test
#action_runs_directlymenu_not_openedresolved_kind_actionResultProvesCovering test
1FFFTresolved_kind_action
2FFTFresolved_kind_actionExempted · defensive — displayRow copies the entry's action and resolves target by kind unconditionally; an action row that opens a menu needs the kind ternary removed (reviewed: REVIEW-M8)
3FTTFaction_runs_directlyExempted · defensive — same unconditional action copy; an action row without its action needs the copy removed (reviewed: REVIEW-M8)
4TFTFmenu_not_openedExempted · defensive — the action row's target is its own id by the same ternary, so activation never navigates; opening a menu needs the ternary removed (reviewed: REVIEW-M8)
5TTTTaction_runs_directly

Its place

How this requirement connects — what proves it, what it affects, and what it rests on. Authored links only here; automatically derived links come from the audit index.

Loading graph…

Trace evidence

The concrete artifacts linked to this requirement — implementing code, verifying tests, documents, and the findings raised against it.

Impact

Blast radius — authored trace links only (automatically derived links come from the audit index and aren't shown here).

If you change this

Requirements
0
Files
1
Tests
2
At-risk contracts
0

Files to re-check (1)

  • Menu.qmlshell/plugins/menu/Menu.qml

Tests to re-run (2)

  • menumodel-replay.test.mjstest/node/menumodel-replay.test.mjs
  • menu-test.shtest/shell.d/menu-test.sh

What this rests on

Discussions

Discuss this with the proof team. Nothing changes in your audit automatically — you open a request and a staff member records any outcome inside the thread.

Sign in to discuss this with the proof team.Sign in