Proof Portal
Omarchy
ProbeLabsviewing a historical runA 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 no item declares a guard, the guard script is empty and no guard process runs.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
When no item declares a guard, the guard script is empty and no guard process runs.
when no_guards_declared the guard_pipeline shall eventually satisfy empty_guard_script
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
MenuModel.js guardScript line 490; menu-guards-test.sh pins the empty case.
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:25 UTC
History
- Created
- Sep 22, 2026, 13:34 UTC · Kimi Dogfood · AI agent
- Modified
- Sep 30, 2026, 07:43 UTC · Leonid Bugaev
Hazard review
- scenarioreviewedboundaryedge_case
Worst case: a guard process spawns for a menu with nothing to guard - wasted spawn plus a stale-answers window - closed by the empty-script early return that also clears all three result maps, so a zero-guard menu renders with no marks and no bash at all. boundary: both halves of the zero case are pinned - no declared guards yields the empty script (the generator contract this consumption sits on) and the empty script yields no process. edge_case: an evaluation while a guard run is in flight defers to the in-flight run (guardsPending), and a guard expression that never completes keeps that run alive forever, stalling all future refreshes - consequence bounded to answer staleness per the documented menu-opens-on-last-answers tradeoff, with the UI itself unaffected. Catalog 1.11.0 re-review: input_domain not applicable, it reads no external text input. concurrency_scale not applicable, no guard means no process runs at all.
- propertyreviewedtotalityidempotency
totality: declared-guard and zero-guard item sets each resolve to exactly one outcome (spawn and collect, or clear-and-skip), with no third path. idempotency: repeated evaluation over unchanged items re-derives the same script and the same results, and the result maps are replaced wholesale rather than merged, so no state accumulates across evaluations.
- structuralnot applicable
An emptiness test on the generated script plus a Process command array with fixed argv (bash -lc script); results are plain object swaps with no parsing of the script on this side.
- domainnot applicable
A local bash spawn over user-authored guards with the user own authority - the same boundary dispositioned at the generator (MQ37) - and no network, crypto, or privilege surface in the spawn-and-collect slice.
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-69
Read guardScript. guards accumulates one guardLine per declared when/checked/disabled; the function returns '' exactly when the accumulated string is empty, so no prelude and no guard process exist for guardless item sets. no_guards_declared models the empty-accumulator case; empty_guard_script is the '' return. Formula conforms to the code.
Cited code (1)
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).
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 no_guards_declared the guard_pipeline shall eventually satisfy empty_guard_script
Witnesses· 2 scenarios total
- preludeexercises 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| # | empty_guard_script | no_guards_declared | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | T | no_guards_declared | |
| 2 | F | T | F | empty_guard_script | — |
| 3 | T | T | T | empty_guard_script |
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)
- MenuModel.jsshell/plugins/menu/MenuModel.js
Tests to re-run (1)
- menu-guards-test.shtest/shell.d/menu-guards-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.