Proof Portal
Omarchy
ProbeLabs73 findings · 87 requirementsA 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.
When a route resolves to an action item with a non-empty action, the action runs directly and no menu opens.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
When a route resolves to an action item with a non-empty action, the action runs directly and no menu opens.
when resolved_kind_action the menu_router shall eventually satisfy action_runs_directly & menu_not_opened
Rationale & tags
Why this requirement exists, and how it is categorised.
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).
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
- 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.
- 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.
- LowOpen
goBack refuses to retrace while activeMenu is root, stranding navStack after a drill that landed on root
KI-MENU-GOBACK-ROOT-STRAND
- LowOpen
openRoute follows a link one hop and never re-inspects the target kind: link-to-action opens as a menu
KI-MENU-LINK-SINGLE-HOP
- LowOpen
pendingInitialMenu is stored and never read: a route summoned before the JSONC loads opens root and stays there
KI-MENU-PENDING-INITIAL-MENU-DEAD
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 need a synced audit
The evidence matrix behind each obligation comes from the audit index, which is produced by running an audit — not read from git. 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).
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:1exercises 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.
mcdc:ignoreNo-actionfalse-result row satisfied by designUncoveredneeds a covering test| # | action_runs_directly | menu_not_opened | resolved_kind_action | Result | Proves | Covering test |
|---|---|---|---|---|---|---|
| 1 | F | F | F | T | resolved_kind_action | |
| 2 | F | F | T | F | resolved_kind_action | Exempted · 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) |
| 3 | F | T | T | F | action_runs_directly | Exempted · defensive — same unconditional action copy; an action row without its action needs the copy removed (reviewed: REVIEW-M8) |
| 4 | T | F | T | F | menu_not_opened | Exempted · 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) |
| 5 | T | T | T | T | action_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).
Impact
Blast radius — authored trace links only (automatically derived links come from the audit index and aren't shown here).
If you change this
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.