lint-acceptance-review-current: 7 issue(s)

lint-formalization-quality: 1 issue(s)

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

lint-hazard-review-current: 123 advisory notice(s)

0 ambiguous pairs (7503 pairs checked)

all referenced requirement IDs and obligation annotations match current spec files

0 autolink errors

all functions traced

all 123 requirements passed quality checks

lint-ac-inverse-coverage: no issues found

lint-ac-subset-of-satisfies: 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-data-constraint-parseable: no issues found

lint-decomposition-adds-refinement: no issues found

lint-evidence-tag-exists: no issues found

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

lint-hallucinated-symbols: no issues found

lint-id-shape-canonical: no issues found

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

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

lint-obligation-checklist-empty: no issues found

lint-operational-invariant-var: no issues found

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

lint-plan-of-record-current: 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-trace-review-evidence-current: no issues found

lint-yaml-escape-artefact: no issues found

2 in-branch-changed change-typed reviews lack the backing evidence their declared change kind requires (refactor: no-authored-change; fix: a resolvable DEFECT; feature: a feature LocalChange + spec update)

4 cataloged obligation(s) on 4 requirement(s) lack signal-rule and evidence backing (silent no-ops)

5 report(s): 2 obligation(s) unbound (no witness / no signal-rule), 5 sibling-sweep nudge(s)

all requirements meet evidence diversity policy

no :fuzz annotations in scope

6 active high/critical-severity or CVE-surface 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

7 requirement(s) have all 33 baseline obligation(s) resolved

7 stakeholder obligation checklist(s) fully covered

170 obligation(s) on 67 requirement(s) covered by satisfying children

all 2 obligation_delegations entries resolve to a target carrying the class

131 evidence requirement(s) on 67 parent requirement(s) covered by usable evidence, 3 nominal exemption(s) (reviewer-stamped)

no evidence profiles configured

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

no obligation suppressions at or above reviewer-required severity

175 witness(es): 95 grounded (static), 45 cleared (coverage), 0 exempt

no z3-boundary requirements consume input data-constraint partitions

no requirements carry a verification_strategy

code-level MC/DC below policy (aggregate decisions 0.0% < 100%, aggregate conditions 0.0% < 100%, parser decisions 0.0% < 100%, parser conditions 0.0% < 100%)

109 effective verification state(s) disagree with the derived proposal (Jira-loophole guard)

disabled by project.checks policy

no coverage data yet — run `proof verify-lemma --coverage` first

go build ./... (ok)

code-level MC/DC evidence available for: go

no requirements with coverage data to check

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

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

116 requirements checked, 388 witness rows total, 0 uncovered

all 0 code-level //mcdc:ignore annotation(s) are classified; capability-gap ignores reference a resolvable KnownIssue; 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

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/go-test.json

124/124 valid

0/0 verification chains complete

no verification_scope.completeness.production_include configured

verify pipeline passed

2 traced production implementation files lacked current no-authored-change review

10 of 10 active known issue(s) below the quality floor (0 missing evidence; 0 missing origin; 0 unresolvable origin; 0 inconsistent defect_class; 0 unclassified defect_class; 0 missing `// Reproduces:` comment; 0 missing/invalid CVSS; 0 severity_basis gap(s); 0 mirror-linkage gap(s); 0 environment_note-only at high assurance; 30 stale/invalid evidence; 0 missing current reproducer evidence; 30 total gap(s); 0 dedup match(es) against 0 current KI(s) (ACC-08, integrated)) — a KI without evidence, a recorded origin, the in-test link comment, a valid CVSS vector (security-relevant), an attributed severity basis (issue #277), a COMPLETE mirror-port link when it concerns a mirrored component, or — at high project assurance — anything beyond a prose `environment_note` (issue #322) is a sticky note, not a tracked defect; stale evidence hashes and missing current reproducer-evidence rows (issue #392) now fail the audit the same way `proof known-issue check --fail` does; possible duplicates against prior-audit / sibling KIs (ACC-08) are now surfaced here as the same tracked-debt shape

5 of 10 open known issue(s) need template-transfer hygiene (0 incomplete transfer; 0 suggest template_class; 5 missing dedup_armor)

10 active known issue(s); 10 stale review(s); 0 blocking disposition(s)

5 report(s) with findings

no active accepted risks

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

all approval-required requirements have current approvals

no active assumptions

all 8 affects: entries land in a matching verification.review.motivation

changed requirement review skipped (no git diff context)

0/0 decompositions complete

no changed requirements in current branch

no readable pkg/mcdc/show.go trailer grammar to compare against

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

documentation.enforce_sources not configured (check disabled)

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

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)

