Proof Portal

Sign in
Projects

jsonparser

ProbeLabs23 findings · 123 requirements
Audit history

Run · 775a6cc

Audited Aug 3, 2026, 11:10 AM on proof-demo.

Needs attention1 error9 warnings
116/116 realizable123/123 meet policyverification complete: 123

as of 775a6cc · Aug 3, 2026 · proof-demo

Run context
What was audited, and where.
Branchproof-demo
Commit775a6cc
RecordedAug 3, 2026, 11:10 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_witnessedPass15 testable acceptance criteria across 7 stakeholder req(s) witnessed (15 via direct acceptance test)
  • 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
  • assume_contract_consistencyPassno reqproof:assume directives found; assume_contract_consistency passed
  • 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_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_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
  • 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)
  • 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
  • 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)
  • 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_gradeFail6 of 6 high/critical-severity or CVE-surface known issue(s) fail the reproducer-grade gate (3 missing/wrong severity_basis; 0 missing evidence_manifests; 0 non-resolving evidence_manifests; 0 missing tripwire_mutation; 6 reproducer does not exercise affected_api; 9 total gap(s)) — a high-stakes claim shall NOT rest on static analysis or judgment alone: set severity_basis=reproducer, declare a tripwire_mutation, and attach a resolving evidence_manifest whose reproducer exercises the target (issues #350, #845)
  • 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_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 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), 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_recheck_duePassno known issues are overdue for upstream re-check
  • 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_reviewedPass10 active known issue(s) visible
  • 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_binding_freshnessSkipno separate-file lemma bindings recorded yet — run `proof verify-lemma` on a package with import-attached `// reqproof:lemma ... binds-to ...` directives to populate
  • 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_evidence_completeFail2 evidence requirement(s) on 2 parent requirement(s) lack 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_groundedPass173 witness(es): 93 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_checkedWarn7 of 7 in-scope known issue(s) (at or above medium severity, or being submitted) have PoC quality gaps (7 missing block, 0 failed rule(s)). ACC-15.
  • 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
  • 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_references_resolveWarn2 dangling role reference(s) across 1 role(s)
  • signal_fixtures_validPasssignal validation packs valid: 67 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_cleanSkipsolver latency check skipped: host load average 35.96 on 14 CPUs (>1.5x) at audit start indicates external CPU pressure; rerun under quieter load for honest measurement
  • 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_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_qualityPasslint-formalization-quality: 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: 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)
  • 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
  • trivial_lemmaPassno candidate-tautology lemmas detected
  • 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