Proof Portal
Omarchy
ProbeLabs74 findings · 94 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 lock service shall report the reader unavailable after 3 probe answers in a row that are neither a listed print nor a definite none.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
The lock service shall report the reader unavailable after 3 probe answers in a row that are neither a listed print nor a definite none. When the service treats fingerprint authentication as configured, 3 unusable attempts in a row shall also cause the report. A usable attempt shows a finger prompt and does not end in a device error within 2 s of the prompt. An attempt that shows a prompt clears the report. After a usable attempt, the service shall start the next attempt after 250 ms. After n unusable attempts, it shall wait 1 s times 2 to the power n-1, at most 40 s. It shall abort an attempt that shows no prompt within 20 s. It shall count a miss within 5 s after a resume as the first miss. It shall restart an attempt or a wait that spans a suspend within 250 ms. User activity shall shorten a longer wait to 250 ms. It shall do so at most once per 2 s or once per current wait, whichever is longer. At the 40 s cap, it shall do so only 32 s after the last attempt ended.
the lock_service shall always satisfy fingerprint_reader_unavailable <=> (probe_miss_streak_reached | (fingerprint_auth_configured & !attempt_usable & attempt_miss_streak_reached))
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
A reader that fprintd cannot claim, for example wedged after suspend or held by another client, made the lock screen retry every 250 ms. The retries continued while the screen stayed locked, and the user saw no sign. Upstream #7158 (FingerprintModel.js and Service.qml) backs off and leaves fprintd its 30 s idle exit, so a wedged claim can clear. It reports the reader unavailable after 3 misses, and the lock view crosses the icon out (SW-REQ-260912-41VV). It also restarts after a resume and stops a claim that never prompts.
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
- Claude Code · AI agent
- Reviewed
- Oct 4, 2026, 19:06 UTC
History
- Created
- Oct 4, 2026, 19:00 UTC · Claude Code · AI agent
- Modified
- Oct 4, 2026, 19:16 UTC · Claude Code · AI agent
Hazard review
- scenarioreviewederror_handlingboundaryedge_caseconcurrency_scale
Worst case: the lock screen hammers a wedged reader forever, or shows "Fingerprint reader unavailable" for a reader that works, or never retries after a resume. error_handling: a device error, a start failure or a claim with no prompt within 20 s is a miss and backs off. boundary: the notice needs 3 misses in a row; the backoff caps at 40 s, above fprintd's 30 s idle exit; a device error within 2 s of a prompt is a miss. edge_case: a miss inside the 5 s resume grace stays at the first tier; a clock stepped backwards counts neither as a sleep nor as an idle stretch. concurrency_scale: onError and onCompleted can both fire for one attempt and the attempt settles once; a nudge never starts a second attempt while one runs. input_domain not applicable: the inputs are timer ticks, PAM signals and wall-clock times. All model rows are witnessed in lock-fingerprint-retry-test.sh (replayed for code-level MC/DC) and the service rows in the lock harness.
- propertyreviewedmonotonicitydeterminism
monotonicity: the retry delay never shrinks while the miss streak grows (witnessed for streaks 1..20). determinism: the model functions depend only on their arguments.
- structuralreviewedoverflow_safety
overflow_safety: Math.pow(2, streak - 1) grows without bound for long outages but is clamped by Math.min to the 40 s cap before it reaches a timer (witnessed for streak 50).
- domainnot applicable
Timing and display state of the lock screen only; authentication itself stays with pam_fprintd.
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.
- Claude Code · AI agentApprovedSpec conformanceOct 4, 2026 · 14 hours agoREVIEW-261004-5V8C
Read shell/plugins/lock/Service.qml and FingerprintModel.js at upstream 035ce29f. fingerprintUnavailable is the binding isUnavailable(fingerprintProbeStreak) || (fingerprintConfigured && (!fingerprintAttemptReachedDevice || fingerprintAttemptFastError) && isUnavailable(fingerprintUnreachedStreak)), with isUnavailable(streak) = streak >= 3. fingerprintProbeStreak counts unknown probe answers and resets on a definitive one; fingerprintUnreachedStreak is advanced by settleFingerprintAttempt through nextStreak (0 after a usable attempt, 1 for a miss inside the resume grace, +1 otherwise). An attempt is usable when it reached the device (noteFingerprintReachedDevice on a non-error PAM message, which also stamps the prompt time) and did not end in a device error within FAST_ERROR_MS (2 s) of it, i.e. !(!reached || fastError). The binding is the formula term for term, so the three violation rows (probe streak reached but not reported, reported with neither streak, configured unusable streak reached but not reported) cannot occur and are dispositioned defensive. Witnesses in test/qml/lock/shell.qml on a real lock: a fresh lock with no misses (not reported); one or two misses against a reader that only sends an error message (not reported yet); three misses then a has-no-fingers answer (not reported once unconfigured); three misses then a reader that prompts, checked while the attempt is still in flight (the prompt clears the report).
Cited code (9)
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
the lock_service shall always satisfy fingerprint_reader_unavailable <=> (probe_miss_streak_reached | (fingerprint_auth_configured & !attempt_usable & attempt_miss_streak_reached))
Witnesses· 4 scenarios total
- stepWaitexercises 4 condition scenarios
MC/DC truth table· 7 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| # | attempt_miss_streak_reached | attempt_usable | fingerprint_auth_configured | fingerprint_reader_unavailable | probe_miss_streak_reached | Result | Proves | Covering test |
|---|---|---|---|---|---|---|---|---|
| 1 | F | F | F | F | F | T | fingerprint_reader_unavailable | |
| 2 | F | F | F | F | T | F | probe_miss_streak_reached | Exempted · defensive — fingerprintUnavailable is a binding whose first disjunct is FingerprintModel.isUnavailable(fingerprintProbeStreak) (streak >= 3), so it is true whenever the probe streak reached 3 (reviewed: REVIEW-261004-5V8C) |
| 3 | F | F | F | T | F | F | fingerprint_reader_unavailable | Exempted · defensive — the binding is exactly its two disjuncts; with the probe streak below 3 and fingerprint unconfigured both are false, so the reader cannot be reported unavailable (reviewed: REVIEW-261004-5V8C) |
| 4 | F | F | T | F | F | T | attempt_miss_streak_reached | |
| 5 | T | F | F | F | F | T | fingerprint_auth_configured | |
| 6 | T | F | T | F | F | F | attempt_miss_streak_reached | Exempted · defensive — the binding's second disjunct is fingerprintConfigured && (!fingerprintAttemptReachedDevice || fingerprintAttemptFastError) && isUnavailable(fingerprintUnreachedStreak), which holds here, so the binding is true (reviewed: REVIEW-261004-5V8C) |
| 7 | T | T | T | F | F | T | attempt_usable |
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 (2)
- FingerprintModel.jsshell/plugins/lock/FingerprintModel.js
- Service.qmlshell/plugins/lock/Service.qml
Tests to re-run (2)
- fingerprintmodel-replay.test.mjstest/node/fingerprintmodel-replay.test.mjs
- shell.qmltest/qml/lock/shell.qml
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.