18 function(s) pending property-based test evaluation

17 stale, 0/17 specs: claim-reviewed, 0 verified, 0 promoted, 0 dismissed

no build_targets declared (build matrix check opt-in)

disabled by project.checks policy

no documented_behaviors declared (documented claim evidence check opt-in)

no dual-path rules declared in proof/dual-path-rules/ or project.dual_path_rules (dual-path guard check opt-in)

disabled by project.checks policy

3 testable acceptance criteria across 2 stakeholder req(s) witnessed (3 via direct acceptance test)

no :acceptance tags share a test carrier with a derived SYS/SW/INT witness

no approved guarantee conflicts with an unacknowledged open known issue

no reqproof:assume directives found; assume_contract_consistency passed

no variables with Z3-backed properties or constraints to verify

all load-bearing code predicates on 70 implemented FRETish requirement(s) are modeled or explicitly not_modeled (63 empty-decision mutex leaf/leaves)

no concerns directory (concern adjudication no-op)

100% coverage (87/87)

0 CVSS-carrying known issue(s) label at or above their own vector band (or carry a reviewer-stamped severity_bound)

project is not Web3/DeFi — deployment_tvl_verified skipped (enable via checks.deployment_tvl_verified.enabled: true)

no differential fixtures under proof/fixtures/ (author one with schema proof.fixtures/v1)

no approved requirement is witnessed only by a failing or skipped test

1 high/critical ObligationHazard class(es) covered by vector related_obligation_classes

no mirrors declared (declare one with `proof mirror add` when starting a refactor/port)

20 in-scope known issue(s) (at or above medium severity, or being submitted) all carry a clean 11-rule PoC quality review

process_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

2 residual(s) pass kill hygiene

no empty-is-win or finding-quota language in 47 role(s)

0 security-named known issue(s) carry a CVSS vector + non-none cve_surface (or a reviewer-stamped security_relevance_justification)

no active known issue has been reported externally (submission / upstream_report block) or marked for submission (disposition)

surface_coverage: OK — 4 surface(s) (ok=4 debt=0 gap=0 dual_gap=0 dual_residual=0) — proof help surface-coverage

15 SYS-REQ(s) have a downward realization (SW-REQ child, implementing code, or verifying tests)

6 configured test command(s) propagate their real failure exit code

no candidate-tautology lemmas detected

5 vector(s); no P0 unresearched campaigns

1 requirement(s) have a variables: list consistent with their FRETish

5 vector(s) satisfy campaign closure (3 terminal; 2 evidence-bound; 0 KI-owned; 0 deferred-by-config)

5 vector(s) pass campaign hygiene

lint-exemplar-missing-on-new: 40 advisory notice(s)

lint-hazard-consequence: 74 advisory notice(s)

lint-ki-banned-markers: 1 advisory notice(s)

disabled by project.checks policy

disabled by project.checks policy

disabled by project.checks policy

0 ambiguous pairs (2355 pairs checked)

all referenced requirement IDs and obligation annotations match current spec files

0 autolink errors

all functions traced

all 87 requirements passed quality checks

lint-ac-inverse-coverage: no issues found

lint-ac-subset-of-satisfies: no issues found

lint-acceptance-review-current: no issues found

lint-annotation-vs-authored: no issues found

lint-assumption-disposition: no issues found

lint-audit-ignore-reason: no issues found

lint-auto-modifier-without-human: no issues found

lint-circularity-self-citation: no issues found

lint-complementary-flags-uninteracted: no issues found

lint-data-constraint-parseable: no issues found

lint-decomposition-adds-refinement: no issues found

lint-degenerate-input-obligation-missing: no issues found

lint-evidence-tag-exists: no issues found

lint-formalization-quality: no issues found

lint-fretish-bare-response: no issues found

lint-fretish-tautology: no issues found

lint-governance-yaml-data-paths: no issues found

lint-hallucinated-symbols: no issues found

lint-hazard-review-current: no issues found

lint-id-shape-canonical: no issues found

lint-inline-impact-review-drift: no issues found

lint-input-domain-obligation-missing: no issues found

lint-ki-attacker-coherence: no issues found

