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.
Delete with the cursor on an app row opens an uninstall confirmation naming the app.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
Delete with the cursor on an app row opens an uninstall confirmation naming the app. Confirming removes the app through the shared app library and closes the menu. Cancelling closes the dialog and returns focus without removing anything. Non-app rows ignore the key.
when delete_key_on_app the menu_actions shall eventually satisfy uninstall_confirmed_flow
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
Menu.qml requestDeleteSelected/cancelDelete/confirmDelete lines 789-813 and Keys.onPressed line 1129.
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, 20:50 UTC
History
- Created
- Sep 22, 2026, 15:09 UTC · Kimi Dogfood · AI agent
- Modified
- Sep 27, 2026, 20:47 UTC · Kimi Zero Warnings · AI agent
Hazard review
- scenarioreviewedboundaryedge_case
Worst case: the destructive arm fires on the wrong object or without consent - confirm binding to the cursor row at confirm time instead of the row the dialog named (closed: deleteTarget snapshots appId+label at open and confirmDelete consumes only that snapshot, so cursor movement under a live dialog cannot retarget the removal), or the dialog failing open (closed: the dialog opens with its selection preset to the No arm, cancel and reopen both reset it, and onOpenedChanged clears dialog state the moment the menu closes). boundary: cursor bounds (no cursor, negative, past end) and the kind!==app gate are the tested partition edges - non-app rows ignore Delete entirely. edge_case: double Delete while the dialog is open re-snapshots the target, Enter-Enter double-confirm finds deleteTarget already null and returns, and Esc-then-reopen starts a clean dialog - none of which can stack two removals. The removal itself and its privilege handling are the app library's own requirements. Catalog 1.11.0 re-review: input_domain not applicable, it reads no external text input. concurrency_scale not applicable, one modal confirmation at a time; repeated Delete presses re-open the same dialog.
- propertyreviewedtotality
Every key-press state (no cursor, out-of-range cursor, non-app row, app row, dialog already open, dialog already closed) resolves to a fully defined outcome - ignore, open dialog, re-open dialog, confirm once, or cancel - with no state leaving a dangling dialog or an orphaned deleteTarget behind.
- structuralnot applicable
Index comparisons, a two-field object snapshot, and boolean dialog flags; no memory, pointer, encoding, or numeric-overflow surface.
- domainnot applicable
Pure UI dialog state machine; the package removal and its privilege escalation live in the shared app library behind appLibrary.remove, owned by that component's requirements - nothing here crosses a privilege boundary, touches a file, or reaches the network.
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-27
Read the delete flow at Menu.qml:841-875. requestDeleteSelected ignores invalid cursors and non-app rows, opens a confirmation naming the app (deleteTarget.label). cancelDelete closes the dialog, restores focus, removes nothing. confirmDelete closes the menu and removes via appLibrary.remove. delete_key_on_app -> uninstall_confirmed_flow matches: the key on an app row always leads to the confirmed/cancelled uninstall flow, never a direct delete.
Cited code (3)
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 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 delete_key_on_app the menu_actions shall eventually satisfy uninstall_confirmed_flow
Witnesses· 2 scenarios total
- pokeGuardsexercises 2 condition scenarios
MC/DC truth table· 3 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| # | delete_key_on_app | uninstall_confirmed_flow | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | T | delete_key_on_app | |
| 2 | T | F | F | delete_key_on_app | Exempted · defensive — requestDeleteSelected opens the confirmation for every app row; an app row ignoring Delete needs the kind check removed (reviewed: REVIEW-MC1) |
| 3 | T | T | T | uninstall_confirmed_flow |
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 (1)
- menu-compositor-test.shtest/shell.d/menu-compositor-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.