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 · e797ba5

Audited Sep 30, 2026, 11:40 PM on quattro.

Partial2 warnings
88/88 realizable90/90 meet policyverification complete: 3

as of e797ba5 · Sep 30, 2026 · quattro

Run context
What was audited, and where.
Branchquattro
Commite797ba5
RecordedSep 30, 2026, 11:40 PM
Tags—
View project as of this runCompare to previous in streamCompare 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_witnessedPass3 testable acceptance criteria across 2 stakeholder req(s) witnessed (3 via direct acceptance test)
  • 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 (2556 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 pin "1.10.1" matches shipped 1.10.1 (policy=manual)
  • change_evidence_completePassevery in-branch-changed change-typed review has complete backing evidence
  • change_record_landsPassall 3 affects: entries land in a matching verification.review.motivation
  • changed_requirements_reviewedPass1 changed requirements are beyond draft
  • circular_deps_cleanPass0 circular dependencies
  • code_mcdc_coveragePasscode-level MC/DC meets configured thresholds (aggregate decisions 100.0%, conditions 100.0%, 0 incomplete functions) (63 ignored decisions)
  • code_mcdc_measurePasscode-level MC/DC evidence available for: bash, js, qml
  • code_predicates_modeledPassall load-bearing code predicates on 73 implemented FRETish requirement(s) are modeled or explicitly not_modeled (66 empty-decision mutex leaf/leaves)
  • 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_coveragePassall 4 components with >=2 formalized guarantees have checkable consistency pairs or recorded justification (4 zero-checked: 4 attested)
  • contract_alignment_cleanPasspublic command surfaces have aligned requirement/help/test coverage
  • coverage_metPass100% coverage (90/90)
  • 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_currentPass18/18 specs: claim-reviewed, 210 verified, 210 promoted, 271 dismissed, 1 deferred
  • 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_reviewedPassall changed FRETish-backed requirement descriptions had explicit formalization review delta
  • 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_cleanPass0 unconstrained outputs
  • high_severity_obligation_without_vectorPass1 high/critical ObligationHazard class(es) covered by vector related_obligation_classes
  • high_severity_reproducer_gradePass2 active high/critical-severity or security-relevant (cve_surface possible/likely/confirmed) known issue(s) carry severity_basis=reproducer + a resolving evidence_manifest
  • integration_evidence_witnessedPassno active integration requirements to witness
  • interface_contract_duplicatesPass0 duplicate interface contracts
  • interface_coveragePassall 1 interfaces covered
  • interface_formalization_completePassno configured cross-component specs require FRETish formalization
  • interface_staleness_cleanPass1 interface contracts checked, 0 stale
  • known_issue_affected_requirements_presentPass63 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_completePass63 active known issue(s) meet the quality floor (evidence attached; severity-scaled core fields present; no dedup matches against prior-audit / sibling KIs)
  • 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_effectivePass2 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_consistentPass63 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_resolvesPass63 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_dispositionPass63 known issue(s); none fixed with template_class, kill_domain, or isomorphic_sites to checklist
  • known_issue_template_transferPass63 open known issue(s) meet template-transfer hygiene
  • known_issues_reviewedPass63 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_completePass15 SYS-REQs fully linked and described
  • l2_software_completePass73 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:15, L2:73)
  • lint_cleanPassall functions traced
  • mcdc_coveragePass88 requirements checked, 322 witness rows total, 0 uncovered
  • mcdc_ignore_classifiedPassall 63 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 4 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_completeWarn45 obligation(s) on 36 requirement(s) covered by satisfying children, 5 deferred (tracked), 9 accepted KI-debt (tripwire-backed, auto-expiring) — deferred obligations are tracked debt, not a pass
  • obligation_delegation_resolvesPassall 1 obligation_delegations entries resolve to a target carrying the class
  • obligation_enforcement_backedPassall 45 cataloged obligation checklist item(s) have signal-rule or evidence backing
  • obligation_evidence_completeWarn64 covered, 6 deferred (tracked), 9 accepted KI-debt (tripwire-backed, auto-expiring) — deferred obligations are tracked debt, not a pass
  • obligation_profile_evidence_completePassno evidence profiles configured
  • obligation_suppression_rationalePassall 14 obligation suppression rationale(s) meet the 32-char minimum
  • obligation_suppression_reviewerPassno obligation suppressions at or above reviewer-required severity
  • obligation_witness_groundedPass56 witness(es): 0 grounded (static), 0 cleared (coverage), 1 exempt; 16 witness(es) coverage-unavailable (advisory)
  • orphan_code_cleanPass231/231 code functions traced
  • orphan_tests_cleanPass53 test functions scanned, 0 orphans
  • partition_evidence_completePassno input data-constraint partitions require runtime evidence
  • poc_quality_checkedPass17 in-scope known issue(s) (at or above medium severity, or being submitted) all carry a clean 11-rule PoC quality review
  • problem_report_class_mitigation_evidencePass3 mitigated report(s) all carry class-mitigation evidence
  • problem_reports_reviewedPass3 problem report(s) reviewed; all dispositioned
  • process_checklistPassprocess_checklist: OK — onboard_v1 complete (14 confirmed, 0 skipped, 3 not-applicable (new-project onboarding and adoption-gated steps auto-skipped)) — proof help process-checklists
  • proof_complexity_cleanPassall formalized components fit proof budgets (100 reqs, 128 vars, 75 guarantees)
  • property_based_test_coverageWarn18 function(s) pending property-based test evaluation
  • property_fixtures_existPassno components declare fixture-backed evidence -- property fixtures not applicable
  • quality_cleanPassall 90 requirements passed quality checks
  • residual_kill_hygienePass2 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 73 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: 88 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: 41 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: 74 advisory notice(s)
  • spec_lint_hazard_review_currentPasslint-hazard-review-current: no issues found
  • 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_ste100Passlint-prose-ste100: no issues found
  • 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_coveragePasssurface_coverage: OK — 4 surface(s) (ok=4 debt=0 gap=0 dual_gap=0 dual_residual=0) — proof help surface-coverage
  • suspect_cleanPass0 suspect links
  • sys_has_software_childPass15 SYS-REQ(s) have a downward realization (SW-REQ child, implementing code, or verifying tests)
  • system_formalization_completePassall 15 SYS-REQs formalized in FRETish
  • system_requirements_linkedPass15/15 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_failurePass4 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: 88 formalized requirements evaluated, 0 in safety/financial scope, all sourced from trusted or sanitized data (0 waived, 0 with recorded reasons)
  • under_modeled_requirements_cleanPassno requirements look under-modeled relative to current tests or implementation
  • unresearched_p0_vectorsPass5 vector(s); no P0 unresearched campaigns
  • vacuity_cleanPass0 vacuity findings across 88 eligible requirements
  • validate_passesPass94/94 valid
  • variable_driftPass4 requirement(s) have a variables: list consistent with their FRETish
  • variable_orphans_cleanPass0 variable model issues
  • variables_declaredPass4 formalized components passed solver preflight
  • vector_campaign_closurePass5 vector(s) satisfy campaign closure (3 terminal; 2 evidence-bound; 0 KI-owned; 0 deferred-by-config)
  • vector_campaign_hygienePass5 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 29 declared production source file(s)
  • verification_state_consistentPass90 requirement(s) evaluated — all agree with the derived proposal
  • verify_passesPassverify pipeline passed
  • 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