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 a72e7f1Oct 2, 2026, 07:59 AMpr/6525Back to current
All requirements
RequirementSW-REQ-260922-T257SoftwareReview

toggle, summon, close, refresh, and ping each exec the matching omarchy-shell IPC call.

This requirement changed after its last recorded review, so approval is stale. Automated checks pass and 2/2 obligations are satisfied.
PriorityshallTypeguaranteeCategoryfunctionalComponentmenuAssuranceCFindingsLowworst open

Specification

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

Description

toggle, summon, close, refresh, and ping each exec the matching omarchy-shell IPC call. toggle and summon pass the route as a JSON payload. help prints usage and exits 0.

FRETish formula
when verb_known the menu_dispatcher shall eventually satisfy ipc_call_executed
View full formal model

Rationale & tags

Why this requirement exists, and how it is categorised.

bin/omarchy-menu lines 19-47.

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:25 UTC

History

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

Hazard review

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

    Worst case: a route string carrying JSON-breaking bytes corrupts the payload and the shell rejects an otherwise valid verb - closed by jq -nc --arg encoding, which JSON-escapes the route unconditionally so any argv bytes arrive as a well-formed string payload; a route that is not a real menu id reaches the shell and surfaces as its own not-found handling on the plugin side. boundary: the case allowlist pins the five verbs plus help, with toggle/summon carrying payloads and close/refresh/ping the empty object - no verb/route combination builds a different call shape. error_handling is the declared class: exec replaces the process with omarchy-shell, so IPC failure surfaces as the client own exit status with no masking, retry, or swallow in this wrapper. Catalog 1.11.0 re-review: input_domain not applicable, it passes the route through as a JSON payload built by a JSON encoder. concurrency_scale not applicable, each CLI call execs one IPC call and keeps no state; the server side is stated on SW-REQ-260922-50RE.

  • propertyreviewedtotality

    Every argv resolves to exactly one exec shape - five verbs with their fixed call forms, help with exit 0, unknown verb to the SNZG diagnostic arm - so the wrapper is total with no argument combination left undefined.

  • structuralnot applicable

    jq --arg JSON encoding plus a case allowlist and exec; the route is never interpolated into a command string, only into a JSON payload field, and the verb never reaches a command name.

  • domainnot applicable

    A local session-bus IPC call to the user own shell instance with user-chosen route data; no network, crypto, or privilege boundary, and no authority moves that the called plugin does not already hold.

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-65

    Read omarchy-menu and BarWidget.qml. toggle, summon, close, refresh and ping each exec the matching omarchy-shell IPC call; toggle and summon pass the route as a JSON payload; help prints usage and exits 0. verb_known models the named-verb case arms; ipc_call_executed is the exec. 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 discharged

Browse the catalogue
Discharged

Behavior when operations fail or dependencies are unavailable.

Discharging evidence2/2 required witnessed
  • negativerequiredpresent
    Covered by 1 test
  • nominalrequiredpresent
    Covered by 1 test

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 verb_known the menu_dispatcher shall eventually satisfy ipc_call_executed

Witnesses· 3 scenarios total

  • menu-dispatcher-test.sh:1
    exercises 3 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.

Covereda test exercises this rowExempteda reviewed mcdc:ignoreNo-actionfalse-result row satisfied by designUncoveredneeds a covering test
#ipc_call_executedverb_knownResultProvesCovering test
1FFTverb_known
2FTFipc_call_executed
3TTTipc_call_executed

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
2
Tests
1
At-risk contracts
0

Files to re-check (2)

  • omarchy-menubin/omarchy-menu
  • BarWidget.qmlshell/plugins/menu/BarWidget.qml

Tests to re-run (1)

  • menu-dispatcher-test.shtest/shell.d/menu-dispatcher-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