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.
When the lock screen's enrollment probe finishes, the lock service shall classify the answer.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
When the lock screen's enrollment probe finishes, the lock service shall classify the answer. It shall treat fingerprint authentication as configured when the answer lists an enrolled fingerprint. It shall treat it as not configured when the answer says that the user has none. The same applies when the fingerprint PAM file or fprintd-list is missing. Any other answer shall leave the state unchanged, for example when the service cannot reach fprintd. While fingerprint authentication stays unconfigured after such an answer, the service shall run the probe again after the attempt backoff.
when fingerprint_probe_answered the lock_service shall always satisfy fingerprint_auth_configured <=> (probe_lists_print | (!probe_says_none & fingerprint_was_configured))
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
The lock screen's probe used to search the fprintd-list answer for the word "finger". An empty enrollment on a reader with Fingerprint in its name then read as enrolled (KI-LOCK-FPRINT-PROBE-FAIL-OPEN). A probe that could not reach fprintd read as not enrolled and switched fingerprint authentication off. Upstream #7158 classifies the answer in FingerprintModel.classifyProbe and Service.applyFingerprintProbe. Only a listed print or a definite none changes the state. The service asks again about an unknown answer, with the attempt backoff.
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_handlingboundarymalformed_input
Worst case: the lock screen offers a fingerprint path that can never succeed, or drops a working one because fprintd was briefly unreachable. error_handling: an unreachable fprintd, a D-Bus timeout or empty output read unknown and keep the state; while unconfigured the probe reruns after 1 s, 2 s, ... capped at 40 s (witnessed in lock-fingerprint-retry-test.sh and the lock harness). boundary: a print row must start a line and carry a numeric index; "no" and "has no fingers enrolled" read none. malformed_input: null, empty or garbled output reads unknown. input_domain not applicable: the probe output comes from the packaged fprintd-list run with LC_ALL=C for the session user. concurrency_scale not applicable: one probe process at a time (the running guard).
- propertyrevieweddeterminismtotality
determinism: classifyProbe depends only on the answer text. totality: every answer maps to yes, no or unknown.
- structuralnot applicable
Two regular expressions and a string compare on decoded text.
- domainnot applicable
Reads the session user's own enrollment through the packaged probe; no trust boundary is crossed.
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 · 15 hours agoREVIEW-261004-D4AD
Read shell/plugins/lock/Service.qml and FingerprintModel.js at upstream 035ce29f. The probe process runs LC_ALL=C fprintd-list "$USER" when the fingerprint PAM file and fprintd-list exist and prints no otherwise; its exit hands the raw answer to applyFingerprintProbe. classifyProbe returns yes when any line is a " - #N:" row, no when the trimmed answer is exactly no or contains has no fingers enrolled, and unknown for anything else; the yes test runs first. applyFingerprintProbe returns on unknown before touching fingerprintConfigured (counting a probe miss and, while locked and unconfigured, arming the paced recheck); on yes or no it assigns fingerprintConfigured = (status === yes). So fingerprint_auth_configured after an answer is probe_lists_print, or the previous value when the answer is neither a print nor a none, exactly the formula. The four violation rows need that order or the early return removed and are dispositioned defensive. Witnesses in test/qml/lock/shell.qml, all on a real lock with the fprintd-list stub printing the real answers: an unreachable fprintd while unconfigured (stays off, probe streak 1, recheck at 1 s); a has-no-fingers answer after a listed print (turns off and stops attempts); a two-reader answer with a print on one and none on the other while configured (stays on); and a no-answer window proved by the probe-exit counter (no-action row).
Cited code (7)
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
when fingerprint_probe_answered the lock_service shall always satisfy fingerprint_auth_configured <=> (probe_lists_print | (!probe_says_none & fingerprint_was_configured))
Witnesses· 4 scenarios total
- stepWaitexercises 4 condition scenarios
MC/DC truth table· 8 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| # | fingerprint_auth_configured | fingerprint_probe_answered | fingerprint_was_configured | probe_lists_print | probe_says_none | Result | Proves | Covering test |
|---|---|---|---|---|---|---|---|---|
| 1 | F | T | F | F | F | T | fingerprint_was_configured | |
| 2 | F | T | T | F | F | F | fingerprint_was_configured | Exempted · defensive — applyFingerprintProbe returns before it assigns fingerprintConfigured when classifyProbe answers unknown and fingerprint is configured, so an answer that is neither a listed print nor a none cannot clear it (reviewed: REVIEW-261004-D4AD) |
| 3 | F | T | T | F | T | T | probe_says_none | |
| 4 | F | T | T | T | T | F | fingerprint_auth_configured | Exempted · defensive — classifyProbe tests for a ' - #N:' row before either none answer, so an answer that lists a print classifies yes even when another reader has none, and the service sets fingerprintConfigured to true (reviewed: REVIEW-261004-D4AD) |
| 5 | T | F | F | F | F | T | fingerprint_probe_answered | |
| 6 | T | T | F | F | F | F | fingerprint_probe_answered | Exempted · defensive — an unknown answer while unconfigured returns before fingerprintConfigured is assigned, so it stays false (reviewed: REVIEW-261004-D4AD) |
| 7 | T | T | T | F | T | F | probe_lists_print | Exempted · defensive — a none answer with no listed print classifies no, and the service assigns fingerprintConfigured = (status === "yes"), which is false (reviewed: REVIEW-261004-D4AD) |
| 8 | T | T | T | T | T | T | fingerprint_auth_configured |
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.