lint-ki-history-chronology: no issues found

lint-ki-open-actionability: no issues found

lint-ki-prose-shape: no issues found

lint-ki-stale-status-refs: no issues found

lint-numbering-gaps-has-tombstone: no issues found

lint-obligation-checklist-empty: no issues found

lint-obligation-coverage-gap: no issues found

lint-operational-invariant-var: no issues found

lint-parent-field-vs-satisfies: no issues found

lint-pinned-delimiter-undispositioned: no issues found

lint-plan-of-record-current: no issues found

lint-prose-ste100: no issues found

lint-reject-combination-composition-witnessed: no issues found

lint-req-type-vs-description: no issues found

lint-review-cadence-current: no issues found

lint-satisfies-target-retired: no issues found

lint-shared-state-rebuild: no issues found

lint-source-doc-hedging: no issues found

lint-source-native-yaml-trace: no issues found

lint-spec-conformance-review-grounded: no issues found

lint-status-vs-review: no issues found

lint-sw-informal-witnessed: no issues found

lint-threat-surface-present: no issues found

lint-trace-review-evidence-current: no issues found

lint-unjoined-effect-halves: no issues found

lint-yaml-escape-artefact: no issues found

every in-branch-changed change-typed review has complete backing evidence

evidence diversity policy disabled

no :fuzz annotations in scope

2 active high/critical-severity or security-relevant (cve_surface possible/likely/confirmed) known issue(s) carry severity_basis=reproducer + a resolving evidence_manifest

no active integration requirements to witness

no mirrors declared (declare one with `proof mirror add` when starting a refactor/port)

0 security-classed requirement(s) carry a negative-path witness

0 requirement(s) have all 0 baseline obligation(s) resolved

2 stakeholder obligation checklist(s) fully covered

46 obligation(s) on 35 requirement(s) covered by satisfying children, 14 accepted KI-debt (tripwire-backed, auto-expiring)

all 1 obligation_delegations entries resolve to a target carrying the class

all 46 cataloged obligation checklist item(s) have signal-rule or evidence backing

62 evidence requirement(s) on 35 parent requirement(s) covered by usable evidence, 15 accepted KI-debt (tripwire-backed, auto-expiring)

no evidence profiles configured

all 15 obligation suppression rationale(s) meet the 32-char minimum

no obligation suppressions at or above reviewer-required severity

69 witness(es): 0 grounded (static), 0 cleared (coverage), 1 exempt; 19 witness(es) coverage-unavailable (advisory)

no input data-constraint partitions require runtime evidence

no problem reports

no requirements carry a verification_strategy

all 4 components with >=2 formalized guarantees have checkable consistency pairs or recorded justification (4 zero-checked: 4 attested)

public command surfaces have aligned requirement/help/test coverage

no variables with Z3-backed properties or constraints to check

no variables with Z3-backed properties or constraints to verify

no SYS-REQ claims formalization_status=valid with a LEMMA: trace or verifies: annotation

no configured cross-component specs require FRETish formalization

no 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

all formalized components fit proof budgets (100 reqs, 130 vars, 75 guarantees)

all 70 review or approved guarantee requirement(s) in 1 configured lower formal-layer spec(s) have a non-envelope FRETish formalization

0 slow solver-backed components over 1m0s

no modeling opportunities: 85 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

0 suspect links

all 15 SYS-REQs formalized in FRETish

no requirements look under-modeled relative to current tests or implementation

0 vacuity findings across 85 eligible requirements

0 variable model issues

4 formalized components passed solver preflight

no comparable parent-child data-constraint partitions

no variables with Z3-backed properties or constraints to verify

no separate-file lemma bindings recorded yet — run `proof verify-lemma` on a package with import-attached `// reqproof:lemma ... binds-to ...` directives to populate

0 reqproof:lemma annotations in project — coverage not applicable until lemmas are authored

for 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)

code-level MC/DC meets configured thresholds (aggregate decisions 100.0%, conditions 100.0%, 0 incomplete functions) (63 ignored decisions)

code-level MC/DC evidence available for: bash, js, qml

no requirements with coverage data to check

no components declare fixture-backed evidence -- fixture staleness not applicable

