Proof Portal

Sign in
Projects

jsonparser

ProbeLabs23 findings · 123 requirements
Audit history

Run · 96a2d33

Audited Aug 20, 2026, 02:30 PM on proof-demo.

Partial13 warningsuncommitted changes
116/116 realizable123/123 meet policyverification complete: 123

as of 96a2d33 · Aug 20, 2026 · proof-demo

Run context
What was audited, and where.
Branchproof-demo
Commit96a2d33
RecordedAug 20, 2026, 02:30 PM
Tags—
Working treeuncommitted changes
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_witnessedFail15 testable acceptance criteria lack an acceptance-test witness across 7 stakeholder req(s) (0 witnessed via direct acceptance test)
  • acceptance_witness_qualityWarn15 acceptance tag(s) sit on a unit/integration test of a derived requirement — a tag is not PoC-quality acceptance evidence
  • accepted_risks_reviewedPassno active accepted risks
  • ambiguity_reviewedPass0 ambiguous pairs (7503 pairs checked)
  • annotation_validityPassall referenced requirement IDs and obligation annotations match current spec files
  • approval_motivation_presentPassall 123 approved requirement(s) carry valid motivation (or are initial-creation exemptions)
  • approvals_currentPassall approval-required requirements have current approvals
  • approved_guarantee_ki_conflictPassno approved guarantee conflicts with an unacknowledged open known issue
  • assumptions_statusPassno active assumptions
  • authored_delta_expectedWarn2 traced production implementation files lacked current no-authored-change review
  • autolink_cleanPass0 autolink errors
  • behavioral_implications_verifiedPass6 behavioral implication checks, all 6 proved
  • build_matrix_completeSkipno build_targets declared (build matrix check opt-in)
  • build_passesPassgo build ./... (ok)
  • catalog_completenessPasscatalog/obligation/signal/requirement set is internally consistent (27 obligation_class(es) declared, 340 catalog class(es) loaded)
  • catalog_version_pinnedPasscatalog version 1.9.1 in use; no pin configured (set project.catalog.version in proof.yaml for auditor-stable upgrades)
  • change_evidence_completeWarn2 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)
  • change_record_landsPassall 8 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_coverageFailcode-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%)
  • code_mcdc_measurePasscode-level MC/DC evidence available for: go
  • code_predicates_modeledPassall load-bearing code predicates on 0 implemented FRETish requirement(s) are modeled or explicitly not_modeled (0 empty-decision mutex leaf/leaves)
  • code_signal_deadline_cast_unreviewedPassno deadline/timelock narrow-cast signal findings detected under proof/signals
  • code_signal_obligations_reviewedPass45 code signal(s) across 0 source artifact(s); explicit signal obligations covered or explicitly resolved
  • code_signal_suppressions_reviewedPassno project signal suppressions declared
  • code_signal_unbindablePass45 code signal(s) across 0 source artifact(s); no proposes_class declarations are unbindable
  • concern_adjudicatedPassno concerns directory (concern adjudication no-op)
  • consistency_pair_coveragePassall 1 components with >=2 formalized guarantees have checkable consistency pairs or recorded justification (0 zero-checked: 0 attested)
  • contract_alignment_cleanPasspublic command surfaces have aligned requirement/help/test coverage
  • coverage_metPass100% coverage (123/123)
  • coverage_thresholdPassno requirements with coverage data to check
  • cross_component_cleanPass0 cross-component reqs fully covered
  • cross_level_completePass100% cross-level coverage (7/7)
  • cross_spec_consistency_cleanPass0 cross-spec contradictions (4186 pairs checked)
  • cvss_severity_consistentPass9 CVSS-carrying known issue(s) label at or above their own vector band (or carry a reviewer-stamped severity_bound)
  • data_constraint_z3_coveragePassdata_constraint coverage: 6/6 Z3-checked
  • data_constraints_completePass8 data-constraint coverage checks, all 8 proved
  • decomposition_reviewedPass0/0 decompositions complete
  • 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_completePassno readable pkg/mcdc/show.go trailer grammar to compare against
  • 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_coveragePass100% documentation coverage (123/123)
  • 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_diversityPassall requirements meet evidence diversity policy
  • 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_existSkipdisabled by project.checks policy
  • 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_vectorPass18 high/critical ObligationHazard class(es) covered by vector related_obligation_classes
  • high_severity_reproducer_gradePass6 active high/critical-severity or CVE-surface 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 0 interfaces covered
  • interface_formalization_completePassno configured cross-component specs require FRETish formalization
  • interface_staleness_cleanPass0 interface contracts checked, 0 stale
  • known_issue_affected_requirements_presentPass10 active known issue(s) name the requirement(s) they violate (or carry a reviewer-stamped requirement_exemption)
  • known_issue_completeWarn10 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
  • 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_poc_quality_effectivePass5 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_consistentPass10 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_resolvesPass10 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_presentPass3 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_dispositionPass16 known issue(s); none fixed with template_class, kill_domain, or isomorphic_sites to checklist
  • known_issue_template_transferWarn5 of 10 open known issue(s) need template-transfer hygiene (0 incomplete transfer; 0 suggest template_class; 5 missing dedup_armor)
  • known_issues_reviewedWarn10 active known issue(s); 10 stale review(s); 0 blocking disposition(s)
  • l0_stakeholder_completePass7 STK-REQs fully structured (persona, story, acceptance criteria with derived_reqs)
  • l1_system_completePass116 SYS-REQs fully linked and described
  • l2_software_completePassno software/integration requirements to check
  • lemma_branch_coverageSkipno coverage data yet — run `proof verify-lemma --coverage` first
  • levels_connectedPassall 2 spec levels connected (L0:7, L1:116, L2:0)
  • lint_cleanPassall functions traced
  • mcdc_coveragePass116 requirements checked, 388 witness rows total, 0 uncovered
  • mcdc_ignore_classifiedPassall 0 code-level //mcdc:ignore annotation(s) are classified; capability-gap ignores reference a resolvable KnownIssue; 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
  • mirror_completePassno 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_reviewedPassevery no-authored-change review covers a Go file with no spec-orphaned new exported surface
  • nonbool_inputs_constrainedPassall 1 non-bool input/mode variables across 1 formalized components carry a domain model (see: proof help domain-modeling)
  • obligation_baselinePass7 requirement(s) have all 33 baseline obligation(s) resolved
  • obligation_completenessPass7 stakeholder obligation checklist(s) fully covered
  • obligation_decomposition_completePass170 obligation(s) on 67 requirement(s) covered by satisfying children
  • obligation_delegation_resolvesPassall 2 obligation_delegations entries resolve to a target carrying the class
  • obligation_enforcement_backedWarn4 cataloged obligation(s) on 4 requirement(s) lack signal-rule and evidence backing (silent no-ops)
  • obligation_evidence_completePass131 evidence requirement(s) on 67 parent requirement(s) covered by usable evidence, 3 nominal exemption(s) (reviewer-stamped)
  • obligation_profile_evidence_completePassno evidence profiles configured
  • obligation_suppression_rationalePassall 40 obligation suppression rationale(s) meet the 32-char minimum
  • obligation_suppression_reviewerPassno obligation suppressions at or above reviewer-required severity
  • obligation_witness_groundedPass175 witness(es): 95 grounded (static), 45 cleared (coverage), 0 exempt
  • orphan_code_cleanPass280/280 code functions traced
  • orphan_tests_cleanPass917 test functions scanned, 0 orphans
  • partition_evidence_completePassno z3-boundary requirements consume input data-constraint partitions
  • poc_quality_checkedPass7 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_evidenceWarn5 report(s): 2 obligation(s) unbound (no witness / no signal-rule), 5 sibling-sweep nudge(s)
  • problem_reports_reviewedWarn5 report(s) with findings
  • process_checklistWarnprocess_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)
  • proof_complexity_cleanPassall formalized components fit proof budgets (120 reqs, 280 vars, 120 guarantees)
  • property_based_test_coverageWarn702 function(s) pending property-based test evaluation
  • property_fixtures_existPassno components declare fixture-backed evidence -- property fixtures not applicable
  • quality_cleanPassall 123 requirements passed quality checks
  • residual_kill_hygienePassno residuals directory (residual kill hygiene no-op) — see: proof help residual-disposition
  • retired_cleanupPassno retired/superseded requirements
  • role_prompt_hygienePassno empty-is-win or finding-quota language in 41 role(s)
  • role_references_resolvePassall role references resolve (41 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_validPasssignal validation packs valid: 69 signal(s) behaviorally verified (positives fire, negatives clean); 144 legacy signal(s) in fixture backlog
  • slow_tests_cleanPassslow-test audit not evaluated from shared instrumented code-level MC/DC test timings
  • software_formalization_completePassno configured lower formal-layer specs require FRETish formalization
  • solver_latency_cleanPass0 slow solver-backed components over 6m0s
  • solver_modeling_opportunityPassno 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
  • 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_currentWarnlint-acceptance-review-current: 7 issue(s)
  • 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_data_constraint_parseablePasslint-data-constraint-parseable: no issues found
  • spec_lint_decomposition_adds_refinementPasslint-decomposition-adds-refinement: no issues found
  • spec_lint_evidence_tag_existsPasslint-evidence-tag-exists: no issues found
  • spec_lint_formalization_qualityWarnlint-formalization-quality: 1 issue(s)
  • 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: 2 advisory notice(s)
  • spec_lint_hazard_review_currentInfolint-hazard-review-current: 123 advisory notice(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_numbering_gaps_has_tombstonePasslint-numbering-gaps-has-tombstone: no issues found
  • spec_lint_obligation_checklist_emptyPasslint-obligation-checklist-empty: 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_plan_of_record_currentPasslint-plan-of-record-current: 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_trace_review_evidence_currentPasslint-trace-review-evidence-current: 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_criteriaPass7 stakeholder reqs all have acceptance criteria with derived_reqs
  • stakeholder_requirements_existPass7 stakeholder requirements found
  • submission_validatedPassno active known issue has been reported externally (submission / upstream_report block) or marked for submission (disposition)
  • surface_coveragePasssurface_coverage: no surfaces extracted (no proof/surfaces/*.yaml declarations) — optional; declare sensitive entry points (proof help surface-coverage)
  • suspect_cleanPass0 suspect links
  • system_formalization_completePassall 116 SYS-REQs formalized in FRETish
  • system_requirements_linkedPass116/116 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_failurePass2 configured test command(s) propagate their real failure exit code
  • tests_passPassall tests passed; linked test results from .proof/test-results/go-test.json
  • trusted_outputs_from_untrusted_inputsPassno 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)
  • under_modeled_requirements_cleanPassno requirements look under-modeled relative to current tests or implementation
  • unresearched_p0_vectorsPass11 vector(s); no P0 unresearched campaigns
  • vacuity_cleanPass0 vacuity findings across 116 eligible requirements
  • validate_passesPass124/124 valid
  • variable_driftPass116 requirement(s) have a variables: list consistent with their FRETish
  • variable_orphans_cleanPass0 variable model issues
  • variables_declaredPass1 formalized components passed solver preflight
  • vector_campaign_hygienePass11 vector(s) pass campaign hygiene
  • verification_chain_completePass0/0 verification chains complete
  • verification_plan_evidencePassno requirements carry a verification_strategy
  • verification_scope_completePassno verification_scope.completeness.production_include configured
  • verification_state_consistentWarn109 effective verification state(s) disagree with the derived proposal (Jira-loophole guard)
  • verify_passesPassverify pipeline passed
  • waivers_reviewedPassno active waivers
  • z3_cross_layer_consistencyPassno comparable parent-child data-constraint partitions
  • z3_properties_verifiedPass28 Z3 proof subjects, all 34 proved