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 the user locks the session, the system shall engage the session lock through the shell IPC.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
When the user locks the session, the system shall engage the session lock through the shell IPC. The system shall reset the keyboard layout to the default. The system shall stop the ttfx screensaver and wait for it to exit before closing its terminal. The system shall lock 1Password when it is running.
when user_lock_requested the lock_component shall eventually satisfy session_lock_engaged & keyboard_layout_default & screensaver_stopped
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
bin/omarchy-system-lock is the user-facing lock entry point. It delegates the lock to the Quickshell lock plugin and cleans up interactive session state. Nominal floor: this guarantee is the positive-path lock engagement. STK-REQ-260912-XJ5D AC-001 exercises it. This child carries the nominal obligation class for the stakeholder checklist.
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 Dogfood · AI agent
- Reviewed
- Sep 12, 2026, 23:50 UTC
History
- Created
- Sep 12, 2026, 19:42 UTC · Kimi Dogfood · AI agent
- Modified
- Sep 30, 2026, 13:58 UTC · Leonid Bugaev
Hazard review
- scenarioreviewederror_handlingconcurrentboundaryconcurrency_scale
Parent-level partitions carried by satisfying children: error_handling via J8SX (missing-pam refusal path) and MXQG (best-effort signal absorption), concurrent via ND55 (timer versus in-flight authentication) and MXQG (async SIGTERM exit), boundary via 41VV and WBS3 (configured and overflow thresholds) and MXQG (1s wait cap). No obligation is held at this level alone. Catalog 1.11.0 re-review: input_domain not applicable, it reads no external text input. concurrency_scale applied, lock requests from the menu, keybindings and suspend can overlap; one engaged lock must result.
- propertynot applicable
Decomposition-level statement; totality and the no-feedback-loop idempotence are recorded on child WBS3 where the code lives.
- structuralnot applicable
Decomposition-level statement over one bash script plus QML view and service; structural surfaces are recorded at the child level.
- domainnot applicable
In-process lock component plus local IPC; no domain class applies_when fires at this level.
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 Dogfood · AI agentApprovedSpec conformanceSep 12, 2026 · 3 weeks agoREVIEW-16
System-level formula matches the script: omarchy-shell lock engages the session lock first, hyprctl switchxkblayout all 0 resets the layout, and the ttfx/screensaver stop follows; all three response conjuncts are attempted on every lock request, matching session_lock_engaged & keyboard_layout_default & screensaver_stopped.
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.
- HighOpen
Lock engages when password PAM disappears during the stabilize window; the stranded watchdog stands down
KI-LOCK-PAM-FLIP-ENGAGES-LOCK
- MediumOpen
Lock-service fingerprint probe fail-open: substring grep treats zero-enrollment fprintd-list output as configured
KI-LOCK-FPRINT-PROBE-FAIL-OPEN
- MediumReviewed
Compositor-side lock loss with a request outstanding is treated as a finished unlock; no re-lock
KI-LOCK-SPONTANEOUS-UNLOCK-FAIL-OPEN
- LowReviewed
Failed/empty readlink result stored as backgroundPath, wiping a good lock-screen wallpaper
KI-LOCK-EMPTY-READLINK-WIPES-WALLPAPER
- LowReviewed
fingerprintPam.start() returning false disables fingerprint auth for the rest of the lock with no retry
KI-LOCK-FPRINT-START-FAIL-NO-RETRY
- LowOpen
Abnormal PAM error increments failedAttempts twice (onError and onCompleted both run handlePasswordFailure)
KI-LOCK-PAM-ERROR-DOUBLE-COUNT
- LowReviewed
In-place video wallpaper overwrite during a running poster job keeps the stale poster frame
KI-LOCK-STALE-POSTER-INPLACE-OVERWRITE
Obligations
What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.
2 obligations · 2 discharged
Browse the catalogueEvidence tagged via <REQ> is witnessed by a requirement that satisfies this one — normal for stakeholder / aggregate requirements, which are proven through the requirements that refine them.
Behavior when operations fail or dependencies are unavailable.
- negativerequiredpresentCovered by 1 test
- nominalrequiredpresentCovered by 1 test
Happy-path behavior with valid inputs.
- nominalrequiredpresentCovered 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).
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 user_lock_requested the lock_component shall eventually satisfy session_lock_engaged & keyboard_layout_default & screensaver_stopped
Witnesses· 5 scenarios total
- system-lock-test.sh:1exercises 5 condition scenarios
MC/DC truth table· 6 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| # | keyboard_layout_default | screensaver_stopped | session_lock_engaged | user_lock_requested | Result | Proves | Covering test |
|---|---|---|---|---|---|---|---|
| 1 | F | F | F | F | T | user_lock_requested | |
| 2 | F | F | F | T | F | user_lock_requested | — |
| 3 | F | T | T | T | F | keyboard_layout_default | |
| 4 | T | F | T | T | F | screensaver_stopped | |
| 5 | T | T | F | T | F | session_lock_engaged | |
| 6 | T | T | T | T | T | keyboard_layout_default |
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.
7 open · 0 resolved
- HighOpen
Lock engages when password PAM disappears during the stabilize window; the stranded watchdog stands down
KI-LOCK-PAM-FLIP-ENGAGES-LOCK
- MediumOpen
Lock-service fingerprint probe fail-open: substring grep treats zero-enrollment fprintd-list output as configured
KI-LOCK-FPRINT-PROBE-FAIL-OPEN
- MediumReviewed
Compositor-side lock loss with a request outstanding is treated as a finished unlock; no re-lock
KI-LOCK-SPONTANEOUS-UNLOCK-FAIL-OPEN
- LowReviewed
Failed/empty readlink result stored as backgroundPath, wiping a good lock-screen wallpaper
KI-LOCK-EMPTY-READLINK-WIPES-WALLPAPER
- LowReviewed
fingerprintPam.start() returning false disables fingerprint auth for the rest of the lock with no retry
KI-LOCK-FPRINT-START-FAIL-NO-RETRY
- LowOpen
Abnormal PAM error increments failedAttempts twice (onError and onCompleted both run handlePasswordFailure)
KI-LOCK-PAM-ERROR-DOUBLE-COUNT
- LowReviewed
In-place video wallpaper overwrite during a running poster job keeps the stale poster frame
KI-LOCK-STALE-POSTER-INPLACE-OVERWRITE
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
Requirements (5)
- When fingerprint authentication is available, the lock view…lock · SW
- When the lock IPC handler receives a lock request and…lock · SW
- When the user locks the session and the ttfx screensaver is…lock · SW
- When the idle blank timer expires during a locked session,…lock · SW
- When entered password text exceeds the field width, the…lock · SW
Files to re-check (3)
- omarchy-system-lockbin/omarchy-system-lock
- LockView.qmlshell/plugins/lock/LockView.qml
- Service.qmlshell/plugins/lock/Service.qml
Tests to re-run (5)
- system-lock-test.shtest/shell.d/system-lock-test.sh
- lock-fingerprint-indicator-test.shtest/shell.d/lock-fingerprint-indicator-test.sh
- lock-missing-pam-test.shtest/shell.d/lock-missing-pam-test.sh
- lock-blank-fingerprint-test.shtest/shell.d/lock-blank-fingerprint-test.sh
- lock-password-overflow-test.shtest/shell.d/lock-password-overflow-test.sh
What this rests on
Parent requirements (1)
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.