no components declare fixture-backed evidence -- FLIP fixtures not applicable

no components declare fixture-backed evidence -- FLIP test alignment not applicable

85 requirements checked, 311 witness rows total, 0 uncovered

all 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

no KI-gated MC/DC or obligation disposition has outlived its fixed bug

mcdc verifies witness enforcement disabled

all MC/DC witness tests reference product code and configured outcome-variable code

no components declare fixture-backed evidence -- property fixtures not applicable

slow-test audit not evaluated from shared instrumented code-level MC/DC test timings

all tests passed; linked test results from .proof/test-results/junit.xml

91/91 valid

14/14 verification chains complete

declared scope covers all 29 declared production source file(s)

87 requirement(s) evaluated — all agree with the derived proposal

verify pipeline passed

0 circular dependencies

0 cross-component reqs fully covered

100% cross-level coverage (2/2)

0 cross-spec contradictions (0 pairs checked)

no baseline available, skipping

0 unconstrained outputs

0 duplicate interface contracts

all 1 interfaces covered

1 interface contracts checked, 0 stale

all 3 spec levels connected (L0:2, L1:15, L2:70)

231/231 code functions traced

138 test functions scanned, 0 orphans

no retired/superseded requirements

all role references resolve (47 built-in + 0 project-local role(s) checked)

15/15 linked to stakeholder reqs

disabled by project.checks policy

no proof/signals directory (deadline-cast signal hunt no-op)

4 code signal(s) across 4 source artifact(s); explicit signal obligations covered or explicitly resolved

no project signal suppressions declared

4 code signal(s) across 4 source artifact(s); no proposes_class declarations are unbindable

disabled by project.checks policy

no known issue declares `platforms:` (platform-bound closure check opt-in)

no build_targets declared (platform coverage check opt-in)

disabled by project.checks policy

no active accepted risks

all 0 approved requirement(s) carry valid motivation (or are initial-creation exemptions)

approval policy disabled

no active assumptions

all traced production implementation files have current no-authored-change reviews

no semantic-scan artifact

no CHG / DEFECT records declared affects: (nothing to cross-check)

changed requirement review skipped (no git diff context)

0/0 decompositions complete; 14 parent(s) state their own verified claim and are refined, not decomposed

no changed requirements in current branch

no active known issues carry a `private` or under-embargo disclosure

documentation.enforce_sources not configured (check disabled)

73 active known issue(s) name the requirement(s) they violate (or carry a reviewer-stamped requirement_exemption)

73 active known issue(s) meet the quality floor (evidence attached; severity-scaled core fields present; no dedup matches against prior-audit / sibling KIs)

0 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)

2 high/critical known issue(s) with a poc_quality block satisfy every applicable rule (or carry a reviewer-stamped poc_quality_exemption)

no known issues are overdue for upstream re-check

73 active known issue(s) with a bound reproducer assert the secure contract or declare a characterization (no reproducer contradicts its finding)

73 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

0 security-relevant known issue(s) document a remediation or mitigation (or carry a reviewer-stamped remediation_exemption)

0 known issue(s) with a prose severity grade match their structured severity field (or carry a reviewer-stamped severity_bound)

73 known issue(s); none fixed with template_class, kill_domain, or isomorphic_sites to checklist

73 open known issue(s) meet template-transfer hygiene

73 active known issue(s) visible (review interval 90 day(s))

no problem reports

no untrusted-input dataflows into trusted outputs: 85 formalized requirements evaluated, 0 in safety/financial scope, all sourced from trusted or sanitized data (0 waived, 0 with recorded reasons)

no active waivers

catalog/obligation/signal/requirement set is internally consistent (18 obligation_class(es) declared, 327 catalog class(es) loaded)

catalog version pin "1.11.0" matches shipped 1.11.0 (policy=manual)

2 STK-REQs fully structured (persona, story, acceptance criteria with derived_reqs)

15 SYS-REQs fully linked and described

70 SW/INT-REQs fully linked to SYS-REQs

SRS generates successfully

all requirements checked

2 stakeholder reqs all have acceptance criteria with derived_reqs

2 stakeholder requirements found

no 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

no 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

no 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