5 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

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

10 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

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

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

every no-authored-change review covers a Go file with no spec-orphaned new exported surface

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

no active waivers

15 testable acceptance criteria lack an acceptance-test witness across 7 stakeholder req(s) (0 witnessed via direct acceptance test)

15 acceptance tag(s) sit on a unit/integration test of a derived requirement — a tag is not PoC-quality acceptance evidence

process_checklist: incomplete onboard_v1 (10 pending, 3 not-applicable (new-project onboarding steps auto-skipped)) — next: spec-review-1 — Spec review — structure and ambiguity (role: spec-review) — run: proof checklist show onboard_v1 (proof help process-checklists)

702 function(s) pending property-based test evaluation

no build_targets declared (build matrix check opt-in)

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

no approved guarantee conflicts with an unacknowledged open known issue

6 behavioral implication checks, all 6 proved

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

no concerns directory (concern adjudication no-op)

100% coverage (123/123)

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

100% documentation coverage (123/123)

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

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

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

no residuals directory (residual kill hygiene no-op) — see: proof help residual-disposition

no empty-is-win or finding-quota language in 41 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: no surfaces extracted (no proof/surfaces/*.yaml declarations) — optional; declare sensitive entry points (proof help surface-coverage)

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

11 vector(s); no P0 unresearched campaigns

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

11 vector(s) pass campaign hygiene

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

public command surfaces have aligned requirement/help/test coverage

data_constraint coverage: 6/6 Z3-checked

8 data-constraint coverage checks, all 8 proved

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

no configured cross-component specs require FRETish formalization

all 1 non-bool input/mode variables across 1 formalized components carry a domain model (see: proof help domain-modeling)

all formalized components fit proof budgets (120 reqs, 280 vars, 120 guarantees)

no configured lower formal-layer specs require FRETish formalization

0 slow solver-backed components over 6m0s

no modeling opportunities: 116 formalized requirements evaluated, 1 carried enumerable-domain signals, all with modeled or waived domains (0 waived, 0 with recorded reasons, 1 suppressed by bool-only gate). See: proof help domain-modeling

0 suspect links

all 116 SYS-REQs formalized in FRETish

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

0 vacuity findings across 116 eligible requirements

0 variable model issues

1 formalized components passed solver preflight

no comparable parent-child data-constraint partitions

28 Z3 proof subjects, all 34 proved

0 circular dependencies

0 cross-component reqs fully covered

100% cross-level coverage (7/7)

0 cross-spec contradictions (4186 pairs checked)

no baseline available, skipping

0 unconstrained outputs

0 duplicate interface contracts

all 0 interfaces covered

0 interface contracts checked, 0 stale

all 2 spec levels connected (L0:7, L1:116, L2:0)

280/280 code functions traced

917 test functions scanned, 0 orphans

no retired/superseded requirements

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

116/116 linked to stakeholder reqs

no deadline/timelock narrow-cast signal findings detected under proof/signals

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

no project signal suppressions declared

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

signal validation packs valid: 69 signal(s) behaviorally verified (positives fire, negatives clean); 144 legacy signal(s) in fixture backlog

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

catalog version 1.9.1 in use; no pin configured (set project.catalog.version in proof.yaml for auditor-stable upgrades)

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

116 SYS-REQs fully linked and described

no software/integration requirements to check

SRS generates successfully

all requirements checked

7 stakeholder reqs all have acceptance criteria with derived_reqs

7 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