Proof Portal

Sign in
Project overview

Omarchy

ProbeLabs73 findings · 87 requirements

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.

Audit history

Run · 7916138

Audited Sep 29, 2026, 09:44 AM on pr/13255.

Partial19 warnings
79/79 realizable81/81 meet policyverification complete: 0

as of 7916138 · Sep 29, 2026 · pr/13255

Run context
What was audited, and where.
Branchpr/13255
Commit7916138
RecordedSep 29, 2026, 09:44 AM
Tags—
View project as of this runCompare to base branch
Checks
This run's recorded check results. Detail links open the current audit, so they are shown as read-only here.
  • acceptance_criteria_witnessedWarn3 testable acceptance criteria across 2 stakeholder req(s) witnessed (0 via direct acceptance test, 3 deferred (tracked)) — deferred ACs are tracked debt, not a pass
  • acceptance_witness_qualityPassno :acceptance tags share a test carrier with a derived SYS/SW/INT witness
  • accepted_risks_reviewedPassno active accepted risks
  • ambiguity_reviewedPass0 ambiguous pairs (1980 pairs checked)
  • annotation_validityPassall referenced requirement IDs and obligation annotations match current spec files
  • approval_motivation_presentPassall 0 approved requirement(s) carry valid motivation (or are initial-creation exemptions)
  • approvals_currentPassapproval policy disabled
  • approved_guarantee_ki_conflictPassno approved guarantee conflicts with an unacknowledged open known issue
  • assumptions_statusPassno active assumptions
  • authored_delta_expectedPassall traced production implementation files have current no-authored-change reviews
  • autolink_cleanPass0 autolink errors
  • behavioral_implications_verifiedPassno variables with Z3-backed properties or constraints to verify
  • build_matrix_completeSkipno build_targets declared (build matrix check opt-in)
  • build_passesPassfor f in bin/omarchy-apply-lock bin/omarchy-system-lock bin/omarchy-update-lock bin/omarchy-hyprland-session-locked bin/omarchy-system-sleep-lock bin/omarchy-menu bin/omarchy-menu-select bin/omarchy-menu-input bin/omarchy-menu-plugin bin/omarchy-menu-share bin/omarchy-menu-timezone bin/omarchy-menu-file bin/omarchy-menu-emoji-insert; do /usr/bin/bash -n "$f" || exit 1; done; node --check shell/plugins/menu/MenuModel.js (ok)
  • catalog_completenessPasscatalog/obligation/signal/requirement set is internally consistent (18 obligation_class(es) declared, 325 catalog class(es) loaded)
  • catalog_semantic_bindings_reviewedPassno semantic-scan artifact
  • catalog_version_pinnedPasscatalog version 1.10.1 in use; no pin configured (set project.catalog.version in proof.yaml for auditor-stable upgrades)
  • change_evidence_completePassno in-branch changed files to gate for change evidence
  • change_record_landsPassall 1 affects: entries land in a matching verification.review.motivation
  • changed_requirements_reviewedPasschanged requirement review skipped (no git diff context)
  • circular_deps_cleanPass0 circular dependencies
  • code_mcdc_coveragePasscode-level MC/DC meets configured thresholds (aggregate decisions 41.4%, conditions 45.3%, 28 incomplete functions) (10 ignored decisions)
  • code_mcdc_measurePasscode-level MC/DC evidence available for: bash, js
  • code_predicates_modeledWarn2 unmodeled code predicate site(s) across 65 implemented FRETish requirement(s)
  • code_signal_deadline_cast_unreviewedPassno proof/signals directory (deadline-cast signal hunt no-op)
  • code_signal_obligations_reviewedPass4 code signal(s) across 4 source artifact(s); explicit signal obligations covered or explicitly resolved
  • code_signal_suppressions_reviewedPassno project signal suppressions declared
  • code_signal_unbindablePass4 code signal(s) across 4 source artifact(s); no proposes_class declarations are unbindable
  • concern_adjudicatedPassno concerns directory (concern adjudication no-op)
  • consistency_pair_coverageWarn4 of 4 components with >=2 formalized guarantees have zero checkable consistency pairs and no recorded justification (0 attested)
  • contract_alignment_cleanPasspublic command surfaces have aligned requirement/help/test coverage
  • coverage_metPass100% coverage (22/22)
  • coverage_thresholdPassno requirements with coverage data to check
  • cross_component_cleanPass0 cross-component reqs fully covered
  • cross_level_completePass100% cross-level coverage (2/2)
  • cross_spec_consistency_cleanPass0 cross-spec contradictions (0 pairs checked)
  • cvss_severity_consistentPass0 CVSS-carrying known issue(s) label at or above their own vector band (or carry a reviewer-stamped severity_bound)
  • data_constraint_z3_coveragePassno variables with Z3-backed properties or constraints to check
  • data_constraints_completePassno variables with Z3-backed properties or constraints to verify
  • decomposition_reviewedPass0/0 decompositions complete; 14 parent(s) state their own verified claim and are refined, not decomposed
  • defect_review_currentInfo3 no-stamp, 11 stale, 1/15 specs: claim-reviewed, 0 verified, 0 promoted, 0 dismissed
  • deletion_without_retirementPassno baseline available, skipping
  • deployment_tvl_verifiedPassproject is not Web3/DeFi — deployment_tvl_verified skipped (enable via checks.deployment_tvl_verified.enabled: true)
  • description_delta_reviewedPassno changed requirements in current branch
  • description_grammar_enumeration_completeSkipdisabled by project.checks policy
  • differential_conformancePassno differential fixtures under proof/fixtures/ (author one with schema proof.fixtures/v1)
  • disclosure_safePassno active known issues carry a `private` or under-embargo disclosure
  • documentation_coverageSkipdisabled by project.checks policy
  • documentation_enforcedPassdocumentation.enforce_sources not configured (check disabled)
  • documented_claim_verifiedSkipno documented_behaviors declared (documented claim evidence check opt-in)
  • dual_path_guards_equivalentSkipno dual-path rules declared in proof/dual-path-rules/ or project.dual_path_rules (dual-path guard check opt-in)
  • evidence_diversityPassevidence diversity policy disabled
  • failing_test_blocks_approvalPassno approved requirement is witnessed only by a failing or skipped test
  • fixture_staleness_cleanPassno components declare fixture-backed evidence -- fixture staleness not applicable
  • flip_fixtures_existPassno components declare fixture-backed evidence -- FLIP fixtures not applicable
  • flip_test_alignmentPassno components declare fixture-backed evidence -- FLIP test alignment not applicable
  • formalization_lemma_verdict_consistencyPassno SYS-REQ claims formalization_status=valid with a LEMMA: trace or verifies: annotation
  • fuzz_evidence_carrier_validPassno :fuzz annotations in scope
  • gaps_cleanWarn6 unconstrained outputs
  • high_severity_obligation_without_vectorPassno high/critical ObligationHazards on active requirements
  • high_severity_reproducer_gradePassno active high/critical-severity or security-relevant (cve_surface possible/likely/confirmed) known issue requires a reproducer-grade gate
  • integration_evidence_witnessedPassno active integration requirements to witness
  • interface_contract_duplicatesPass0 duplicate interface contracts
  • interface_coverageWarn2 interface coverage gaps (2 components without interfaces, 0 interfaces without reqs, 0 broken references)
  • interface_formalization_completePassno configured cross-component specs require FRETish formalization
  • interface_staleness_cleanPass0 interface contracts checked, 0 stale
  • known_issue_affected_requirements_presentPass1 active known issue(s) name the requirement(s) they violate (or carry a reviewer-stamped requirement_exemption)
  • known_issue_closure_platform_boundSkipno known issue declares `platforms:` (platform-bound closure check opt-in)
  • known_issue_completeWarn1 of 1 active known issue(s) below the quality floor (1 stale/invalid evidence; 1 total gap(s)) — see `proof help known_issue_complete` (full per-category breakdown in the check metadata / --format json)
  • known_issue_mirror_anchor_relevantPass0 active known issue(s) with a declared mirror anchor have affected_requirements that fall inside that mirror's scope (or resolve to no scope / are waived)
  • known_issue_platform_coverageSkipno build_targets declared (platform coverage check opt-in)
  • known_issue_poc_quality_effectivePass0 high/critical known issue(s) with a poc_quality block satisfy every applicable rule (or carry a reviewer-stamped poc_quality_exemption)
  • known_issue_recheck_duePassno known issues are overdue for upstream re-check
  • known_issue_reproducer_consistentPass1 active known issue(s) with a bound reproducer assert the secure contract or declare a characterization (no reproducer contradicts its finding)
  • known_issue_reproducer_present_and_resolvesPass1 active known issue(s) carry a runnable reproducer (a resolving test selector, a runnable command, or a `// Reproduces:` annotation) or a reviewer-stamped poc_presence_exemption
  • known_issue_security_remediation_presentPass0 security-relevant known issue(s) document a remediation or mitigation (or carry a reviewer-stamped remediation_exemption)
  • known_issue_severity_prose_consistentPass0 known issue(s) with a prose severity grade match their structured severity field (or carry a reviewer-stamped severity_bound)
  • known_issue_sibling_dispositionPass1 known issue(s); none fixed with template_class, kill_domain, or isomorphic_sites to checklist
  • known_issue_template_transferPass1 open known issue(s) meet template-transfer hygiene
  • known_issues_reviewedPass1 active known issue(s) visible (review interval 90 day(s))
  • l0_stakeholder_completePass2 STK-REQs fully structured (persona, story, acceptance criteria with derived_reqs)
  • l1_system_completePass14 SYS-REQs fully linked and described
  • l2_software_completePass65 SW/INT-REQs fully linked to SYS-REQs
  • lemma_branch_coverageSkip0 reqproof:lemma annotations in project — coverage not applicable until lemmas are authored
  • levels_connectedPassall 3 spec levels connected (L0:2, L1:14, L2:65)
  • lint_cleanPass142 untraced function(s): 142 owned by orphan_code_clean, 0 owned by orphan_tests_clean, 0 unowned — this roll-up adds no finding of its own; fix them under their owning check
  • mcdc_coveragePass79 requirements checked, 295 witness rows total, 0 uncovered
  • mcdc_ignore_classifiedPassall 10 code-level //mcdc:ignore annotation(s) are classified; capability-gap ignores reference an open KnownIssue with a failing tripwire; honored witness-row exemptions are categorized
  • mcdc_known_issue_disposition_stalePassno KI-gated MC/DC or obligation disposition has outlived its fixed bug
  • mcdc_verifies_witnessesPassmcdc verifies witness enforcement disabled
  • mcdc_witness_drives_codePassall MC/DC witness tests reference product code and configured outcome-variable code
  • mirror_completePassno mirrors declared (declare one with `proof mirror add` when starting a refactor/port)
  • mirror_stalePassno mirrors declared (declare one with `proof mirror add` when starting a refactor/port)
  • negative_path_witness_requiredPass0 security-classed requirement(s) carry a negative-path witness
  • no_authored_change_surface_reviewedSkipdisabled by project.checks policy
  • nonbool_inputs_constrainedPassno non-bool input/mode variables across 3 formalized components — every modeled input is a boolean. If any component handles quantitative values (sizes, timeouts, costs, status codes, rates), declaring them as range:/data_constraint variables unlocks Z3 verification, boundary testing, and partition evidence. See: proof help domain-modeling
  • obligation_baselinePass0 requirement(s) have all 0 baseline obligation(s) resolved
  • obligation_completenessPass2 stakeholder obligation checklist(s) fully covered
  • obligation_decomposition_completeWarn30 obligation(s) on 23 requirement(s) covered by satisfying children, 1 deferred (tracked) — deferred obligations are tracked debt, not a pass
  • obligation_delegation_resolvesPassno obligation_delegations declared
  • obligation_enforcement_backedPassall 30 cataloged obligation checklist item(s) have signal-rule or evidence backing
  • obligation_evidence_completeWarn42 covered, 1 deferred (tracked) — deferred obligations are tracked debt, not a pass
  • obligation_profile_evidence_completePassno evidence profiles configured
  • obligation_suppression_rationalePassall 5 obligation suppression rationale(s) meet the 32-char minimum
  • obligation_suppression_reviewerPassno obligation suppressions at or above reviewer-required severity
  • obligation_witness_groundedPass32 witness(es): 0 grounded (static), 0 cleared (coverage), 0 exempt; 8 witness(es) coverage-unavailable (advisory)
  • orphan_code_cleanWarn142 code functions have no requirement annotation
  • orphan_tests_cleanPass35 test functions scanned, 0 orphans
  • partition_evidence_completePassno input data-constraint partitions require runtime evidence
  • poc_quality_checkedWarn1 of 1 in-scope known issue(s) (at or above medium severity, or being submitted) have PoC quality gaps (1 missing block, 0 failed rule(s)). ACC-15.
  • problem_report_class_mitigation_evidencePass1 mitigated report(s) all carry class-mitigation evidence
  • problem_reports_reviewedPass1 problem report(s) reviewed; all dispositioned
  • process_checklistWarnprocess_checklist: incomplete onboard_v1 (14 pending, 3 not-applicable (new-project onboarding and adoption-gated steps auto-skipped)) — next: traces-light — Light code↔spec graph (Implements/Documents) (role: onboard) — run: proof checklist show onboard_v1 (proof help process-checklists)
  • proof_complexity_cleanWarn1 proof complexity budget overruns across 1 components
  • property_based_test_coverageWarn17 function(s) pending property-based test evaluation
  • property_fixtures_existPassno components declare fixture-backed evidence -- property fixtures not applicable
  • quality_cleanPassall 81 requirements passed quality checks
  • residual_kill_hygienePass1 residual(s) pass kill hygiene
  • retired_cleanupPassno retired/superseded requirements
  • role_prompt_hygienePassno empty-is-win or finding-quota language in 47 role(s)
  • role_references_resolvePassall role references resolve (47 built-in + 0 project-local role(s) checked)
  • security_relevance_consistentPass0 security-named known issue(s) carry a CVSS vector + non-none cve_surface (or a reviewer-stamped security_relevance_justification)
  • security_surface_coveredSkipdisabled by project.checks policy
  • signal_fixtures_validSkipdisabled by project.checks policy
  • slow_tests_cleanSkipslow-test audit enabled but test-results artifact is not configured
  • software_formalization_completePassall 16 review or approved guarantee requirement(s) in 1 configured lower formal-layer spec(s) have a non-envelope FRETish formalization
  • solver_latency_cleanPass0 slow solver-backed components over 1m0s
  • solver_modeling_opportunityPassno modeling opportunities: 79 formalized requirements evaluated, 3 carried enumerable-domain signals, all with modeled or waived domains (0 waived, 0 with recorded reasons, 3 suppressed by bool-only gate). See: proof help domain-modeling
  • spec_lint_ac_inverse_coveragePasslint-ac-inverse-coverage: no issues found
  • spec_lint_ac_subset_of_satisfiesPasslint-ac-subset-of-satisfies: no issues found
  • spec_lint_acceptance_review_currentPasslint-acceptance-review-current: no issues found
  • spec_lint_annotation_vs_authoredPasslint-annotation-vs-authored: no issues found
  • spec_lint_assumption_dispositionPasslint-assumption-disposition: no issues found
  • spec_lint_audit_ignore_reasonPasslint-audit-ignore-reason: no issues found
  • spec_lint_auto_modifier_without_humanPasslint-auto-modifier-without-human: no issues found
  • spec_lint_circularity_self_citationPasslint-circularity-self-citation: no issues found
  • spec_lint_complementary_flags_uninteractedPasslint-complementary-flags-uninteracted: no issues found
  • spec_lint_data_constraint_parseablePasslint-data-constraint-parseable: no issues found
  • spec_lint_decomposition_adds_refinementPasslint-decomposition-adds-refinement: no issues found
  • spec_lint_degenerate_input_obligation_missingPasslint-degenerate-input-obligation-missing: no issues found
  • spec_lint_evidence_tag_existsPasslint-evidence-tag-exists: no issues found
  • spec_lint_exemplar_missing_on_newInfolint-exemplar-missing-on-new: 56 advisory notice(s)
  • spec_lint_formalization_qualityPasslint-formalization-quality: no issues found
  • spec_lint_fretish_bare_responsePasslint-fretish-bare-response: no issues found
  • spec_lint_fretish_tautologyPasslint-fretish-tautology: no issues found
  • spec_lint_governance_yaml_data_pathsPasslint-governance-yaml-data-paths: no issues found
  • spec_lint_hallucinated_symbolsPasslint-hallucinated-symbols: no issues found
  • spec_lint_hazard_consequenceInfolint-hazard-consequence: 80 advisory notice(s)
  • spec_lint_hazard_review_currentWarnlint-hazard-review-current: 3 issue(s)
  • spec_lint_id_shape_canonicalPasslint-id-shape-canonical: no issues found
  • spec_lint_inline_impact_review_driftPasslint-inline-impact-review-drift: no issues found
  • spec_lint_ki_attacker_coherencePasslint-ki-attacker-coherence: no issues found
  • spec_lint_ki_banned_markersInfolint-ki-banned-markers: 1 advisory notice(s)
  • spec_lint_ki_history_chronologyPasslint-ki-history-chronology: no issues found
  • spec_lint_ki_open_actionabilityPasslint-ki-open-actionability: no issues found
  • spec_lint_ki_prose_shapePasslint-ki-prose-shape: no issues found
  • spec_lint_ki_stale_status_refsPasslint-ki-stale-status-refs: no issues found
  • spec_lint_mediation_contract_contradictedSkipdisabled by project.checks policy
  • spec_lint_na_denies_property_enforced_unevenlySkipdisabled by project.checks policy
  • spec_lint_na_denies_property_the_code_managesSkipdisabled by project.checks policy
  • spec_lint_numbering_gaps_has_tombstonePasslint-numbering-gaps-has-tombstone: no issues found
  • spec_lint_obligation_checklist_emptyPasslint-obligation-checklist-empty: no issues found
  • spec_lint_obligation_coverage_gapPasslint-obligation-coverage-gap: no issues found
  • spec_lint_operational_invariant_varPasslint-operational-invariant-var: no issues found
  • spec_lint_parent_field_vs_satisfiesPasslint-parent-field-vs-satisfies: no issues found
  • spec_lint_pinned_delimiter_undispositionedPasslint-pinned-delimiter-undispositioned: no issues found
  • spec_lint_plan_of_record_currentPasslint-plan-of-record-current: no issues found
  • spec_lint_prose_ste100Warnlint-prose-ste100: 87 issue(s)
  • spec_lint_reject_combination_composition_witnessedPasslint-reject-combination-composition-witnessed: no issues found
  • spec_lint_req_type_vs_descriptionPasslint-req-type-vs-description: no issues found
  • spec_lint_review_cadence_currentPasslint-review-cadence-current: no issues found
  • spec_lint_satisfies_target_retiredPasslint-satisfies-target-retired: no issues found
  • spec_lint_shared_state_rebuildPasslint-shared-state-rebuild: no issues found
  • spec_lint_source_doc_hedgingPasslint-source-doc-hedging: no issues found
  • spec_lint_source_native_yaml_tracePasslint-source-native-yaml-trace: no issues found
  • spec_lint_spec_conformance_review_groundedPasslint-spec-conformance-review-grounded: no issues found
  • spec_lint_status_vs_reviewPasslint-status-vs-review: no issues found
  • spec_lint_sw_informal_witnessedPasslint-sw-informal-witnessed: no issues found
  • spec_lint_threat_surface_presentPasslint-threat-surface-present: no issues found
  • spec_lint_trace_review_evidence_currentPasslint-trace-review-evidence-current: no issues found
  • spec_lint_unjoined_effect_halvesPasslint-unjoined-effect-halves: no issues found
  • spec_lint_yaml_escape_artefactPasslint-yaml-escape-artefact: no issues found
  • srs_generatesPassSRS generates successfully
  • srs_no_uncheckedPassall requirements checked
  • stakeholder_acceptance_criteriaPass2 stakeholder reqs all have acceptance criteria with derived_reqs
  • stakeholder_requirements_existPass2 stakeholder requirements found
  • submission_validatedPassno active known issue has been reported externally (submission / upstream_report block) or marked for submission (disposition)
  • surface_coverageWarnsurface_coverage: 1 GAP / 0 dual-surface-GAP / 0 dual-surface-residual of 1 surface(s) (ok=0 debt=0) — recommended: proof role show surface-close --format agent (then re-audit); proof help surface_coverage
  • suspect_cleanWarn193 suspect links
  • sys_has_software_childPass14 SYS-REQ(s) have a downward realization (SW-REQ child, implementing code, or verifying tests)
  • system_formalization_completePassall 14 SYS-REQs formalized in FRETish
  • system_requirements_linkedPass14/14 linked to stakeholder reqs
  • table_completePassno decision tables declared (domain.tables in <component>.vars.yaml); nothing to check. If any component has lookup-table or enum*action behavior (permission matrices, per-role/per-state surfaces, status transitions), declaring it under domain.tables enables completeness/consistency/equivalence checking. See: proof help domain-modeling
  • table_consistentPassno decision tables declared (domain.tables in <component>.vars.yaml); nothing to check. If any component has lookup-table or enum*action behavior (permission matrices, per-role/per-state surfaces, status transitions), declaring it under domain.tables enables completeness/consistency/equivalence checking. See: proof help domain-modeling
  • table_equivalencePassno decision tables declared (domain.tables in <component>.vars.yaml); nothing to check. If any component has lookup-table or enum*action behavior (permission matrices, per-role/per-state surfaces, status transitions), declaring it under domain.tables enables completeness/consistency/equivalence checking. See: proof help domain-modeling
  • test_command_propagates_failurePass3 configured test command(s) propagate their real failure exit code
  • tests_passPassall tests passed
  • trusted_outputs_from_untrusted_inputsPassno untrusted-input dataflows into trusted outputs: 79 formalized requirements evaluated, 0 in safety/financial scope, all sourced from trusted or sanitized data (0 waived, 0 with recorded reasons)
  • under_modeled_requirements_cleanWarn2 requirement/family finding(s) likely under-modeled relative to current tests or implementation
  • unresearched_p0_vectorsPass1 vector(s); no P0 unresearched campaigns
  • vacuity_cleanPass0 vacuity findings across 79 eligible requirements
  • validate_passesPass85/85 valid
  • variable_driftPass1 requirement(s) have a variables: list consistent with their FRETish
  • variable_orphans_cleanWarn12 variable model issues (12 declared-unused, 0 undeclared-used)
  • variables_declaredPass4 formalized components passed solver preflight
  • vector_campaign_closurePass1 vector(s) satisfy campaign closure (1 terminal; 0 evidence-bound; 0 KI-owned; 0 deferred-by-config)
  • vector_campaign_hygienePass1 vector(s) pass campaign hygiene
  • verification_chain_completePass14/14 verification chains complete
  • verification_plan_evidencePassno requirements carry a verification_strategy
  • verification_scope_completePassdeclared scope covers all 27 declared production source file(s)
  • verification_state_consistentPass81 requirement(s) evaluated — all agree with the derived proposal
  • verify_passesWarnverify: 0 failing steps, 2 warning steps
  • waivers_reviewedPassno active waivers
  • z3_cross_layer_consistencyPassno comparable parent-child data-constraint partitions
  • z3_properties_verifiedPassno variables with Z3-backed properties or constraints to verify