Proof Portal

Projects

jsonparser

ProbeLabs23 findings · 123 requirements

The fastest JSON parser for Go — formally verified with ReqProof (real library, master).

All requirements
RequirementSTK-REQ-003StakeholderReview

Library users shall extract known numeric and boolean JSON values through typed helpers without manual byte parsing or ad-hoc conversions.

This requirement changed after its last recorded review, so approval is stale. Automated checks pass and 2/2 obligations are satisfied.
PriorityshallTypeguaranteeCategoryfunctionalComponentparserAssuranceEFindingsnone open

Specification

The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.

Description

Library users shall extract known numeric and boolean JSON values through typed helpers without manual byte parsing or ad-hoc conversions.

Rationale & tags

Why this requirement exists, and how it is categorised.

The README presents typed helpers as part of the public API for callers who already know the expected JSON scalar type.

parseraccepts_user_data

Verification & provenance

How this requirement was checked: the review trail, edit history, and the machine-analysis status terms (each ⓘ explains what it means).

Assurance levelE
Formalizationnone
Vacuitychecked_ok
Strategyinformal

Review

Status
approved
Reviewer
Leonidbugaev
Reviewed
Apr 23, 2026, 00:00 UTC

History

Created
Apr 13, 2026, 17:10 UTC · Created via CLI
Modified
Jul 26, 2026, 12:53 UTC · Created via CLI

Change history

Every recorded revision of this requirement's source file — newest first, each with its commit message and the diff for that change.

Every recorded revision of this object's source — newest first, each with the commit message and its file-level diff.

Obligations

What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.

9 obligations · 8 discharged · 1 not yet witnessed

Browse the catalogue

Evidence tagged via <REQ> is witnessed by a requirement that satisfies this one — normal for stakeholder / aggregate requirements, which are proven through the requirements that refine them.

Discharged

Behavior at limits, thresholds, and edge-of-range values.

If it were violatedMedium

GetInt on int64.MaxInt64+1 silently wraps via parseInt overflow flag; if the overflow check regresses, GetInt returns a negative int64 instead of OverflowIntegerError.

Discharging evidence0/0 required witnessed
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-076
Discharged

Output identical regardless of collection ordering or runtime conditions.

If it were violatedMedium

ParseFloat on the same numeric token must return the same float64 across calls; a regression in parseFloat rounding direction (architecture-dependent FPU) produces non-deterministic results.

Discharging evidence0/0 required witnessed
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-003
Discharged

Behavior for unusual but valid input combinations.

If it were violatedMedium

GetBoolean on a payload with value null returns NullValueError instead of (false,nil); callers treating the zero-value as absent silently misread null fields as boolean false.

Discharging evidence0/0 required witnessed
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-076
Discharged

Behavior when inputs are absent, nil, zero-length, or blank.

If it were violatedHigh

GetInt on a zero-length []byte flows through Get empty-input path; the data[offset] dereference in getType panics with index-out-of-range on the empty slice.

Discharging evidence0/0 required witnessed
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-078
Discharged

Behavior when inputs are syntactically or structurally invalid.

If it were violatedHigh

GetInt on a token like 12x34 drives parseInt to ok=false; if the malformed check regresses, GetInt silently returns 12 (the partial parse) instead of MalformedValueError.

Discharging evidence1/1 required witnessed
  • negativerequiredpresent
    Covered by 2 tests
    via SYS-REQ-075
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-075
Discharged

Behavior specified when inputs are nil, null, or zero-value.

If it were violatedHigh

GetBoolean(nil, ...) flows through Get nil-slice path; getType(nil,0) data[offset] dereference panics with nil-slice index-out-of-range.

Discharging evidence1/1 required witnessed
  • negativerequiredpresent
    Covered by 2 tests
    via SYS-REQ-078
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-078
Not yet witnessed

Happy-path behavior with valid inputs.

Discharging evidence0/0 required witnessed
    Discharged
    If it were violatedHigh

    GetBoolean on a truncated tru or fals token fails bytes.Equal against the literal; if the partial-literal recovery regresses the caller path panics on the empty value slice.

    Discharging evidence0/0 required witnessed
    • nominalrecommendedpresent
      Covered by 1 test
      via SYS-REQ-079
    Discharged
    If it were violatedMedium

    GetInt on a JSON String value returns the documented not-a-number error; if the type check regresses, GetInt feeds raw quoted bytes to ParseInt which silently returns 0 instead of erroring.

    Discharging evidence0/0 required witnessed
    • nominalrecommendedpresent
      Covered by 1 test
      via SYS-REQ-077

    Acceptance criteria

    Stakeholder conditions for satisfaction, traced to the derived requirements and evidence that discharge them.

    Stakeholder-authored conditions defining when the requirement is satisfied, traced to derived requirements / evidence.

    • AC-1verify: test

      A caller can request an integer-valued field through a typed helper and receive the expected int64 result or an error when integer access is invalid.

      Acceptance test
    • AC-2verify: test

      A caller can request a floating-point field through a typed helper and receive the expected float64 result or an error when float access is invalid.

      Derived requirements
      Acceptance test
    • AC-3verify: test

      A caller can request a boolean field through a typed helper and receive the expected bool result or an error when boolean access is invalid.

      Acceptance test

    Its place

    This requirement shown inside its trace neighbourhood — the parents it satisfies, the code and tests attached to it, and its findings.

    Loading graph…

    Trace evidence

    The concrete artifacts linked to this requirement — implementing code, verifying tests, documents, and the findings raised against it.

    No implementation linked

    No source files are traced to this requirement yet.

    Impact

    Blast radius — if you change this requirement, what else may need re-checking, and what it in turn depends on.

    If you change this

    Requirements
    11
    Files
    3
    Tests
    13
    At-risk contracts
    0

    Files to re-check (3)

    • fuzz.gofuzz.go
    • parser.goparser.go
    • aliases.goaliases.go

    Tests to re-run (13)

    • benchmark_large_payload_test.gobenchmark/benchmark_large_payload_test.go
    • benchmark_medium_payload_test.gobenchmark/benchmark_medium_payload_test.go
    • benchmark_small_payload_test.gobenchmark/benchmark_small_payload_test.go
    • obligation_evidence_test.goobligation_evidence_test.go
    • parser_test.goparser_test.go
    • fuzz_native_test.gofuzz_native_test.go
    • len_uint_test.golen_uint_test.go
    • mcdc_spec_witnesses_test.gomcdc_spec_witnesses_test.go
    • mcdc_supplement_test.gomcdc_supplement_test.go
    • aliases_test.goaliases_test.go
    • array_each_err_test.goarray_each_err_test.go
    • deep_spec_test.godeep_spec_test.go
    • obligation_property_test.goobligation_property_test.go

    What this rests on

    Discussions

    Discuss this with the proof team. Nothing changes in your audit automatically — you open a request and a staff member records any outcome inside the thread.

    Sign in to discuss this with the proof team.Sign in