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.
The listing matches the requested formats case-insensitively, prunes dotfiles and dot-directories, and sorts rows by modification time descending.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
The listing matches the requested formats case-insensitively, prunes dotfiles and dot-directories, and sorts rows by modification time descending. The script rejects a nonexistent path on stderr with exit 1.
when paths_given the file_picker shall eventually satisfy listing_shape
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
bin/omarchy-menu-file lines 28-48.
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:28 UTC · Leonid Bugaev
Hazard review
- scenarioreviewedboundaryedge_caseerror_handling
Worst case: a hostile directory layout makes the picker lie - a dot-directory prune miss leaks hidden files into a user-facing pick list, and a case-fold mismatch silently drops files the caller asked for. boundary: dotfile vs dot-directory pruning is the exact partition (files named .jpg are dropped by the ! -name .*, dot-directories are pruned except the search roots themselves via ! -name ., and -iname matches case-insensitively while the prune stays case-sensitive). edge_case: filenames containing tabs or newlines collide with the %T@ tab record format, mangling single rows (cosmetic row loss, no crash, no wrong file selected); an empty formats word lands in the usage guard. error_handling: every nonexistent path element rejects with stderr and exit 1 before any listing (tested); find stderr is suppressed so an unreadable subdirectory yields a silently partial listing rather than an abort - honest gap, consequence limited to a truncated pick list. Catalog 1.11.0 re-review: input_domain not applicable, it lists file names and modification times and reads no file contents. concurrency_scale not applicable, one run per user action that owns its own temp files and shares no state with a concurrent run.
- propertyrevieweddeterminismtotality
determinism: rows order solely by sort -rn over the %T@ epoch float; equal timestamps fall to the whole-line reverse string compare, which is stable for a given directory state. totality: every (paths, formats) input resolves to one defined ending - usage exit 1, missing-path exit 1, or the filtered listing - with no input leaving the picker half-drawn.
- structuralnot applicable
Bash over GNU find: arguments are built as an array so a format word like -o -type d is passed as a single -iname glob operand, never re-parsed as an option; no eval, no IFS word-splitting of file data, no arithmetic.
- domainnot applicable
Local-filesystem reads plus the omarchy-menu-select IPC summon owned by the protocol siblings (SW-REQ-260922-Q6ZS/9ABD); no network egress, crypto, secrets, or privilege surface in the listing slice this requirement governs.
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-51
Read omarchy-menu-file. The listing filters requested formats case-insensitively, prunes dotfiles and dot-directories, sorts by mtime descending, and a nonexistent path is rejected on stderr (usage guard for <3 args is separate). The paths_given condition models the listing entry point; the listing_shape response covers filter/prune/sort. 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.
1 obligation · 1 deferred
Browse the catalogueEvery cross-process call shall declare connect, read, and total deadlines; no external call is defaulted to "no timeout."
omarchy-menu-file hands its listing to omarchy-menu-select and waits synchronously; the callee polls the done_file with no deadline and no peer-liveness probe, so a menu that dies after summon hangs every menu-file caller - the same reproduced defect class as the KI, third caller downstream of the same unbounded poll. The bound belongs to the KI fix at the poll site, which bounds this caller transitively.
- nominalrequireddeferredWitnessing deferred — accepted while the tracking known issue stays open.
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 paths_given the file_picker shall eventually satisfy listing_shape
Witnesses· 2 scenarios total
- menu-file-test.sh:1exercises 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| # | listing_shape | paths_given | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | T | paths_given | |
| 2 | F | T | F | listing_shape | Exempted · defensive — the find pipeline (prune dotdirs, drop dotfiles, match formats, print mtime+path, sort newest first, cut to the path) is built unconditionally once the paths validate; a misshapen listing from valid paths needs a broken find arg build mcdc:witness-out-of-process (reviewed: REVIEW-M7) |
| 3 | T | T | T | listing_shape |
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)
- omarchy-menu-filebin/omarchy-menu-file
Tests to re-run (1)
- menu-file-test.shtest/shell.d/menu-file-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.