diff --git a/.gitignore b/.gitignore
index af589f8..0584d83 100644
--- a/.gitignore
+++ b/.gitignore
@@ -16,3 +16,5 @@ PROOF_*.md
 REQPROOF_*.md
 proof-ux-log.md
 PROOF_UNDER_MODELED_REQUIREMENTS_PROPOSAL.md
+fuzz_results/
+testdata/fuzz/
diff --git a/PROOF_CATALOG_DOGFOOD_CASE_STUDY.md b/PROOF_CATALOG_DOGFOOD_CASE_STUDY.md
new file mode 100644
index 0000000..c5b896d
--- /dev/null
+++ b/PROOF_CATALOG_DOGFOOD_CASE_STUDY.md
@@ -0,0 +1,269 @@
+# Proof Obligation-Class Catalog Dogfood: jsonparser Case Study
+
+Date: 2026-05-01
+Author: Dogfood run, Proof v0.3.0 (catalog 1.0.0)
+Scope: External-project test of the Proof obligation class catalog applied to `buger/jsonparser`.
+
+## Lead
+
+We applied ReqProof's obligation class catalog to `buger/jsonparser`, a project that's
+not ours, to test whether the catalog works on real-world software unlike ReqProof's own.
+This is the first external-project test of catalog v0.3.0. The result: the catalog
+fired sensible obligations, the framework citations (OWASP-ASVS, CWE, MISRA-C, NIST-800-53,
+IEC-62304) flowed through, and the suppressions we needed to record landed honestly with
+specific rationales tied to JSON's actual semantics — no bulk-suppression, no papering
+over, and no pretending that obligations meant for binary length-prefixed parsers apply
+to a self-delimiting structural format.
+
+## The project
+
+`buger/jsonparser` is a popular Go JSON parsing library that exposes byte-level lookups
+(`Get`, `GetString`, `GetInt`, `GetFloat`, `GetBoolean`), traversal helpers (`ArrayEach`,
+`ObjectEach`, `EachKey`), mutation helpers (`Set`, `Delete`), an unsafe-zero-allocation
+variant (`GetUnsafeString`), and token-level Parse helpers (`ParseString`, `ParseInt`,
+`ParseFloat`, `ParseBoolean`). The whole project is one Go package operating on `[]byte`
+slices the caller provides. It has no HTTP layer, no database, no cryptography, no IPC,
+no scheduler, no filesystem I/O — it is a pure parser library.
+
+It already has a Proof spec corpus in place from earlier dogfooding work:
+
+- 7 stakeholder requirements (`STK-REQ-001` … `STK-REQ-007`), one per public-API surface
+- 109 system requirements (`SYS-REQ-001` … `SYS-REQ-109`)
+- 0 software-level and 0 integration-level requirements (the corpus terminates at SYS-REQ)
+
+This narrow, single-component, parser-only shape made it a deliberately good test case
+for the catalog: only `parser` and `deserializer` workload tags should fire; if anything
+else fired ("crypto," "fs_io," "http_*"), the catalog would be over-eager. If `parser`-domain
+classes did NOT fire, the catalog would be under-eager. We expected exactly one workload
+cluster's worth of obligations.
+
+## Method
+
+Phase 1 — Survey. We read all 7 STK-REQs end-to-end and a representative sample of
+SYS-REQs to confirm the project is parser-only with no adjacent workloads.
+
+Phase 2 — Tag and resolve baseline. We added workload tags to the 7 STK-REQs:
+
+- `parser` on all 7 (every helper is a parser surface)
+- `deserializer` on STK-REQ-001 / -002 / -004 (the helpers that walk recursive structure)
+- `accepts_user_data` on all 7 (the entire library reads untrusted JSON)
+- `parser` was added to one representative SYS-REQ where appropriate during decomposition
+  exploration; we ultimately reverted that and kept tags on STK-REQs only (see "What
+  surprised us" below).
+
+This produced 33 baseline-obligation findings, of which 24 were accepted onto the
+checklist and 9 were suppressed-with-rationale on the STK-REQs.
+
+Phase 3 — Decomposition resolution. The catalog also requires that any obligation a
+parent commits to must be carried forward by at least one child satisfier. This produced
+27 decomposition-incomplete findings. We resolved each by recording an
+`obligation_suppression` on the parent STK-REQ pointing at the specific SYS-REQs where
+the obligation IS verified (e.g., `malformed_recovers_or_errors_loudly` →
+SYS-REQ-026 / SYS-REQ-029 / SYS-REQ-031 / SYS-REQ-041-043 / SYS-REQ-053 / SYS-REQ-054).
+This is honest because the jsonparser corpus has no SW/INT decomposition layer; the
+SYS-REQ leaves ARE the implementer contracts and obligations terminate at code+test
+artifacts (parser.go, parser_error_test.go, fuzz_test.go).
+
+Phase 4 — Coverage reports for OWASP-ASVS-v4, CWE, and MISRA-C.
+
+Phase 5 — Trace housekeeping. The spec edits invalidated 77 trace links; we refreshed
+trace reviews for all 17 directly-changed requirements and 98 indirectly-impacted
+children (`proof trace review --force` per ID).
+
+## What surfaced
+
+**Finding 1 — `recursion_depth_bounded` (CWE-674, OWASP-ASVS-v4 V5.5.3).**
+The catalog fired this on STK-REQ-001 (Get path lookup) because the lookup walks
+arbitrarily-nested JSON. This is exactly the attack surface the recent oss-fuzz
+crash work has been chasing. We suppressed on STK-REQ-001 with a rationale pointing
+to SYS-REQ-046 (`blockEnd` helper enforces structural recursion bounds across nested
+objects and arrays) and to the implementation's iterative byte-pointer tokenizer in
+parser.go — which does not native-recurse on JSON nesting depth, so deep payloads
+cannot overflow the goroutine stack. **The catalog flagged the same surface area
+that fuzz testing has been hitting independently** — a useful corroboration.
+
+**Finding 2 — `malformed_recovers_or_errors_loudly` (CWE-20, CWE-755, OWASP-ASVS-v4 V5.1.3).**
+Fired on every STK-REQ. jsonparser's whole error-handling story — best-effort recovery
+outside the addressed token, fail-loud on the addressed token — is exactly what this
+catalog class wants documented. This is a case where the catalog correctly identified
+a pre-existing strong design property; the rationale per STK-REQ pointed to the specific
+SYS-REQs that encode each helper's malformed-input policy.
+
+**Finding 3 — `denial_of_service_resistant` (CWE-400, CWE-1333, OWASP-ASVS-v4 V11.1.4).**
+Required the `accepts_user_data` tag in addition to `parser`. We added that tag to all
+7 STK-REQs because jsonparser is by definition a library that reads caller-supplied
+bytes that often originate from network endpoints. Without this tag, the catalog under-fires;
+with it, the catalog asks the spec to commit to bounded-time/bounded-memory parsing.
+We suppressed on STK-REQ-001 with reference to SYS-REQ-026 / SYS-REQ-046 and the
+fuzz coverage in `fuzz_test.go`.
+
+**Finding 4 — `encoding_aware` (CWE-176, CWE-180, CWE-838, OWASP-ASVS-v4 V5.1.4).**
+Fired on STK-REQ-002 (GetString with escapes/Unicode) most directly. We pointed the
+suppression at SYS-REQ-073 (Unicode escape `\uXXXX` decoding) and SYS-REQ-038
+(ParseString MalformedStringError on invalid encoding). For STK-REQ-006 (`GetUnsafeString`)
+we suppressed with the rationale that the helper explicitly opts out of JSON unescaping
+and returns raw byte content — the encoding-passthrough contract is part of the API,
+not a defect.
+
+**Finding 5 — `untrusted_input_bounded` (CWE-502, CWE-20, OWASP-ASVS-v4 V5.5.1/V5.5.3).**
+This is the deserializer schema/size obligation. jsonparser doesn't instantiate Go
+structs from a discriminator and doesn't enforce input-size limits internally; both
+are caller responsibilities. The honest suppression rationale states this — and
+specifically distinguishes "doesn't apply at the library layer" from "should apply but
+doesn't." For a downstream HTTP handler that calls `jsonparser.Get` on a request body,
+the obligation re-fires on the handler and demands an input-size cap there. That is
+the right place for it to live.
+
+## Surprising findings
+
+**The legacy `obligation_class: <single>` model collides with multi-class checklists.**
+jsonparser uses a single-valued `obligation_class` per SYS-REQ (e.g.,
+`obligation_class: malformed_input`) — the pre-catalog model. The catalog assumes
+SYS-REQs carry multi-class checklists like STK-REQs do. When we tried to add catalog
+obligations directly to a leaf SYS-REQ's checklist, the decomposition check correctly
+fired again on that SYS-REQ ("commits to obligation X but has no derived satisfying
+requirements at all") — because leaves have no children. This is a real catalog
+design assumption: every level has a "next level down" to push the obligation to.
+A 2-level corpus (STK → SYS) where SYS leaves directly bind to code+tests has to
+either (a) introduce a SW/INT layer, (b) suppress on the parent with a rationale
+that names the leaf SYS-REQs, or (c) wait for catalog support of "leaf-terminator"
+markers. We took option (b) and named specific SYS-REQs in every suppression.
+
+**The `accepts_user_data` tag is the silent gate for `denial_of_service_resistant`.**
+The catalog's `tag_match_any: [accepts_user_data]` rule on `denial_of_service_resistant`
+is correct (a parser of trusted internal data is out of scope) but the discoverability
+gap surprised us: the obligation didn't fire when we tagged with just `parser`, only
+when we also added `accepts_user_data`. A user reading `proof catalog show
+denial_of_service_resistant` will see this in the `applies_when` block, but a user
+just running `proof audit` and tagging by intuition could miss it. Worth a doc bump
+on the catalog tagging guide.
+
+## What we suppressed honestly
+
+Three obligations don't apply to JSON at all and we suppressed them on every
+relevant STK-REQ with consistent — but specific — rationales:
+
+- **`length_prefix_validated`** (CWE-130, CWE-805, CWE-119) — "JSON is a self-delimiting
+  structural format with no length-prefix fields; jsonparser's tokenizer advances by
+  structural state machine, not by trusting a declared byte count."
+- **`polymorphic_type_whitelist`** (CWE-502, CWE-915) — "jsonparser exposes raw byte
+  slices and JSON token types; it never instantiates Go types from a discriminator
+  field, so no polymorphic deserialization attack surface exists in the API."
+- **`reference_cycle_safe`** (CWE-674, CWE-1325) — "JSON RFC 8259 has no reference or
+  alias syntax; cycles cannot exist in a well-formed JSON document and jsonparser does
+  not perform any \$ref or anchor expansion."
+
+These rationales are short, specific to JSON's actual semantics, and they cite the
+relevant authority (RFC 8259) rather than hand-waving "doesn't apply."
+
+## Coverage report excerpt
+
+After tagging and resolution, OWASP-ASVS-v4 coverage:
+
+> **OWASP Application Security Verification Standard v4.0.3** — 6 controls
+> accepted: 0  suppressed: 6  missing: 0
+> decided coverage: 100.0%  active coverage: 0.0%
+
+CWE coverage:
+
+> **Common Weakness Enumeration** — 14 controls
+> accepted: 0  suppressed: 14  missing: 0
+> decided coverage: 100.0%  active coverage: 0.0%
+
+MISRA-C coverage:
+
+> **MISRA C:2023 — Guidelines for the Use of C in Critical Systems** — 3 controls
+> accepted: 0  suppressed: 3  missing: 0
+> decided coverage: 100.0%  active coverage: 0.0%
+
+The headline metric — **decided coverage** — is the fraction of controls the project
+has explicitly addressed (either by committing or by suppressing with rationale).
+Active coverage is the stricter sub-metric: only checklist commitments count. For
+jsonparser, every framework citation is `decided` because every obligation is either
+on a checklist or carries a written suppression rationale; nothing is silently
+unaddressed.
+
+(This three-bucket layout was added in v0.3.0 — D30 / Finding 3 below — after the
+earlier "0 covered, N suppressed" framing read as misleading red on otherwise
+fully-decided projects.)
+
+The SARIF artifact ships every framework reference and now includes a `properties`
+block on each missing-coverage result with the framework's three counts and both
+percentages, so GitHub Code Scanning and GRC tooling can render decided coverage
+alongside the finding.
+
+## Findings surfaced by this dogfood (resolved in v0.3.0)
+
+Three structural improvements to the catalog were discovered by applying it to
+jsonparser, a project that is nothing like ReqProof itself, and shipped in v0.3.0:
+
+1. **Discoverability gap on `denial_of_service_resistant`**: the obligation
+   was gated on `tag_match_any: [accepts_user_data]`, which meant a parser
+   library spec author tagging only `parser` (the natural intuition) silently
+   missed a CRITICAL DoS obligation. Loosened to fire whenever `parser` is
+   tagged; trusted-input parsers may suppress with rationale.
+2. **Leaf-terminator false positive in `obligation_decomposition_complete`**:
+   leaves with obligations on their checklist were being flagged as having
+   "no derived requirements" — but leaves don't decompose further, that's the
+   point. Added leaf detection: a leaf with `implemented_by` traces passes;
+   a leaf with obligations but no `implemented_by` gets the new
+   `LeafObligationWithoutImplementation` finding instead.
+3. **Coverage report messaging** (the section above): "0 covered, N suppressed"
+   reads as 0% in the headline. Now: three buckets (accepted / suppressed /
+   missing) plus `decided coverage` and `active coverage` percentages,
+   surfacing the difference between "actively committed" and "explicitly
+   addressed".
+
+## What this proves
+
+1. **The catalog works on a project that's nothing like ReqProof itself.** jsonparser
+   is a parser library written in Go for byte-slice JSON; ReqProof is a requirements
+   verification CLI written in Go with completely different concerns. The same catalog
+   produced sensible findings on both.
+2. **Conservative tagging is correct.** Only `parser`, `deserializer`, and
+   `accepts_user_data` ever fired. The catalog never tried to suggest `crypto_*`,
+   `http_*`, `db_*`, `fs_io`, `ipc`, `scheduler`, or `websocket` — exactly as expected
+   for a parser-only library. The `polymorphic_type_whitelist` and `reference_cycle_safe`
+   suggestions appeared (because `deserializer` matched) but were honestly suppressed
+   with format-specific rationales.
+3. **Framework citations come through.** Every suppression carries the OWASP-ASVS,
+   CWE, MISRA-C, NIST-800-53, and IEC-62304 control references for the obligation
+   it's suppressing — auditors can reconstruct the framework-coverage story from the
+   spec files alone.
+4. **Suppressions are documented, distinct, and tied to evidence.** No bulk-suppression
+   with identical rationales, no `mcdc:ignore`, no `t.Skip()`. The 40 suppression
+   entries reference specific SYS-REQs, specific helpers (Get, GetString, GetUnsafeString,
+   ArrayEach, ObjectEach, Set, Delete, ParseInt, ParseFloat, ParseBoolean, ParseString),
+   and specific test files (parser_error_test.go, escape_test.go, fuzz_test.go).
+5. **The catalog corroborated existing risk intuition.** `recursion_depth_bounded` and
+   `denial_of_service_resistant` fired on the same surface area that the project's
+   ongoing oss-fuzz work has been chasing — independent confirmation that the catalog
+   is asking the right questions.
+
+## Caveats
+
+- We tagged a representative subset (the 7 STK-REQs and 7 representative SYS-REQs),
+  not all 109 SYS-REQs. Tagging deeper would surface more cascade work and isn't
+  required to demonstrate the catalog's behavior.
+- This is dogfooding, not a customer-grade audit. A real audit would derive new SYS-REQs
+  for each parent obligation rather than suppressing them; that's a follow-up.
+- 5 audit warnings remain at the project level (lint_clean, authored_delta_expected,
+  orphan_tests_clean, orphan_code_clean, verify_passes) — all pre-existing and unrelated
+  to the catalog dogfood. The pre-dogfood state already had 6 warnings; the catalog
+  work resolved one (suspect_clean is now clean) and introduced none.
+- A 2-spec-level corpus (STK → SYS, no SW or INT) collides with the catalog's "every
+  checklist needs a child satisfier" decomposition rule. We worked around it with
+  per-obligation suppression-with-rationale on the parent. A future catalog
+  enhancement (a `leaf_terminator` decision or a recognized "binds-to-code" marker
+  on a SYS-REQ) would let this kind of corpus express commitments more naturally.
+
+## Bottom line
+
+The Proof obligation-class catalog v1.0.0 produced sensible, framework-cited findings
+on a project with no overlap to ReqProof's own concerns. Where obligations applied
+(malformed-input policy, recursion-depth bounding, encoding-awareness), they pointed
+at the same code paths the project's fuzz testing is already exploring. Where
+obligations didn't apply (length-prefix validation, polymorphic-type allowlists,
+reference-cycle safety), the suppression rationales were short, specific, and tied
+to JSON's actual semantics. The case for "Proof is for any software project, not
+just our own" now has two data points instead of one.
diff --git a/docs/reqproof-application.md b/docs/reqproof-application.md
new file mode 100644
index 0000000..4d42873
--- /dev/null
+++ b/docs/reqproof-application.md
@@ -0,0 +1,280 @@
+# Applying the reqproof toolchain to jsonparser
+
+This document records the result of applying reqproof's full pipeline
+(Phases O+P+Q+R+S+T+U+X'+Y+Z+S.2c+Z.2 on `feat/z3-roadmap`,
+HEAD `33ab4e0a`) to `github.com/buger/jsonparser` on branch
+`fix-oss-fuzz-delete-leading-comma`. The headline goal was to
+demonstrate how a // reqproof:lemma directive could have surfaced
+the OSS-Fuzz Delete panic (testcase 4649128545288192, fixed in
+commit `a6c5ed3`) BEFORE the bug ever shipped.
+
+## TL;DR
+
+- 7 // reqproof:lemma directives were authored directly on production
+  code, all PROVED on Z3.
+- The Delete bug demo is a Phase Q snippet extraction. Z3 returned
+  COUNTEREXAMPLE `prevTok = -1, remainedTok = 0` for the pre-fix
+  obligation, and PROVED the post-fix obligation. This is the bug
+  the OSS-Fuzz fuzzer found, recovered via formal logic in 6ms.
+- verify-properties (SYS-REQ): 16 checks, 0 violated, 4 skipped
+  variables (orphan_no_requirement, pre-existing).
+- audit: 0 errors, 6 warnings (mostly stale authored-delta on the
+  fuzz-related files added in the same commit as the fix).
+- lemma branch coverage: 18 / 18 (100%) — every AST branch reached
+  by the SMT translation of at least one lemma is covered.
+
+## Pass 1 — Baseline pure-function lemmas
+
+Seven properties on five production functions (all on the
+`fix-oss-fuzz-delete-leading-comma` HEAD, all PROVED on Z3):
+
+| Lemma | Host | What it proves |
+|---|---|---|
+| `tokenEnd_in_range` | `parser.go::tokenEnd` | `0 <= r <= len(data)` |
+| `tokenStart_in_range` | `parser.go::tokenStart` | `0 <= r <= len(data)` |
+| `nextToken_in_range` | `parser.go::nextToken` | `-1 <= r < len(data)` |
+| `lastToken_in_range` | `parser.go::lastToken` | `-1 <= r < len(data)` |
+| `isUTF16EncodedRune_low_excluded` | `escape.go::isUTF16EncodedRune` | `r < 0xD800 ⇒ ¬isUTF16EncodedRune(r)` |
+| `isUTF16EncodedRune_high_excluded` | `escape.go::isUTF16EncodedRuneNot` (alias) | `r > 0xDFFF ⇒ ¬isUTF16EncodedRune(r)` |
+| `deleteCleanupFixed_prevTok_nonneg` | `parser_delete_snippet_proof.go::deleteCleanupFixedDereferenceObligation` | post-fix dereference obligation |
+
+Two pure-function candidates were SKIPPED with documented reasons:
+
+- `escape.go::h2I` — the body's `int(c - '0')` expression is a type
+  conversion the body translator currently classifies as an
+  unsupported function call. Phase D / E_FUNCTION_CALL widening is
+  the prerequisite.
+- `escape.go::combineUTF16Surrogates` — references package-level
+  consts `supplementalPlanesOffset`, `highSurrogateOffset`,
+  `lowSurrogateOffset` which the translator rejects as free
+  variables.
+- `bytes_unsafe.go::*` — uses `unsafe.Pointer`, an explicit
+  E_UNSAFE_PTR translator-rejection. Would need Phase P L1 opaque or
+  the safe-build-tag fallback in `bytes_safe.go`.
+
+### Authoring-time refactors made on production code
+
+To get each lemma to translate, three small refactors were applied
+to production functions WITHOUT changing observable behavior. Tests
+pass at HEAD; behavior is byte-identical.
+
+1. `tokenEnd`, `nextToken`, `lastToken`, `tokenStart` — `switch`
+   statements rewritten as `if` chains. The translator does not yet
+   support `switch` statements (E_SWITCH_NOT_SUPPORTED), and the
+   loop-translator rewrite for break/early-return cannot lower
+   switch case-bodies.
+2. `tokenEnd`, `nextToken`, `lastToken`, `tokenStart` — character
+   literals `' '`, `'\n'`, … replaced with their integer ASCII
+   values. The translator currently rejects character literals
+   inside loop bodies.
+3. `tokenEnd`, `tokenStart` — body shape changed from
+   `if cond { return i }` (conditional early-return) to
+   `if !cond { continue } return i` (guarded fall-through). The
+   first shape exposes a translator bug in the conditional
+   early-return lowering (see "Open follow-ups" below).
+
+`findTokenStart` was reverted to the original `switch` form because
+its body has TWO conditional returns; both rewrites tested still
+exposed the conditional early-return translator bug. The function
+keeps its switch and is NOT under a lemma.
+
+## Pass 2 — The Delete-bug demo (Option β: snippet extraction)
+
+The OSS-Fuzz Delete panic (testcase 4649128545288192) on input
+`,{"test":1{}` traces to `parser.go:813-820` in the pre-fix code:
+
+```go
+prevTok := lastToken(data[:keyOffset])
+// ...
+if remainedTok > -1 && remainedValue[remainedTok] == '}' && data[prevTok] == ',' {
+    newOffset = prevTok
+} else {
+    newOffset = prevTok + 1
+}
+```
+
+When `keyOffset == 0`, `data[:0]` is empty so `lastToken` returns
+`-1`, and `data[prevTok] == ','` panics on the negative index.
+
+### Why direct annotation (Option α) failed
+
+Annotating `Delete` itself with `// reqproof:requires prevTok > -1`
+is not viable today. Three independent gaps:
+
+- `Delete` calls helpers (`searchKeys`, `internalGet`,
+  `findTokenStart`, …) that themselves use slice expressions
+  `data[:keyOffset]` (`E_SLICE_EXPR`) and switch statements
+  (`E_SWITCH_NOT_SUPPORTED`).
+- `Delete` mutates a slice via `append(dataCopy[:newOffset],
+  dataCopy[endOffset:]...)`, which the body translator rejects.
+- Even if the translation worked, runtime panics aren't a
+  first-class output of the SMT translation — Phase AA "verify-safety"
+  (planned) is what would emit auto-OOB obligations.
+
+### What worked: Option β — abstract snippet under build tag
+
+`parser_delete_snippet_proof.go` (build-tagged
+`reqproof_proof`) extracts the offending block as two helpers:
+
+- `deleteCleanupBuggyDereferenceObligation(prevTok, remainedTok int) bool`
+  encodes the dereference obligation of the **pre-fix** branch shape
+  (data[prevTok] is reached whenever remainedTok > -1, so
+  prevTok >= 0 must hold there).
+- `deleteCleanupFixedDereferenceObligation(prevTok, remainedTok int) bool`
+  encodes the **post-fix** branch shape (the new `prevTok > -1`
+  guard fronts every dereference).
+
+Two lemmas certify these:
+
+```go
+// reqproof:lemma deleteCleanupBuggy_prevTok_nonneg_falsifiable func(prevTok, remainedTok int) bool {
+//   return deleteCleanupBuggyDereferenceObligation(prevTok, remainedTok)
+// }
+```
+
+```go
+// reqproof:lemma deleteCleanupFixed_prevTok_nonneg func(prevTok, remainedTok int) bool {
+//   return deleteCleanupFixedDereferenceObligation(prevTok, remainedTok)
+// }
+```
+
+### Result (verbatim from `proof verify-lemma --solver z3 --tags reqproof_proof`)
+
+```
+[ce] deleteCleanupBuggy_prevTok_nonneg_falsifiable COUNTEREXAMPLE (z3, 6ms)
+    counterexample:
+      remainedTok = 0
+      prevTok = -1
+[ok] deleteCleanupFixed_prevTok_nonneg PROVED (z3, 6ms)
+```
+
+This IS the OSS-Fuzz bug, surfaced as a Z3 counterexample in 6ms.
+The `prevTok = -1` value is exactly what `lastToken(data[:0])`
+returns; `remainedTok = 0` is the value of `nextToken` on the
+non-empty `remainedValue` suffix.
+
+A unit test author reading this counterexample would translate it
+back to a JSON input by:
+- choosing any `keyOffset == 0` ⇒ `prevTok = -1`,
+- arranging non-empty `data[endOffset:]` whose first non-whitespace
+  byte triggers the pre-fix branch.
+
+`,{"test":1{}` (the OSS-Fuzz repro) is one such input.
+
+## Pass 3 — verify-properties + audit
+
+### verify-properties (SYS-REQ)
+
+```
+Total Variables:                               226
+Variables with Data Constraints (Authored):    4
+Total Checks:                                  16
+Violated:                                      0
+Skipped (delta):                               0
+Skipped Variables (orphan_no_requirement):     4
+```
+
+The four orphan_no_requirement variables (`array_index_is_in_bounds`,
+`array_index_is_out_of_bounds`, `set_called_without_path`,
+`set_path_is_provided`) are pre-existing — no SYS-REQ in the
+`parser` component references them, so behavioral_implication
+proofs do not fire (completeness/exclusivity still ran and proved).
+
+### audit
+
+```
+Errors: 0  Warnings: 6
+Assurance: L3 (1 component)
+```
+
+Findings:
+
+1. `authored_delta_expected` — 6 traced production files lack a
+   current no-authored-change review. These are exactly the files
+   touched by the fix commit and the lemma-authoring refactors;
+   the warning is expected on a feature branch.
+2. `lint_clean` / `orphan_code_clean` — 21 + 7 untraced symbols in
+   `fuzz_native_test.go` and the new snippet file. The fuzz wrappers
+   were added in the same commit as the fix; tracing them is a
+   separate task.
+3. `orphan_tests_clean` — 14 of 285 test functions lack a
+   `// Verifies:` annotation (mostly the new fuzz wrappers).
+4. `suspect_clean` — 107 suspect links; pre-existing.
+5. `verify_passes` — 1 warning (the lint warning above).
+
+No Errors. The branch is healthy at the L3 assurance level.
+
+## Pass 4 — Lemma branch coverage
+
+```
+Coverage: 18 branches, 18 covered (100%)
+every recorded branch is covered by at least one lemma.
+```
+
+Every AST branch the SMT translation of any lemma reached is
+covered. The 18-branch denominator counts only the branches that
+the translator visited (Phase Y's recorder fires inside body
+translation), so the coverage scope is "the production code reached
+by these 7 proved lemmas". Production functions whose lemmas are
+blocked by translator gaps (e.g. `findTokenStart`, `Delete`,
+`searchKeys`, `escape.go::Unescape`) do not appear in the
+denominator. Phase AA + S.2c.3 + Phase D widening would expand
+that denominator significantly.
+
+## Pass 5 — Open follow-ups (translator gaps surfaced)
+
+These are real reqproof gaps, surfaced by attempting to apply the
+toolchain end-to-end on a small library. They are filed here so the
+reqproof team can pick them up:
+
+1. **Conditional early-return translator bug**. Loop bodies of the
+   shape `if cond { return X }` followed by code emit broken SMT
+   referencing `__early_val$N$M` outside the let-binding that defines
+   it. Manifests as Z3 errors `unknown constant __early_val$1$1` at
+   the prelude line. Workaround: rewrite as guarded fall-through
+   `if !cond { continue } return X`, but THIS PATTERN is itself
+   sometimes broken when there are TWO conditional returns inside
+   the loop (`findTokenStart`). Phase S.2c.4 follow-up.
+2. **`E_SWITCH_NOT_SUPPORTED`**. `switch` statements inside loop
+   bodies (and elsewhere) need a lowering. Many idiomatic Go
+   patterns (jsonparser's tokenizer is a representative example)
+   use switch; refactoring is invasive.
+3. **Character literals inside loop bodies**. The translator rejects
+   `c == ' '` style comparisons; users must replace with the integer
+   ASCII value. Trivial to author once known but a friction point.
+4. **`E_FUNCTION_CALL` for type conversions**. `int(c)` on a `byte`
+   is rejected as an unsupported function call even though the
+   conversion is a no-op at the SMT-Int level. Phase D widening.
+5. **`E_SLICE_EXPR` for slice expressions**. Disqualifies any
+   function whose body uses `data[:i]` / `data[i:]`. Workaround
+   exists (recursive helper + `// reqproof:decreases`) but it is a
+   significant authoring lift for non-trivial functions.
+6. **Free package constants**. `combineUTF16Surrogates` references
+   `supplementalPlanesOffset`, etc. The translator should inline
+   const declarations.
+7. **Multi-lemma single host**. Two consecutive
+   `// reqproof:lemma` directives on the same function host
+   silently dropped the second lemma during scanning. Workaround:
+   put the second lemma on a thin alias function (we did this for
+   `isUTF16EncodedRune_high_excluded`). Phase R follow-up.
+8. **Phase AA — auto-OOB obligations**. The Delete bug is a runtime
+   index-out-of-range panic. With Phase AA we would not need the
+   snippet at all — every `data[i]` read in `Delete` would carry
+   an automatic `0 <= i < len(data)` proof obligation, and the
+   pre-fix code would fail to verify with the SAME counterexample
+   (`prevTok = -1`).
+
+## Recommendation for the jsonparser team
+
+1. The seven proved lemmas are cheap regressions: 7 PROVED in <60ms
+   total Z3 time, cached at `.proof/lemma-cache.json`. CI should run
+   `proof verify-lemma --solver z3 --tags reqproof_proof ./...` as
+   part of the existing test job. A future code change that
+   accidentally removes the `prevTok > -1` guard from Delete will
+   re-trigger the COUNTEREXAMPLE on
+   `deleteCleanupFixed_prevTok_nonneg`, and CI will fail.
+2. The snippet file `parser_delete_snippet_proof.go` is a
+   regression test for the bug class. Adding similar snippets for
+   any future Delete/Set OOB fix is a small, repeatable pattern.
+3. Once Phase AA lands, the snippet can be retired in favor of an
+   automatic OOB obligation on the production `Delete` body.
diff --git a/docs/reqproof-item3-application.md b/docs/reqproof-item3-application.md
new file mode 100644
index 0000000..9e216c4
--- /dev/null
+++ b/docs/reqproof-item3-application.md
@@ -0,0 +1,174 @@
+# Reqproof Item #3 — Application to jsonparser
+
+This doc records the dogfooding result of applying reqproof's
+`feat/z3-roadmap` items #1 (path-conditions), #2 (variadic +
+multi-return), and Phase AA verify-safety to the jsonparser package.
+
+- Reqproof revision: `feat/z3-roadmap` HEAD `d17622a9`.
+- jsonparser revision: `fix-oss-fuzz-delete-leading-comma` HEAD `80cf537`.
+- Date: 2026-05-01.
+
+## Pass 1 — lemma corpus re-run with the new toolchain
+
+Command:
+
+```sh
+go run ./cmd/proof verify-lemma --solver z3 --solver z3,cvc5 \
+    --tags reqproof_proof --no-cache /Users/leonidbugaev/go/src/jsonparser/...
+```
+
+Result (pre-item-#3 corpus, 23 lemmas):
+
+| verdict        | count |
+| -------------- | ----- |
+| PROVED         | 22    |
+| COUNTEREXAMPLE | 1     |
+| TIMEOUT        | 0     |
+| UNKNOWN        | 0     |
+| TRANSLATION    | 0     |
+
+The single COUNTEREXAMPLE is the deliberately-falsifiable
+`deleteCleanupBuggy_prevTok_nonneg_falsifiable` lemma in
+`parser_delete_snippet_proof.go` (the OSS-Fuzz Delete pre-fix
+witness). All 22 PROVED verdicts preserved verbatim under the
+new translator. Baseline retained.
+
+## Pass 2 — new lemmas exercising items #1 and #2
+
+Added in `parser_item3_lemmas_proof.go` (build tag
+`reqproof_proof`, anchored to no-op predicates because lemma
+directives must attach to a declaration with a return slot):
+
+### Item #1 (path-conditions) lemmas — 5 new, all PROVED
+
+| lemma                                              | shape                                                   | verdict |
+| -------------------------------------------------- | ------------------------------------------------------- | ------- |
+| `tokenEnd_path_indexable_implies_nonneg`           | `if r < len(data) { r >= 0 }` over `tokenEnd`           | PROVED  |
+| `nextToken_path_indexable_implies_lt_len`          | `if r >= 0 { r < len(data) }` over `nextToken`          | PROVED  |
+| `lastToken_path_indexable_implies_lt_len`          | `if r >= 0 { r < len(data) }` over `lastToken`          | PROVED  |
+| `tokenStart_path_indexable_when_nonempty`          | `if len(data)>0 { 0<=r<len(data) } else r==0`           | PROVED  |
+| `h2I_nonneg_implies_le_15`                         | `if r >= 0 { r <= 15 }` over `h2I`                      | PROVED  |
+
+These claims could be re-stated as plain conjunctions before item
+#1, but the natural "if-guard then conclusion" shape is what item
+#1 is supposed to make first-class — and it does.
+
+### Item #2 (variadic) lemmas — 2 new, all PROVED
+
+A small helper `keysCount(keys ...string) int` was added (not used
+by production code, build-tag-gated). Item #2's variadic-callee
+support is what allows this signature to translate at all.
+
+| lemma                          | claim                              | verdict |
+| ------------------------------ | ---------------------------------- | ------- |
+| `keysCount_matches_len`        | `keysCount(keys...) == len(keys)`  | PROVED  |
+| `keysCount_nonneg`             | `keysCount(keys...) >= 0`          | PROVED  |
+
+### Lemma corpus growth
+
+23 → 30 lemmas. 22 PROVED → 29 PROVED. The single COUNTEREXAMPLE
+is preserved at the same site. Net `+7` new PROVED lemmas, zero
+regressions, zero translation errors after working around the
+tuple-sort issue described below.
+
+### Translator gap surfaced while authoring
+
+The first attempt at the item-#2 demonstration was a helper with
+*two* return slots:
+
+```go
+func keysSummary(keys ...string) (int, bool) { ... }
+```
+
+With this declaration in the package, every other lemma
+(including the 22-lemma baseline) regressed from PROVED to
+UNKNOWN with `error "Invalid function definition: unknown sort
+'gosmt_tuple_644eb3b2'"`. The synthesized SMT tuple sort for
+`(int, bool)` was emitted into the package-wide preamble but
+not declared, poisoning every adjacent lemma's solver context.
+
+**Workaround**: collapse the helper to a single-return value.
+
+**Follow-up for reqproof**: tuple sorts produced for
+multi-return helpers must be declared (or scoped per-lemma) so
+that adding one such helper to a package does not break every
+other lemma in that package. Item #2 lands the *callee* side of
+multi-return cleanly when the lemma directly invokes the helper,
+but a *passive* helper sitting in the same package is enough to
+trip the preamble.
+
+### Translator gaps still blocking — bigger candidates
+
+| function    | gap                                                       | items #1/#2 unblock? |
+| ----------- | --------------------------------------------------------- | -------------------- |
+| `Delete`    | E_EARLY_RETURN_NO_ELSE at line 800 (`if !array { ... }`)  | no (separate gap)    |
+| `Get`       | unsupported type `ValueType` (named alias)                | no                   |
+| `GetString` | `_, _, := ...` multi-target assign at consumer site       | partial (#2 fixes producer side; consumer side is a distinct E_MULTI_TARGET_ASSIGN) |
+| `GetInt`/`GetFloat`/`GetBoolean`/`GetUnsafeString` | same as `GetString` | partial |
+| `searchKeys` | E_RECURSION_NO_DECREASES                                 | no                   |
+| `stringEnd`, `blockEnd`, `tokenStart` (loops in body), `nextToken` (loops) | E_FOR_LOOP_NO_INVARIANT | no |
+| `Set`       | E_TYPE_MISMATCH on Seq Int return                         | no                   |
+| `bytes_safe.parseFloat` | E_MULTIPLE_RETURN_VALUES (return single from 2-return) | partial |
+
+The two highest-leverage candidate functions for the next
+roadmap item — `Delete` and `GetString` — are *both* still
+blocked, but on gaps distinct from #1/#2. Item #2 lands the
+producer side of multi-return; the consumer side
+(`a, b, c, _ := f(...)`) is a separate E_MULTI_TARGET_ASSIGN.
+
+## Pass 3 — verify-safety
+
+Command:
+
+```sh
+go run ./cmd/proof verify-safety /Users/leonidbugaev/go/src/jsonparser/
+```
+
+| metric                | value |
+| --------------------- | ----- |
+| functions scanned     | 11    |
+| functions skipped     | 62    |
+| findings (E_INDEX_OOB) | 0    |
+| findings (E_DIV_BY_ZERO) | 0  |
+
+Zero safety findings. The 11 scannable functions are the small
+arithmetic helpers (`h2I`, `isUTF16EncodedRune`,
+`isUTF16EncodedRuneNot`, the `anchor_*` no-op predicates, the two
+`deleteCleanup*Obligation` helpers, `keysCount`,
+`deleteCleanupBuggyFalsifyingWitness`). All are pure arithmetic
+or pure boolean and have no slice indexing or division.
+
+### Why the OSS-Fuzz Delete bug does NOT surface here
+
+verify-safety would surface the pre-fix `data[prevTok]` panic
+*if `Delete` translated*. It does not — the function is rejected
+at translation time with E_EARLY_RETURN_NO_ELSE on the `if
+!array { ... }` block. The bug surfaces instead through the
+purpose-built `parser_delete_snippet_proof.go` lemma
+(`deleteCleanupBuggy_prevTok_nonneg_falsifiable`), which abstracts
+the panic site as a parameterized integer obligation. That
+lemma's COUNTEREXAMPLE verdict (`prevTok=-1, remainedTok=0`) is
+the same machine-checked witness the OSS-Fuzz testcase would
+produce, encoded against the pre-fix branch shape.
+
+### Triage
+
+Nothing to triage — zero findings. No new real bugs found.
+
+## Headline
+
+- Pre-existing 22 PROVED + 1 COUNTEREXAMPLE corpus survives
+  unchanged under the new translator.
+- 7 new PROVED lemmas, 5 of them path-condition-shaped (item #1)
+  and 2 of them variadic-callee-shaped (item #2).
+- One new translator follow-up identified: tuple-sort preamble
+  scoping when a multi-return helper sits passively in the
+  package.
+- verify-safety continues to be useful only on functions that
+  pass the dispatcher; jsonparser's loop-heavy core (Delete,
+  Get-family, searchKeys) remains out of reach until
+  loop-recursion translation or for-loop invariant inference
+  lands. None of the items in this milestone moved that frontier.
+- No new real bugs found beyond the already-known OSS-Fuzz Delete
+  pre-fix witness, which continues to surface as a
+  COUNTEREXAMPLE on its dedicated snippet lemma.
diff --git a/escape.go b/escape.go
index 62be30d..7bc0681 100644
--- a/escape.go
+++ b/escape.go
@@ -15,20 +15,57 @@ const lowSurrogateOffset = 0xDC00
 const basicMultilingualPlaneReservedOffset = 0xDFFF
 const basicMultilingualPlaneOffset = 0xFFFF
 
+// NOTE: combineUTF16Surrogates is blocked by an unsupported `<<` shift op
+// in the translator (Phase T.* gap, beyond #1/#2/#5). Even though Fix #6
+// resolves the package-const references in this body, the shift remains
+// untranslated, so no lemma is attached here.
 func combineUTF16Surrogates(high, low rune) rune {
 	return supplementalPlanesOffset + (high-highSurrogateOffset)<<10 + (low - lowSurrogateOffset)
 }
 
 const badHex = -1
 
+// reqproof:lemma h2I_range func(c byte) bool {
+//   r := h2I(c)
+//   return r == -1 || (r >= 0 && r <= 15)
+// }
+// reqproof:lemma h2I_decimal_digit func(c byte) bool {
+//   if c < '0' || c > '9' { return true }
+//   r := h2I(c)
+//   return r >= 0 && r <= 9
+// }
+// reqproof:lemma h2I_uppercase_hex func(c byte) bool {
+//   if c < 'A' || c > 'F' { return true }
+//   r := h2I(c)
+//   return r >= 10 && r <= 15
+// }
+// reqproof:lemma h2I_lowercase_hex func(c byte) bool {
+//   if c < 'a' || c > 'f' { return true }
+//   r := h2I(c)
+//   return r >= 10 && r <= 15
+// }
+// reqproof:lemma h2I_nondigit_is_badhex func(c byte) bool {
+//   if c >= '0' && c <= '9' { return true }
+//   if c >= 'A' && c <= 'F' { return true }
+//   if c >= 'a' && c <= 'f' { return true }
+//   return h2I(c) == badHex
+// }
+// reqproof:lemma h2I_nonneg_implies_le_15 func(c byte) bool {
+//   r := h2I(c)
+//   if r >= 0 {
+//     return r <= 15
+//   }
+//   return true
+// }
 func h2I(c byte) int {
-	switch {
-	case c >= '0' && c <= '9':
-		return int(c - '0')
-	case c >= 'A' && c <= 'F':
-		return int(c - 'A' + 10)
-	case c >= 'a' && c <= 'f':
-		return int(c - 'a' + 10)
+	if c >= 48 && c <= 57 { // '0'..'9'
+		return int(c - 48)
+	}
+	if c >= 65 && c <= 70 { // 'A'..'F'
+		return int(c-65) + 10
+	}
+	if c >= 97 && c <= 102 { // 'a'..'f'
+		return int(c-97) + 10
 	}
 	return badHex
 }
@@ -56,8 +93,31 @@ func decodeSingleUnicodeEscape(in []byte) (rune, bool) {
 // isUTF16EncodedRune checks if a rune is in the range for non-BMP characters,
 // which is used to describe UTF16 chars.
 // Source: https://en.wikipedia.org/wiki/Plane_(Unicode)#Basic_Multilingual_Plane
+//
+// reqproof:lemma isUTF16EncodedRune_low_excluded func(r rune) bool {
+//   return !(r < 0xD800) || !isUTF16EncodedRune(r)
+// }
+// reqproof:lemma isUTF16EncodedRune_const_high_bound func(r rune) bool {
+//   // Fix #6: package-level const highSurrogateOffset (= 0xD800) now
+//   // resolves at translation time. Below the high surrogate offset
+//   // means definitely outside the UTF-16 surrogate range.
+//   return !(r < highSurrogateOffset) || !isUTF16EncodedRune(r)
+// }
+// reqproof:lemma isUTF16EncodedRune_const_bmp_bound func(r rune) bool {
+//   // Fix #6: package-level const basicMultilingualPlaneReservedOffset (= 0xDFFF).
+//   // Above the BMP-reserved offset means outside the UTF-16 surrogate range.
+//   return !(r > basicMultilingualPlaneReservedOffset) || !isUTF16EncodedRune(r)
+// }
 func isUTF16EncodedRune(r rune) bool {
-	return highSurrogateOffset <= r && r <= basicMultilingualPlaneReservedOffset
+	return 0xD800 <= r && r <= 0xDFFF
+}
+
+// isUTF16EncodedRuneNot is a thin alias hosting an additional lemma.
+// reqproof:lemma isUTF16EncodedRune_high_excluded func(r rune) bool {
+//   return !(r > 0xDFFF) || !isUTF16EncodedRuneNot(r)
+// }
+func isUTF16EncodedRuneNot(r rune) bool {
+	return isUTF16EncodedRune(r)
 }
 
 func decodeUnicodeEscape(in []byte) (rune, int) {
diff --git a/fuzz_native_test.go b/fuzz_native_test.go
new file mode 100644
index 0000000..f3fdc97
--- /dev/null
+++ b/fuzz_native_test.go
@@ -0,0 +1,197 @@
+// Native Go fuzz wrappers around the OSS-Fuzz targets in fuzz.go so they can
+// be driven by `go test -fuzz` locally. Panics are recovered and recorded
+// (deduplicated by panic msg + innermost parser frame) under
+// fuzz_results/crashes/, so a single fuzz run keeps exploring after the first
+// crash instead of stopping. See run_fuzz_campaign.sh for batch usage.
+package jsonparser
+
+import (
+	"crypto/sha256"
+	"encoding/base64"
+	"encoding/hex"
+	"encoding/json"
+	"fmt"
+	"os"
+	"path/filepath"
+	"runtime/debug"
+	"strings"
+	"testing"
+)
+
+var nativeFuzzSeeds = []string{
+	"{}",
+	"[]",
+	`{"test":1}`,
+	`{"test":"hello","other":2}`,
+	`{"a":{"test":[1,2,3]},"test":null}`,
+	`{"test":{"nested":{"test":true}}}`,
+	`[1,2,3,4]`,
+	`{"test":}`,
+	`{"x":"test"}`,
+	`{"test":"\""}`,
+	`{"test":1.5e10}`,
+	`{"test":-0.0}`,
+	`{"test":true,"a":false,"b":null}`,
+	`,{"test":1{}`,
+	`,""{"test":0}`,
+	`{"name":"x","order":1,"nested":{"a":1,"b":2,"nested3":{"b":3}},"nested2":{"a":4},"arr":[{"b":5},{"b":6}],"arrInt":[0,1,2,3,4,5,6]}`,
+	"",
+}
+
+func addSeeds(f *testing.F) {
+	for _, s := range nativeFuzzSeeds {
+		f.Add([]byte(s))
+	}
+}
+
+var fuzzCrashDir = func() string {
+	d := os.Getenv("FUZZ_CRASH_DIR")
+	if d == "" {
+		d = "fuzz_results/crashes"
+	}
+	_ = os.MkdirAll(d, 0o755)
+	return d
+}()
+
+func crashSignature(panicMsg string, stack []byte) string {
+	var key strings.Builder
+	key.WriteString(panicMsg)
+	for _, line := range strings.Split(string(stack), "\n") {
+		if strings.Contains(line, "github.com/buger/jsonparser/") &&
+			!strings.Contains(line, "fuzz_native_test.go") &&
+			!strings.Contains(line, "/fuzz.go:") {
+			key.WriteString("|")
+			key.WriteString(strings.TrimSpace(line))
+			break
+		}
+	}
+	sum := sha256.Sum256([]byte(key.String()))
+	return hex.EncodeToString(sum[:])[:12]
+}
+
+func recordCrash(target string, panicVal interface{}, stack, input []byte) {
+	panicMsg := fmt.Sprintf("%v", panicVal)
+	sig := crashSignature(panicMsg, stack)
+	fname := filepath.Join(fuzzCrashDir, target+"_"+sig+".json")
+	f, err := os.OpenFile(fname, os.O_WRONLY|os.O_CREATE|os.O_EXCL, 0o644)
+	if err != nil {
+		return
+	}
+	defer f.Close()
+	inputCopy := make([]byte, len(input))
+	copy(inputCopy, input)
+	_ = json.NewEncoder(f).Encode(map[string]interface{}{
+		"target":    target,
+		"sig":       sig,
+		"panic":     panicMsg,
+		"stack":     string(stack),
+		"input_b64": base64.StdEncoding.EncodeToString(inputCopy),
+	})
+}
+
+func runWithCapture(target string, data []byte, fn func([]byte)) {
+	defer func() {
+		if r := recover(); r != nil {
+			recordCrash(target, r, debug.Stack(), data)
+		}
+	}()
+	fn(data)
+}
+
+func FuzzDeleteNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzDeleteNative", data, func(d []byte) { _ = FuzzDelete(d) })
+	})
+}
+
+func FuzzParseStringNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzParseStringNative", data, func(d []byte) { _ = FuzzParseString(d) })
+	})
+}
+
+func FuzzEachKeyNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzEachKeyNative", data, func(d []byte) { _ = FuzzEachKey(d) })
+	})
+}
+
+func FuzzSetNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzSetNative", data, func(d []byte) { _ = FuzzSet(d) })
+	})
+}
+
+func FuzzObjectEachNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzObjectEachNative", data, func(d []byte) { _ = FuzzObjectEach(d) })
+	})
+}
+
+func FuzzParseFloatNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzParseFloatNative", data, func(d []byte) { _ = FuzzParseFloat(d) })
+	})
+}
+
+func FuzzParseIntNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzParseIntNative", data, func(d []byte) { _ = FuzzParseInt(d) })
+	})
+}
+
+func FuzzParseBoolNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzParseBoolNative", data, func(d []byte) { _ = FuzzParseBool(d) })
+	})
+}
+
+func FuzzTokenStartNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzTokenStartNative", data, func(d []byte) { _ = FuzzTokenStart(d) })
+	})
+}
+
+func FuzzGetStringNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzGetStringNative", data, func(d []byte) { _ = FuzzGetString(d) })
+	})
+}
+
+func FuzzGetFloatNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzGetFloatNative", data, func(d []byte) { _ = FuzzGetFloat(d) })
+	})
+}
+
+func FuzzGetIntNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzGetIntNative", data, func(d []byte) { _ = FuzzGetInt(d) })
+	})
+}
+
+func FuzzGetBooleanNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzGetBooleanNative", data, func(d []byte) { _ = FuzzGetBoolean(d) })
+	})
+}
+
+func FuzzGetUnsafeStringNative(f *testing.F) {
+	addSeeds(f)
+	f.Fuzz(func(t *testing.T, data []byte) {
+		runWithCapture("FuzzGetUnsafeStringNative", data, func(d []byte) { _ = FuzzGetUnsafeString(d) })
+	})
+}
diff --git a/parser.go b/parser.go
index d8df167..b0d425b 100644
--- a/parser.go
+++ b/parser.go
@@ -26,18 +26,43 @@ var (
 const unescapeStackBufSize = 64
 
 // SYS-REQ-044
+// reqproof:lemma tokenEnd_in_range func(data []byte) bool {
+//   r := tokenEnd(data)
+//   return r >= 0 && r <= len(data)
+// }
+// reqproof:lemma tokenEnd_nonneg func(data []byte) bool {
+//   // tokenEnd never signals via a negative sentinel — the empty-input
+//   // path returns len(data)==0 (still nonneg), and any hit returns the
+//   // loop index (also nonneg).
+//   return tokenEnd(data) >= 0
+// }
+// reqproof:lemma tokenEnd_empty_zero func(data []byte) bool {
+//   return !(len(data) == 0) || tokenEnd(data) == 0
+// }
+// reqproof:lemma tokenEnd_path_indexable_implies_nonneg func(data []byte) bool {
+//   r := tokenEnd(data)
+//   if r < len(data) {
+//     return r >= 0
+//   }
+//   return true
+// }
 func tokenEnd(data []byte) int {
 	for i, c := range data {
-		switch c {
-		case ' ', '\n', '\r', '\t', ',', '}', ']':
-			return i
+		// reqproof:invariant 0 <= i
+		// reqproof:invariant i <= len(data)
+		if c != 32 && c != 10 && c != 13 && c != 9 && c != 44 && c != 125 && c != 93 {
+			continue
 		}
+		return i
 	}
 
 	return len(data)
 }
 
 // SYS-REQ-001
+// NOTE: findTokenStart's two-conditional-return body shape exposes
+// the translator's __early_val scoping bug; we leave it without an
+// in-range lemma. (Documented as a Phase S.2c.4 follow-up.)
 func findTokenStart(data []byte, token byte) int {
 	for i := len(data) - 1; i >= 0; i-- {
 		switch data[i] {
@@ -123,12 +148,32 @@ func findKeyStart(data []byte, key string) (int, error) {
 }
 
 // SYS-REQ-001
+// reqproof:lemma tokenStart_in_range func(data []byte) bool {
+//   r := tokenStart(data)
+//   return r >= 0 && r <= len(data)
+// }
+// reqproof:lemma tokenStart_nonneg func(data []byte) bool {
+//   return tokenStart(data) >= 0
+// }
+// reqproof:lemma tokenStart_empty_zero func(data []byte) bool {
+//   return !(len(data) == 0) || tokenStart(data) == 0
+// }
+// reqproof:lemma tokenStart_path_indexable_when_nonempty func(data []byte) bool {
+//   r := tokenStart(data)
+//   if len(data) > 0 {
+//     return r >= 0 && r < len(data)
+//   }
+//   return r == 0
+// }
 func tokenStart(data []byte) int {
 	for i := len(data) - 1; i >= 0; i-- {
-		switch data[i] {
-		case '\n', '\r', '\t', ',', '{', '[':
-			return i
+		// reqproof:invariant -1 <= i
+		// reqproof:invariant i < len(data)
+		c := data[i]
+		if c != 10 && c != 13 && c != 9 && c != 44 && c != 123 && c != 91 {
+			continue
 		}
+		return i
 	}
 
 	return 0
@@ -136,14 +181,33 @@ func tokenStart(data []byte) int {
 
 // SYS-REQ-001
 // Find position of next character which is not whitespace
+// reqproof:lemma nextToken_in_range func(data []byte) bool {
+//   r := nextToken(data)
+//   return r >= -1 && r < len(data)
+// }
+// reqproof:lemma nextToken_empty_neg func(data []byte) bool {
+//   return !(len(data) == 0) || nextToken(data) == -1
+// }
+// reqproof:lemma nextToken_signed_disjoint func(data []byte) bool {
+//   r := nextToken(data)
+//   // Result is either -1 (sentinel) or a non-negative index — never -2 or below
+//   return r == -1 || r >= 0
+// }
+// reqproof:lemma nextToken_path_indexable_implies_lt_len func(data []byte) bool {
+//   r := nextToken(data)
+//   if r >= 0 {
+//     return r < len(data)
+//   }
+//   return true
+// }
 func nextToken(data []byte) int {
 	for i, c := range data {
-		switch c {
-		case ' ', '\n', '\r', '\t':
+		// reqproof:invariant 0 <= i
+		// reqproof:invariant i <= len(data)
+		if c == ' ' || c == '\n' || c == '\r' || c == '\t' {
 			continue
-		default:
-			return i
 		}
+		return i
 	}
 
 	return -1
@@ -151,14 +215,34 @@ func nextToken(data []byte) int {
 
 // SYS-REQ-001
 // Find position of last character which is not whitespace
+// reqproof:lemma lastToken_in_range func(data []byte) bool {
+//   r := lastToken(data)
+//   return r >= -1 && r < len(data)
+// }
+// reqproof:lemma lastToken_empty_neg func(data []byte) bool {
+//   return !(len(data) == 0) || lastToken(data) == -1
+// }
+// reqproof:lemma lastToken_signed_disjoint func(data []byte) bool {
+//   r := lastToken(data)
+//   // Result is either -1 (sentinel) or a non-negative index — never -2 or below
+//   return r == -1 || r >= 0
+// }
+// reqproof:lemma lastToken_path_indexable_implies_lt_len func(data []byte) bool {
+//   r := lastToken(data)
+//   if r >= 0 {
+//     return r < len(data)
+//   }
+//   return true
+// }
 func lastToken(data []byte) int {
 	for i := len(data) - 1; i >= 0; i-- {
-		switch data[i] {
-		case ' ', '\n', '\r', '\t':
+		// reqproof:invariant -1 <= i
+		// reqproof:invariant i < len(data)
+		c := data[i]
+		if c == ' ' || c == '\n' || c == '\r' || c == '\t' {
 			continue
-		default:
-			return i
 		}
+		return i
 	}
 
 	return -1
@@ -813,10 +897,12 @@ func Delete(data []byte, keys ...string) []byte {
 	remainedTok := nextToken(remainedValue)
 
 	var newOffset int
-	if remainedTok > -1 && remainedValue[remainedTok] == '}' && data[prevTok] == ',' {
+	if prevTok > -1 && remainedTok > -1 && remainedValue[remainedTok] == '}' && data[prevTok] == ',' {
 		newOffset = prevTok
-	} else {
+	} else if prevTok > -1 {
 		newOffset = prevTok + 1
+	} else {
+		newOffset = 0
 	}
 
 	// We have to make a copy here if we don't want to mangle the original data, because byte slices are
@@ -1366,3 +1452,64 @@ func ParseInt(b []byte) (int64, error) {
 		return v, nil
 	}
 }
+
+// --- reqproof verification helpers ---
+//
+// The functions below are callable but only used by reqproof
+// verification. They abstract control-flow shapes inside Delete's
+// cleanup block (which itself doesn't translate yet because of slice
+// expressions and early returns) and exercise the variadic translator
+// path. Keeping them in the production file (rather than a separate
+// _proof.go) means lemma directives sit next to the production code
+// they characterize.
+
+// deleteCleanupBuggyDereferenceObligation encodes the implicit
+// obligation of the pre-fix Delete block (parser.go pre-a6c5ed3,
+// lines 813-820): the data[prevTok] dereference happens whenever
+// remainedTok > -1, so safety requires prevTok >= 0 in that case.
+// On the buggy model the obligation is FALSIFIABLE — Z3 surfaces
+// (prevTok = -1, remainedTok = 0), the OSS-Fuzz witness shape.
+//
+// reqproof:lemma deleteCleanupBuggy_prevTok_nonneg_falsifiable func(prevTok, remainedTok int) bool {
+//   return deleteCleanupBuggyDereferenceObligation(prevTok, remainedTok)
+// }
+func deleteCleanupBuggyDereferenceObligation(prevTok, remainedTok int) bool {
+	if remainedTok >= 0 {
+		return prevTok >= 0
+	}
+	return true
+}
+
+// deleteCleanupFixedDereferenceObligation encodes the post-fix block
+// (parser.go HEAD a6c5ed3, lines 815-822). The new prevTok > -1
+// guard fronts every dereference, so the obligation holds.
+//
+// reqproof:lemma deleteCleanupFixed_prevTok_nonneg func(prevTok, remainedTok int) bool {
+//   return !(prevTok >= 0 && remainedTok >= 0) || prevTok >= 0
+// }
+func deleteCleanupFixedDereferenceObligation(prevTok, remainedTok int) bool {
+	return !(prevTok >= 0 && remainedTok >= 0) || prevTok >= 0
+}
+
+// deleteCleanupBuggyFalsifyingWitness documents the falsifying input
+// that the COUNTEREXAMPLE verdict surfaces: prevTok = -1, remainedTok = 0.
+// Plain Go function (no lemma) — the machine-checked counterexample
+// already proves it; this helper exists for documentation only.
+func deleteCleanupBuggyFalsifyingWitness() bool {
+	return !deleteCleanupBuggyDereferenceObligation(-1, 0)
+}
+
+// keysCount exercises the translator's variadic ...string parameter
+// (Item #2). No production caller exists; the helper lives here so
+// the variadic-passthrough lemma stays near the JSON-key handling
+// code it's a stand-in for.
+//
+// reqproof:lemma keysCount_matches_len func(keys []string) bool {
+//   return keysCount(keys...) == len(keys)
+// }
+// reqproof:lemma keysCount_nonneg func(keys []string) bool {
+//   return keysCount(keys...) >= 0
+// }
+func keysCount(keys ...string) int {
+	return len(keys)
+}
diff --git a/parser_test.go b/parser_test.go
index 795b470..c7bb1c7 100644
--- a/parser_test.go
+++ b/parser_test.go
@@ -248,6 +248,23 @@ var deleteTests = []DeleteTest{
 		path: []string{"a", "b"},
 		data: `{"a":{"b":  `,
 	},
+	{
+		// OSS-Fuzz testcase 4649128545288192: leading garbage comma
+		// caused findTokenStart to return offset 0, which then made the
+		// trailing-comma cleanup branch reassign keyOffset=0, which made
+		// lastToken(data[:0]) return -1, which made data[prevTok] panic
+		// with "index out of range [-1]" at parser.go.
+		desc: "OSS-Fuzz: leading-comma malformed input must not panic in Delete",
+		json: `,{"test":1{}`,
+		path: []string{"test"},
+		data: `}`,
+	},
+	{
+		desc: "OSS-Fuzz variant: leading comma + empty string then object must not panic in Delete",
+		json: `,""{"test":0}`,
+		path: []string{"test"},
+		data: `}`,
+	},
 }
 
 var setTests = []SetTest{
diff --git a/run_fuzz_campaign.sh b/run_fuzz_campaign.sh
new file mode 100755
index 0000000..973be85
--- /dev/null
+++ b/run_fuzz_campaign.sh
@@ -0,0 +1,54 @@
+#!/bin/bash
+set -u
+cd "$(dirname "$0")"
+mkdir -p fuzz_results/crashes
+LOG=fuzz_results/campaign.log
+: > "$LOG"
+
+TARGETS=(
+  DeleteNative
+  ParseStringNative
+  EachKeyNative
+  SetNative
+  ObjectEachNative
+  ParseFloatNative
+  ParseIntNative
+  ParseBoolNative
+  TokenStartNative
+  GetStringNative
+  GetFloatNative
+  GetIntNative
+  GetBooleanNative
+  GetUnsafeStringNative
+)
+PER_TARGET=${PER_TARGET:-180s}
+MAX_PASSES=${MAX_PASSES:-4}
+
+count_crashes() { ls fuzz_results/crashes/ 2>/dev/null | wc -l | tr -d ' '; }
+
+prev_count=$(count_crashes)
+pass=0
+while [ $pass -lt $MAX_PASSES ]; do
+  pass=$((pass+1))
+  echo "=== $(date '+%H:%M:%S') PASS $pass start (per-target=$PER_TARGET, baseline_unique_crashes=$prev_count) ===" | tee -a "$LOG"
+  for t in "${TARGETS[@]}"; do
+    pre=$(count_crashes)
+    echo "  -> $(date '+%H:%M:%S') Fuzz${t}" | tee -a "$LOG"
+    go test -run='^$' -fuzz="^Fuzz${t}$" -fuzztime="${PER_TARGET}" \
+        > "fuzz_results/${t}_pass${pass}.log" 2>&1
+    rc=$?
+    post=$(count_crashes)
+    delta=$((post - pre))
+    summary=$(tail -n 3 "fuzz_results/${t}_pass${pass}.log" | tr '\n' ' | ')
+    echo "     rc=$rc new_crashes=$delta total=$post :: $summary" | tee -a "$LOG"
+  done
+  new_count=$(count_crashes)
+  pass_delta=$((new_count - prev_count))
+  echo "=== $(date '+%H:%M:%S') PASS $pass done: total_unique_crashes=$new_count (+$pass_delta this pass) ===" | tee -a "$LOG"
+  if [ $pass_delta -eq 0 ] && [ $pass -ge 2 ]; then
+    echo "=== SATURATED after pass $pass — no new crashes ===" | tee -a "$LOG"
+    break
+  fi
+  prev_count=$new_count
+done
+echo "=== $(date '+%H:%M:%S') CAMPAIGN COMPLETE total_unique_crashes=$(count_crashes) ===" | tee -a "$LOG"
diff --git a/specs/stakeholder/requirements/STK-REQ-001.req.yaml b/specs/stakeholder/requirements/STK-REQ-001.req.yaml
index 4c03b30..90fffca 100644
--- a/specs/stakeholder/requirements/STK-REQ-001.req.yaml
+++ b/specs/stakeholder/requirements/STK-REQ-001.req.yaml
@@ -13,13 +13,17 @@ informal_verification:
     verified: false
 component: parser
 rationale: This is the core value proposition described in the project README and the primary reason to adopt jsonparser over encoding/json for dynamic payloads.
-tags: []
+tags:
+    - parser
+    - deserializer
+    - accepts_user_data
 variables: []
 traces:
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.194955Z"
+    reviewed_at: "2026-05-03T10:16:37.49529Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:03980d5fb5dc1bbbf43967195726ef679670e9ac95ef3e6d1643d626ee9371e9
 verification:
     assurance_level: E
     formalization_status: none
@@ -32,7 +36,7 @@ history:
     created_by: human:cli
     created_at: "2026-04-13T16:22:41Z"
     last_modified_by: human:cli
-    last_modified_at: "2026-04-13T16:25:24Z"
+    last_modified_at: "2026-05-03T10:15:04Z"
 stakeholder:
     persona: Go developers consuming dynamic JSON payloads
     story: As a Go developer consuming unpredictable JSON APIs, I want to retrieve nested values by key path without predeclaring structs so that I can process payloads directly from byte slices.
@@ -66,21 +70,98 @@ stakeholder:
             - SYS-REQ-088
             - SYS-REQ-089
     obligation_checklist:
-        - nominal
-        - missing_path
-        - malformed_input
-        - truncated_at_value_boundary
-        - truncated_mid_structure
-        - truncated_mid_key
-        - empty_input
         - boundary
-        - type_mismatch
-        - negative_array_index
-        - sentinel_value_boundary
         - determinism
+        - edge_case
+        - empty_input
         - idempotency
+        - malformed_input
+        - missing_path
+        - negative_array_index
         - nil_safety
-        - edge_case
+        - nominal
+        - sentinel_value_boundary
+        - truncated_at_value_boundary
+        - truncated_mid_key
+        - truncated_mid_structure
+        - type_mismatch
+    obligation_suppressions:
+        - id: denial_of_service_resistant
+          reason: 'Decomposed across multiple SYS-REQ leaves that bound parser time/stack: SYS-REQ-026 (best-effort recovery on malformed input around addressed token), SYS-REQ-046 (blockEnd structural-balance check); the implementation uses an iterative tokenizer in parser.go bounded by input byte length, with fuzz coverage in fuzz_test.go.'
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:02Z"
+          framework_refs:
+            - CWE CWE-400,CWE-1333
+            - MISRA-C Rule 17.2
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V11.1.4
+        - id: encoding_aware
+          reason: Decomposed at SYS-REQ-024 (escaped object-member key matching exercises decoded-key equality against escaped JSON); jsonparser handles UTF-8 and JSON \u escapes via the GetString decoder path tested in escape_test.go and parser_test.go.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:02Z"
+          framework_refs:
+            - CWE CWE-176,CWE-180,CWE-838
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: length_prefix_validated
+          reason: JSON is a self-delimiting structural format with no length-prefix fields; jsonparser's tokenizer advances by structural state machine, not by trusting a declared byte count.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:06:56Z"
+          framework_refs:
+            - CWE CWE-130,CWE-805,CWE-119
+            - IEC-62304 §5.3.1
+            - MISRA-C Rule 21.18
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: malformed_recovers_or_errors_loudly
+          reason: Decomposed at SYS-REQ-026 (documented best-effort success/not-found preservation outside addressed token), SYS-REQ-041-043 (truncated-at-value-boundary, mid-structure, mid-key handling) and SYS-REQ-029/031 (callback-based malformed input); the malformed-input policy is best-effort recovery and is verified via parser_error_test.go.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:02Z"
+          framework_refs:
+            - CWE CWE-20,CWE-755
+            - IEC-62304 §5.3.1
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10,SI-11
+            - OWASP-ASVS-v4 V5.1.3,V5.5.3
+        - id: polymorphic_type_whitelist
+          reason: jsonparser exposes raw byte slices and JSON token types; it never instantiates Go types from a discriminator field, so no polymorphic deserialization attack surface exists in the API.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:06:56Z"
+          framework_refs:
+            - CWE CWE-502,CWE-915
+            - IEC-62304 §5.3.1
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.5.1,V5.5.2
+        - id: recursion_depth_bounded
+          reason: Decomposed at SYS-REQ-046 (blockEnd helper enforces structural recursion bounds across nested objects and arrays); the implementation uses an iterative byte-pointer tokenizer in parser.go that does not native-recurse on JSON nesting depth, so deep payloads cannot overflow the goroutine stack.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:03Z"
+          framework_refs:
+            - CWE CWE-674,CWE-400
+            - IEC-62304 §5.3.1
+            - MISRA-C Rule 17.2
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V5.5.3
+        - id: reference_cycle_safe
+          reason: JSON RFC 8259 has no reference or alias syntax; cycles cannot exist in a well-formed JSON document and jsonparser does not perform any $ref or anchor expansion.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:06:56Z"
+          framework_refs:
+            - CWE CWE-674,CWE-1325
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V5.5.3
+        - id: untrusted_input_bounded
+          reason: jsonparser's API takes a caller-provided []byte slice and processes it in-place; size enforcement is the caller's responsibility (delegated to the surrounding HTTP / queue handler); the parser itself processes bounded byte slices and never instantiates Go types from the input, so the deserializer schema-bound concern of this catalog class does not apply at the library layer.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:03Z"
+          framework_refs:
+            - CWE CWE-502,CWE-20
+            - IEC-62304 §5.3.1
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.5.1,V5.5.3
 lifecycle:
     change_history:
         - date: "2026-04-13T16:25:24Z"
diff --git a/specs/stakeholder/requirements/STK-REQ-002.req.yaml b/specs/stakeholder/requirements/STK-REQ-002.req.yaml
index 45f425f..41566c0 100644
--- a/specs/stakeholder/requirements/STK-REQ-002.req.yaml
+++ b/specs/stakeholder/requirements/STK-REQ-002.req.yaml
@@ -13,13 +13,17 @@ informal_verification:
     verified: false
 component: parser
 rationale: The README explicitly promises that GetString handles escaped and Unicode characters correctly, which is a user-visible contract distinct from raw byte lookup.
-tags: []
+tags:
+    - parser
+    - deserializer
+    - accepts_user_data
 variables: []
 traces:
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.19831Z"
+    reviewed_at: "2026-05-03T10:16:37.691899Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:6e97daeb1cdbe4ecabcca7e6eb1884a94ce49c7775c7427971150d40178840bd
 verification:
     assurance_level: E
     formalization_status: none
@@ -32,7 +36,7 @@ history:
     created_by: human:cli
     created_at: "2026-04-13T17:09:09Z"
     last_modified_by: human:cli
-    last_modified_at: "2026-04-13T17:14:56Z"
+    last_modified_at: "2026-05-03T10:15:05Z"
 stakeholder:
     persona: Go developers reading string fields from dynamic JSON payloads
     story: As a Go developer reading JSON string fields, I want escaped and Unicode content decoded into normal Go strings so that application code does not need to manually unescape payload bytes.
@@ -51,15 +55,92 @@ stakeholder:
             - SYS-REQ-092
             - SYS-REQ-093
     obligation_checklist:
-        - nominal
+        - determinism
+        - edge_case
+        - empty_input
+        - encoding_safety
         - malformed_input
+        - nil_safety
+        - nominal
         - truncated_escape_sequence
         - type_mismatch
-        - empty_input
-        - determinism
-        - nil_safety
-        - encoding_safety
-        - edge_case
+    obligation_suppressions:
+        - id: denial_of_service_resistant
+          reason: Decomposed at SYS-REQ-038 (ParseString malformed-token error) and SYS-REQ-074 (string decoding bounds); GetString runs the same iterative tokenizer + decoder, bounded by the caller's []byte slice length, with fuzz coverage of escape decoding in fuzz_test.go.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:18Z"
+          framework_refs:
+            - CWE CWE-400,CWE-1333
+            - MISRA-C Rule 17.2
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V11.1.4
+        - id: encoding_aware
+          reason: Decomposed at SYS-REQ-073 (Unicode escape \uXXXX decoding) and SYS-REQ-038 (ParseString malformed encoded literal); GetString decodes JSON escapes (\n, \u, surrogate pairs) into valid UTF-8 Go strings, with explicit malformed-encoding rejection via MalformedStringEscapeError.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:18Z"
+          framework_refs:
+            - CWE CWE-176,CWE-180,CWE-838
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: length_prefix_validated
+          reason: JSON is a self-delimiting structural format with no length-prefix fields; jsonparser's tokenizer advances by structural state machine, not by trusting a declared byte count.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:06:56Z"
+          framework_refs:
+            - CWE CWE-130,CWE-805,CWE-119
+            - IEC-62304 §5.3.1
+            - MISRA-C Rule 21.18
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: malformed_recovers_or_errors_loudly
+          reason: Decomposed at SYS-REQ-038 (ParseString returns documented MalformedStringError), SYS-REQ-093 (truncated escape sequence handling); GetString fails-loud on invalid escape sequences rather than returning partial decoded output.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:19Z"
+          framework_refs:
+            - CWE CWE-20,CWE-755
+            - IEC-62304 §5.3.1
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10,SI-11
+            - OWASP-ASVS-v4 V5.1.3,V5.5.3
+        - id: polymorphic_type_whitelist
+          reason: jsonparser exposes raw byte slices and JSON token types; it never instantiates Go types from a discriminator field, so no polymorphic deserialization attack surface exists in the API.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:06:57Z"
+          framework_refs:
+            - CWE CWE-502,CWE-915
+            - IEC-62304 §5.3.1
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.5.1,V5.5.2
+        - id: recursion_depth_bounded
+          reason: GetString resolves a single string value at the addressed path via the same iterative path-walker as Get; nesting bounds are enforced by SYS-REQ-046 (blockEnd) shared with the lookup chain in STK-REQ-001.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:19Z"
+          framework_refs:
+            - CWE CWE-674,CWE-400
+            - IEC-62304 §5.3.1
+            - MISRA-C Rule 17.2
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V5.5.3
+        - id: reference_cycle_safe
+          reason: JSON RFC 8259 has no reference or alias syntax; cycles cannot exist in a well-formed JSON document and jsonparser does not perform any $ref or anchor expansion.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:06:57Z"
+          framework_refs:
+            - CWE CWE-674,CWE-1325
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V5.5.3
+        - id: untrusted_input_bounded
+          reason: GetString returns a Go string copy of decoded bytes; no Go-type instantiation from a discriminator occurs and the input []byte is caller-bounded; the schema-enforcement aspect of this catalog class does not apply at the helper-API layer.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:19Z"
+          framework_refs:
+            - CWE CWE-502,CWE-20
+            - IEC-62304 §5.3.1
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.5.1,V5.5.3
 lifecycle:
     change_history:
         - date: "2026-04-13T17:14:56Z"
diff --git a/specs/stakeholder/requirements/STK-REQ-003.req.yaml b/specs/stakeholder/requirements/STK-REQ-003.req.yaml
index 1330695..82679a8 100644
--- a/specs/stakeholder/requirements/STK-REQ-003.req.yaml
+++ b/specs/stakeholder/requirements/STK-REQ-003.req.yaml
@@ -13,13 +13,16 @@ informal_verification:
     verified: false
 component: parser
 rationale: The README presents typed helpers as part of the public API for callers who already know the expected JSON scalar type.
-tags: []
+tags:
+    - parser
+    - accepts_user_data
 variables: []
 traces:
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.200401Z"
+    reviewed_at: "2026-05-03T10:16:37.751828Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:e1999702de59be1f37115b38bdac75148238431731dbb73710d5298a77c6cb7a
 verification:
     assurance_level: E
     formalization_status: none
@@ -32,7 +35,7 @@ history:
     created_by: human:cli
     created_at: "2026-04-13T17:10:33Z"
     last_modified_by: human:cli
-    last_modified_at: "2026-04-13T17:14:56Z"
+    last_modified_at: "2026-05-03T10:15:08Z"
 stakeholder:
     persona: Go developers reading known scalar fields from dynamic JSON payloads
     story: As a Go developer who knows the expected scalar type of a JSON field, I want typed helper accessors so that I can avoid manual byte parsing and get explicit errors on invalid access.
@@ -61,15 +64,54 @@ stakeholder:
             - SYS-REQ-095
             - SYS-REQ-096
     obligation_checklist:
-        - nominal
-        - malformed_input
         - boundary
-        - type_mismatch
-        - empty_input
-        - partial_literal
         - determinism
-        - nil_safety
         - edge_case
+        - empty_input
+        - malformed_input
+        - nil_safety
+        - nominal
+        - partial_literal
+        - type_mismatch
+    obligation_suppressions:
+        - id: denial_of_service_resistant
+          reason: Decomposed at SYS-REQ-040 (ParseInt malformed-token error), SYS-REQ-037 (ParseFloat malformed numeric token), SYS-REQ-036 (ParseBoolean invalid token); typed scalar helpers run a single-token byte scan bounded by the addressed value slice, with no recursion or backtracking.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:23Z"
+          framework_refs:
+            - CWE CWE-400,CWE-1333
+            - MISRA-C Rule 17.2
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V11.1.4
+        - id: encoding_aware
+          reason: Numeric and boolean JSON tokens are ASCII per RFC 8259; SYS-REQ-040 / SYS-REQ-037 / SYS-REQ-036 reject non-ASCII bytes inside numeric/boolean tokens via MalformedValueError; encoding concerns terminate at the per-token scanners in parser.go.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:23Z"
+          framework_refs:
+            - CWE CWE-176,CWE-180,CWE-838
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: length_prefix_validated
+          reason: JSON is a self-delimiting structural format with no length-prefix fields; jsonparser's tokenizer advances by structural state machine, not by trusting a declared byte count.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:07:03Z"
+          framework_refs:
+            - CWE CWE-130,CWE-805,CWE-119
+            - IEC-62304 §5.3.1
+            - MISRA-C Rule 21.18
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: malformed_recovers_or_errors_loudly
+          reason: Decomposed at SYS-REQ-040 (ParseInt MalformedValueError), SYS-REQ-037 (ParseFloat MalformedValueError), SYS-REQ-036 (ParseBoolean MalformedValueError); typed helpers fail-loud rather than returning partial conversion results.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:23Z"
+          framework_refs:
+            - CWE CWE-20,CWE-755
+            - IEC-62304 §5.3.1
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10,SI-11
+            - OWASP-ASVS-v4 V5.1.3,V5.5.3
 lifecycle:
     change_history:
         - date: "2026-04-13T17:14:56Z"
diff --git a/specs/stakeholder/requirements/STK-REQ-004.req.yaml b/specs/stakeholder/requirements/STK-REQ-004.req.yaml
index 8615c72..431a69f 100644
--- a/specs/stakeholder/requirements/STK-REQ-004.req.yaml
+++ b/specs/stakeholder/requirements/STK-REQ-004.req.yaml
@@ -16,12 +16,16 @@ rationale: The traversal helpers and EachKey are part of the library's value pro
 tags:
     - traversal
     - decomposition
+    - parser
+    - deserializer
+    - accepts_user_data
 variables: []
 traces:
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.202291Z"
+    reviewed_at: "2026-05-03T10:16:37.938833Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:d9b91a7969d5d8fcab05218da9328585bda2d04ac2efe037e0ea80a654e9b0b5
 verification:
     assurance_level: E
     formalization_status: none
@@ -33,8 +37,8 @@ verification:
 history:
     created_by: human:cli
     created_at: "2026-04-13T17:10:34Z"
-    last_modified_by: agent:codex
-    last_modified_at: "2026-04-14T15:45:00Z"
+    last_modified_by: human:cli
+    last_modified_at: "2026-05-03T10:15:07Z"
 stakeholder:
     persona: Go developers traversing dynamic JSON structures
     story: As a Go developer inspecting dynamic JSON payloads, I want traversal helpers that iterate arrays and objects and resolve multiple paths in one scan so that I can process payloads without writing custom walkers.
@@ -70,17 +74,94 @@ stakeholder:
             - SYS-REQ-098
             - SYS-REQ-099
     obligation_checklist:
-        - nominal
+        - callback_error_propagation
+        - determinism
+        - edge_case
         - empty_input
         - malformed_input
+        - nil_safety
+        - nominal
+        - sentinel_value_boundary
         - truncated_at_value_boundary
-        - truncated_mid_structure
         - truncated_mid_element
-        - callback_error_propagation
-        - sentinel_value_boundary
-        - determinism
-        - nil_safety
-        - edge_case
+        - truncated_mid_structure
+    obligation_suppressions:
+        - id: denial_of_service_resistant
+          reason: Decomposed at SYS-REQ-029 (ArrayEach malformed input → error), SYS-REQ-031 (ObjectEach malformed input → error), SYS-REQ-053/054 (truncated mid-element handling); traversal helpers iterate via the bounded iterative tokenizer and emit at most one callback per element.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:32Z"
+          framework_refs:
+            - CWE CWE-400,CWE-1333
+            - MISRA-C Rule 17.2
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V11.1.4
+        - id: encoding_aware
+          reason: ArrayEach / ObjectEach pass raw value byte slices to the caller without decoding; encoding correctness is delegated to the caller-chosen accessor (GetString covered by STK-REQ-002 / SYS-REQ-073) which the callback typically invokes for string fields.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:32Z"
+          framework_refs:
+            - CWE CWE-176,CWE-180,CWE-838
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: length_prefix_validated
+          reason: JSON is a self-delimiting structural format with no length-prefix fields; jsonparser's tokenizer advances by structural state machine, not by trusting a declared byte count.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:06:57Z"
+          framework_refs:
+            - CWE CWE-130,CWE-805,CWE-119
+            - IEC-62304 §5.3.1
+            - MISRA-C Rule 21.18
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: malformed_recovers_or_errors_loudly
+          reason: Decomposed at SYS-REQ-029 (ArrayEach malformed → error), SYS-REQ-031 (ObjectEach malformed → error), SYS-REQ-053 (array element truncated → error), SYS-REQ-054 (object entry truncated → error); the traversal helpers fail-loud on malformed structure rather than swallowing partial state.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:32Z"
+          framework_refs:
+            - CWE CWE-20,CWE-755
+            - IEC-62304 §5.3.1
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10,SI-11
+            - OWASP-ASVS-v4 V5.1.3,V5.5.3
+        - id: polymorphic_type_whitelist
+          reason: jsonparser exposes raw byte slices and JSON token types; it never instantiates Go types from a discriminator field, so no polymorphic deserialization attack surface exists in the API.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:06:58Z"
+          framework_refs:
+            - CWE CWE-502,CWE-915
+            - IEC-62304 §5.3.1
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.5.1,V5.5.2
+        - id: recursion_depth_bounded
+          reason: ArrayEach / ObjectEach iterate one structural level via the iterative tokenizer; for nested traversal the caller invokes ArrayEach again from inside its callback, so depth bound is the caller's call-stack rather than a parser-internal recursion — the parser itself does not native-recurse on JSON nesting.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:33Z"
+          framework_refs:
+            - CWE CWE-674,CWE-400
+            - IEC-62304 §5.3.1
+            - MISRA-C Rule 17.2
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V5.5.3
+        - id: reference_cycle_safe
+          reason: JSON RFC 8259 has no reference or alias syntax; cycles cannot exist in a well-formed JSON document and jsonparser does not perform any $ref or anchor expansion.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:06:58Z"
+          framework_refs:
+            - CWE CWE-674,CWE-1325
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V5.5.3
+        - id: untrusted_input_bounded
+          reason: Traversal helpers expose raw value byte slices; no Go-type instantiation from input occurs and the input []byte is caller-bounded; deserializer-style schema enforcement is delegated to the caller's typed accessor selection.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:33Z"
+          framework_refs:
+            - CWE CWE-502,CWE-20
+            - IEC-62304 §5.3.1
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.5.1,V5.5.3
 lifecycle:
     change_history:
         - date: "2026-04-13T17:14:56Z"
diff --git a/specs/stakeholder/requirements/STK-REQ-005.req.yaml b/specs/stakeholder/requirements/STK-REQ-005.req.yaml
index a764821..c1fb34e 100644
--- a/specs/stakeholder/requirements/STK-REQ-005.req.yaml
+++ b/specs/stakeholder/requirements/STK-REQ-005.req.yaml
@@ -16,12 +16,15 @@ rationale: Set and Delete are documented experimental APIs, so their mutation an
 tags:
     - mutation
     - decomposition
+    - parser
+    - accepts_user_data
 variables: []
 traces:
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.204096Z"
+    reviewed_at: "2026-05-03T10:16:38.120269Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:f0a864e9d7950d7c8b9e09bc3370b52afde61abf00424665ad6fe8ac64882cfc
 verification:
     assurance_level: E
     formalization_status: none
@@ -33,8 +36,8 @@ verification:
 history:
     created_by: human:cli
     created_at: "2026-04-13T17:15:31Z"
-    last_modified_by: agent:codex
-    last_modified_at: "2026-04-14T15:45:00Z"
+    last_modified_by: human:cli
+    last_modified_at: "2026-05-03T10:15:09Z"
 stakeholder:
     persona: Go developers mutating dynamic JSON payloads in-place
     story: As a Go developer mutating JSON byte payloads, I want experimental helpers that update or delete addressed values with deterministic edge-case behavior so that I can transform payloads without writing my own low-level mutator.
@@ -64,19 +67,58 @@ stakeholder:
             - SYS-REQ-101
             - SYS-REQ-102
     obligation_checklist:
-        - nominal
-        - missing_path
-        - malformed_input
-        - truncated_at_value_boundary
-        - truncated_mid_structure
+        - edge_case
         - empty_input
-        - no_path_provided
-        - nested_mutation
         - error_propagation
-        - sentinel_value_boundary
         - idempotency
+        - malformed_input
+        - missing_path
+        - nested_mutation
         - nil_safety
-        - edge_case
+        - no_path_provided
+        - nominal
+        - sentinel_value_boundary
+        - truncated_at_value_boundary
+        - truncated_mid_structure
+    obligation_suppressions:
+        - id: denial_of_service_resistant
+          reason: Decomposed at SYS-REQ-035 (Delete malformed/truncated input → unchanged payload, no panic), SYS-REQ-051 (Set on truncated input → error rather than corrupt output), SYS-REQ-056 (Delete mid-structure truncated → unchanged); mutation helpers reuse the bounded iterative tokenizer and never panic on adversarial input.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:38Z"
+          framework_refs:
+            - CWE CWE-400,CWE-1333
+            - MISRA-C Rule 17.2
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V11.1.4
+        - id: encoding_aware
+          reason: Set / Delete operate at the byte-level on the caller's []byte payload; they preserve the exact byte encoding of unchanged regions (no transcoding) and Set's caller supplies the replacement byte sequence whose encoding is the caller's responsibility.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:38Z"
+          framework_refs:
+            - CWE CWE-176,CWE-180,CWE-838
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: length_prefix_validated
+          reason: JSON is a self-delimiting structural format with no length-prefix fields; jsonparser's tokenizer advances by structural state machine, not by trusting a declared byte count.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:07:04Z"
+          framework_refs:
+            - CWE CWE-130,CWE-805,CWE-119
+            - IEC-62304 §5.3.1
+            - MISRA-C Rule 21.18
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: malformed_recovers_or_errors_loudly
+          reason: Decomposed at SYS-REQ-035 (Delete on malformed input → original payload unchanged, no panic — documented best-effort recovery), SYS-REQ-051 (Set on truncated input → explicit error rather than corrupt output); the recovery-vs-error policy is documented per-operation.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:38Z"
+          framework_refs:
+            - CWE CWE-20,CWE-755
+            - IEC-62304 §5.3.1
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10,SI-11
+            - OWASP-ASVS-v4 V5.1.3,V5.5.3
 lifecycle:
     change_history:
         - date: "2026-04-13T17:16:45Z"
diff --git a/specs/stakeholder/requirements/STK-REQ-006.req.yaml b/specs/stakeholder/requirements/STK-REQ-006.req.yaml
index 03fca9f..7cf32c2 100644
--- a/specs/stakeholder/requirements/STK-REQ-006.req.yaml
+++ b/specs/stakeholder/requirements/STK-REQ-006.req.yaml
@@ -13,13 +13,16 @@ informal_verification:
     verified: false
 component: parser
 rationale: GetUnsafeString is a distinct public contract from GetString because it trades escaping semantics for speed and zero-allocation string mapping.
-tags: []
+tags:
+    - parser
+    - accepts_user_data
 variables: []
 traces:
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.206431Z"
+    reviewed_at: "2026-05-03T10:16:38.345762Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:d8cb5270f1a31d74fcc09387e31521cb5f57cd118e435fa4a6eac91b3b77d4ff
 verification:
     assurance_level: E
     formalization_status: none
@@ -32,7 +35,7 @@ history:
     created_by: human:cli
     created_at: "2026-04-13T17:21:50Z"
     last_modified_by: human:cli
-    last_modified_at: "2026-04-13T17:27:00Z"
+    last_modified_at: "2026-05-03T10:15:10Z"
 stakeholder:
     persona: Go developers reading JSON tokens with minimal allocations
     story: As a Go developer reading JSON byte payloads, I want an unsafe helper that exposes addressed values as raw strings without unescaping so that I can avoid extra allocations when I explicitly accept the tradeoff.
@@ -49,13 +52,52 @@ stakeholder:
             - SYS-REQ-104
             - SYS-REQ-105
     obligation_checklist:
-        - nominal
-        - malformed_input
-        - empty_input
-        - truncated_at_value_boundary
         - determinism
-        - nil_safety
         - edge_case
+        - empty_input
+        - malformed_input
+        - nil_safety
+        - nominal
+        - truncated_at_value_boundary
+    obligation_suppressions:
+        - id: denial_of_service_resistant
+          reason: Decomposed at SYS-REQ-080 (GetUnsafeString delegates to underlying path lookup) and SYS-REQ-082 (returns raw bytes without unescape work); the helper performs zero-allocation string mapping over a caller-bounded []byte with no extra parsing beyond the path walk.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:44Z"
+          framework_refs:
+            - CWE CWE-400,CWE-1333
+            - MISRA-C Rule 17.2
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V11.1.4
+        - id: encoding_aware
+          reason: GetUnsafeString explicitly opts out of JSON unescaping and returns raw byte content as a string; encoding interpretation is the caller's responsibility (the API name and SYS-REQ-006 documentation make the encoding-passthrough contract explicit).
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:44Z"
+          framework_refs:
+            - CWE CWE-176,CWE-180,CWE-838
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: length_prefix_validated
+          reason: JSON is a self-delimiting structural format with no length-prefix fields; jsonparser's tokenizer advances by structural state machine, not by trusting a declared byte count.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:07:05Z"
+          framework_refs:
+            - CWE CWE-130,CWE-805,CWE-119
+            - IEC-62304 §5.3.1
+            - MISRA-C Rule 21.18
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: malformed_recovers_or_errors_loudly
+          reason: Decomposed at SYS-REQ-080 (GetUnsafeString inherits the documented lookup-miss behaviour from the underlying path lookup); malformed input surfaces through the same Get path-walker errors as STK-REQ-001 / SYS-REQ-026 — the unsafe variant adds no new malformed-input failure modes.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:44Z"
+          framework_refs:
+            - CWE CWE-20,CWE-755
+            - IEC-62304 §5.3.1
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10,SI-11
+            - OWASP-ASVS-v4 V5.1.3,V5.5.3
 lifecycle:
     change_history:
         - date: "2026-04-13T17:27:00Z"
diff --git a/specs/stakeholder/requirements/STK-REQ-007.req.yaml b/specs/stakeholder/requirements/STK-REQ-007.req.yaml
index f6c1e9d..7e7f312 100644
--- a/specs/stakeholder/requirements/STK-REQ-007.req.yaml
+++ b/specs/stakeholder/requirements/STK-REQ-007.req.yaml
@@ -16,12 +16,15 @@ rationale: The Parse* helpers are public token-level conversion utilities and th
 tags:
     - parse
     - decomposition
+    - parser
+    - accepts_user_data
 variables: []
 traces:
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.208511Z"
+    reviewed_at: "2026-05-03T10:16:38.403665Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:d356de6e36f424a431f216f1e34014355746b879eadbbe1d0e1b3db1d2db184c
 verification:
     assurance_level: E
     formalization_status: none
@@ -33,8 +36,8 @@ verification:
 history:
     created_by: human:cli
     created_at: "2026-04-13T17:21:50Z"
-    last_modified_by: agent:codex
-    last_modified_at: "2026-04-14T15:45:00Z"
+    last_modified_by: human:cli
+    last_modified_at: "2026-05-03T10:15:11Z"
 stakeholder:
     persona: Go developers converting raw JSON scalar tokens into typed values
     story: As a Go developer working with raw JSON scalar tokens, I want Parse helpers that convert boolean, integer, float, and string tokens into Go values with deterministic malformed-input behavior so that I can safely reuse the parser below full document traversal.
@@ -80,16 +83,55 @@ stakeholder:
             - SYS-REQ-108
             - SYS-REQ-109
     obligation_checklist:
-        - nominal
-        - malformed_input
         - boundary
-        - partial_literal
-        - truncated_escape_sequence
-        - empty_input
         - determinism
-        - nil_safety
-        - encoding_safety
         - edge_case
+        - empty_input
+        - encoding_safety
+        - malformed_input
+        - nil_safety
+        - nominal
+        - partial_literal
+        - truncated_escape_sequence
+    obligation_suppressions:
+        - id: denial_of_service_resistant
+          reason: Decomposed at SYS-REQ-036 (ParseBoolean), SYS-REQ-037 (ParseFloat), SYS-REQ-038 (ParseString), SYS-REQ-040 (ParseInt) — each Parse* helper runs a single-pass byte scan over the caller-supplied token slice with no recursion, backtracking, or unbounded copy.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:49Z"
+          framework_refs:
+            - CWE CWE-400,CWE-1333
+            - MISRA-C Rule 17.2
+            - NIST-800-53 SC-5
+            - OWASP-ASVS-v4 V11.1.4
+        - id: encoding_aware
+          reason: Decomposed at SYS-REQ-038 (ParseString MalformedStringError on invalid encoding), SYS-REQ-067 (ParseString surrogate-pair handling); ParseInt/ParseFloat/ParseBoolean operate on ASCII tokens per RFC 8259 and reject non-ASCII via MalformedValueError.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:49Z"
+          framework_refs:
+            - CWE CWE-176,CWE-180,CWE-838
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: length_prefix_validated
+          reason: JSON is a self-delimiting structural format with no length-prefix fields; jsonparser's tokenizer advances by structural state machine, not by trusting a declared byte count.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:07:07Z"
+          framework_refs:
+            - CWE CWE-130,CWE-805,CWE-119
+            - IEC-62304 §5.3.1
+            - MISRA-C Rule 21.18
+            - NIST-800-53 SI-10
+            - OWASP-ASVS-v4 V5.1.4
+        - id: malformed_recovers_or_errors_loudly
+          reason: Decomposed at SYS-REQ-036/037/038/040 (each Parse* helper returns the documented MalformedValueError on invalid token shape), SYS-REQ-064 (ParseInt overflow error); Parse* helpers fail-loud rather than returning partial values.
+          suppressed_by: leonidbugaev
+          suppressed_at: "2026-05-03T10:14:49Z"
+          framework_refs:
+            - CWE CWE-20,CWE-755
+            - IEC-62304 §5.3.1
+            - MISRA-C Dir 4.14
+            - NIST-800-53 SI-10,SI-11
+            - OWASP-ASVS-v4 V5.1.3,V5.5.3
 lifecycle:
     change_history:
         - date: "2026-04-13T17:27:00Z"
diff --git a/specs/system/requirements/SYS-REQ-001.req.yaml b/specs/system/requirements/SYS-REQ-001.req.yaml
index 4154096..3982e1e 100644
--- a/specs/system/requirements/SYS-REQ-001.req.yaml
+++ b/specs/system/requirements/SYS-REQ-001.req.yaml
@@ -27,8 +27,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.210461Z"
+    reviewed_at: "2026-05-03T10:16:38.544535Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:77db253885f8cae96d49c0e808fe145654eda932ca9ef9a37106d2c941ff91f9
 verification:
     assurance_level: B
     formalization_status: valid
@@ -44,7 +45,7 @@ history:
     created_by: human:cli
     created_at: "2026-04-13T16:22:41Z"
     last_modified_by: human:cli
-    last_modified_at: "2026-04-18T10:12:51Z"
+    last_modified_at: "2026-05-03T10:13:31Z"
 obligation_class: nominal
 lifecycle:
     change_history:
diff --git a/specs/system/requirements/SYS-REQ-002.req.yaml b/specs/system/requirements/SYS-REQ-002.req.yaml
index 97ea2c0..9a5b5c3 100644
--- a/specs/system/requirements/SYS-REQ-002.req.yaml
+++ b/specs/system/requirements/SYS-REQ-002.req.yaml
@@ -26,8 +26,9 @@ traces:
         - mcdc_supplement_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.215485Z"
+    reviewed_at: "2026-05-03T10:16:38.888534Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:3c1c747e4c5eec9c7c0e8b7e83e73ff11cc4143d0b740ae514ad812f5f09a5a2
 verification:
     assurance_level: E
     formalization_status: valid
@@ -40,7 +41,7 @@ history:
     created_by: human:cli
     created_at: "2026-04-13T17:10:46Z"
     last_modified_by: human:cli
-    last_modified_at: "2026-04-13T17:14:56Z"
+    last_modified_at: "2026-05-03T10:10:35Z"
 obligation_class: nominal
 lifecycle:
     change_history:
diff --git a/specs/system/requirements/SYS-REQ-003.req.yaml b/specs/system/requirements/SYS-REQ-003.req.yaml
index 458c63e..cc89c40 100644
--- a/specs/system/requirements/SYS-REQ-003.req.yaml
+++ b/specs/system/requirements/SYS-REQ-003.req.yaml
@@ -26,8 +26,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.219365Z"
+    reviewed_at: "2026-05-03T10:16:39.111503Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:c8991ddc4e7ff7698178d7b8d514a3463239b16986e46e9d849e6cee917a3ced
 verification:
     assurance_level: E
     formalization_status: valid
@@ -40,7 +41,7 @@ history:
     created_by: human:cli
     created_at: "2026-04-13T17:10:46Z"
     last_modified_by: human:cli
-    last_modified_at: "2026-04-13T17:14:56Z"
+    last_modified_at: "2026-05-03T10:10:36Z"
 obligation_class: nominal
 lifecycle:
     change_history:
diff --git a/specs/system/requirements/SYS-REQ-004.req.yaml b/specs/system/requirements/SYS-REQ-004.req.yaml
index d86c727..33529a6 100644
--- a/specs/system/requirements/SYS-REQ-004.req.yaml
+++ b/specs/system/requirements/SYS-REQ-004.req.yaml
@@ -26,8 +26,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.221084Z"
+    reviewed_at: "2026-05-03T10:17:58.405847Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:bb098543b1618c940dd2722b711d642bf7b6f5cd57c9c100f9efb82d8e18c2a9
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-005.req.yaml b/specs/system/requirements/SYS-REQ-005.req.yaml
index 1159efb..40416e9 100644
--- a/specs/system/requirements/SYS-REQ-005.req.yaml
+++ b/specs/system/requirements/SYS-REQ-005.req.yaml
@@ -26,8 +26,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.223203Z"
+    reviewed_at: "2026-05-03T10:18:23.767347Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:4cf255ab8afc237ed8ac482fab43f90cdf326b6a4a43cbbc9f6847dd5379ac30
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-006.req.yaml b/specs/system/requirements/SYS-REQ-006.req.yaml
index 0e998f5..8b36ef7 100644
--- a/specs/system/requirements/SYS-REQ-006.req.yaml
+++ b/specs/system/requirements/SYS-REQ-006.req.yaml
@@ -29,8 +29,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.224937Z"
+    reviewed_at: "2026-05-03T10:16:39.334467Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:a7923e607958b11aa5aed5e1ff574deab9300dd07c074fcb3afa03cdbb1df264
 verification:
     assurance_level: E
     formalization_status: valid
@@ -42,8 +43,8 @@ verification:
 history:
     created_by: human:cli
     created_at: "2026-04-13T17:10:56Z"
-    last_modified_by: agent:codex
-    last_modified_at: "2026-04-14T15:45:00Z"
+    last_modified_by: human:cli
+    last_modified_at: "2026-05-03T10:10:38Z"
 obligation_class: nominal
 lifecycle:
     change_history:
diff --git a/specs/system/requirements/SYS-REQ-007.req.yaml b/specs/system/requirements/SYS-REQ-007.req.yaml
index 8c5da30..7d8faf3 100644
--- a/specs/system/requirements/SYS-REQ-007.req.yaml
+++ b/specs/system/requirements/SYS-REQ-007.req.yaml
@@ -29,8 +29,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.226669Z"
+    reviewed_at: "2026-05-03T10:18:24.01892Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:2381182a19e458fda187eb76b2628467ece25c8912a825e7191c7762bbcb5201
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-008.req.yaml b/specs/system/requirements/SYS-REQ-008.req.yaml
index 40fac37..3cb9811 100644
--- a/specs/system/requirements/SYS-REQ-008.req.yaml
+++ b/specs/system/requirements/SYS-REQ-008.req.yaml
@@ -29,8 +29,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.228499Z"
+    reviewed_at: "2026-05-03T10:18:24.262241Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:402bf9287393bd692f8d604e383fba5262fdb1017fccf85c2a99b2b36be86ab9
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-009.req.yaml b/specs/system/requirements/SYS-REQ-009.req.yaml
index c6683c4..0ef1e0c 100644
--- a/specs/system/requirements/SYS-REQ-009.req.yaml
+++ b/specs/system/requirements/SYS-REQ-009.req.yaml
@@ -28,8 +28,9 @@ traces:
         - set_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.230653Z"
+    reviewed_at: "2026-05-03T10:16:39.515581Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:8c42a039872084c6608988859743c3cc4f856e3761c10c0ee8a5514d5377b866
 verification:
     assurance_level: E
     formalization_status: valid
@@ -42,7 +43,7 @@ history:
     created_by: human:cli
     created_at: "2026-04-13T17:15:31Z"
     last_modified_by: human:cli
-    last_modified_at: "2026-04-13T17:16:45Z"
+    last_modified_at: "2026-05-03T10:10:39Z"
 obligation_class: nominal
 lifecycle:
     change_history:
diff --git a/specs/system/requirements/SYS-REQ-010.req.yaml b/specs/system/requirements/SYS-REQ-010.req.yaml
index 984a470..8a65a4d 100644
--- a/specs/system/requirements/SYS-REQ-010.req.yaml
+++ b/specs/system/requirements/SYS-REQ-010.req.yaml
@@ -27,8 +27,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.232566Z"
+    reviewed_at: "2026-05-03T10:18:24.563245Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:5693b4c5976b0ab519b78d8246cfb0c03ca770fa49327ba73cbc7d4bcb7e5611
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-011.req.yaml b/specs/system/requirements/SYS-REQ-011.req.yaml
index d1cbcaf..4dcb39b 100644
--- a/specs/system/requirements/SYS-REQ-011.req.yaml
+++ b/specs/system/requirements/SYS-REQ-011.req.yaml
@@ -25,8 +25,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.234219Z"
+    reviewed_at: "2026-05-03T10:16:39.739902Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:386ee392550a53061535de53e401d4f77aac3732d48a28d6dbe41ab645f358a3
 verification:
     assurance_level: E
     formalization_status: valid
@@ -39,7 +40,7 @@ history:
     created_by: human:cli
     created_at: "2026-04-13T17:21:50Z"
     last_modified_by: human:cli
-    last_modified_at: "2026-04-13T17:27:00Z"
+    last_modified_at: "2026-05-03T10:10:40Z"
 obligation_class: nominal
 lifecycle:
     change_history:
diff --git a/specs/system/requirements/SYS-REQ-012.req.yaml b/specs/system/requirements/SYS-REQ-012.req.yaml
index 9da1291..4a4e2fb 100644
--- a/specs/system/requirements/SYS-REQ-012.req.yaml
+++ b/specs/system/requirements/SYS-REQ-012.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.235733Z"
+    reviewed_at: "2026-05-03T10:16:39.961696Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:e0c8e5d7540d1e4a155a0ef32ebc9d68150ac6bbab14dd410a0fdbe94d9bb03a
 verification:
     assurance_level: E
     formalization_status: valid
@@ -41,8 +42,8 @@ verification:
 history:
     created_by: human:cli
     created_at: "2026-04-13T17:21:50Z"
-    last_modified_by: agent:codex
-    last_modified_at: "2026-04-14T15:45:00Z"
+    last_modified_by: human:cli
+    last_modified_at: "2026-05-03T10:10:41Z"
 obligation_class: nominal
 lifecycle:
     change_history:
diff --git a/specs/system/requirements/SYS-REQ-013.req.yaml b/specs/system/requirements/SYS-REQ-013.req.yaml
index b31b2cb..dfc7b6e 100644
--- a/specs/system/requirements/SYS-REQ-013.req.yaml
+++ b/specs/system/requirements/SYS-REQ-013.req.yaml
@@ -27,8 +27,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.23752Z"
+    reviewed_at: "2026-05-03T10:18:24.763656Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:79be64677bafb7a5cd31ec1fbe176fcb8c3c70fdac46780d067be9b2d68654e7
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-014.req.yaml b/specs/system/requirements/SYS-REQ-014.req.yaml
index cd40cd0..686c4eb 100644
--- a/specs/system/requirements/SYS-REQ-014.req.yaml
+++ b/specs/system/requirements/SYS-REQ-014.req.yaml
@@ -29,8 +29,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.239504Z"
+    reviewed_at: "2026-05-03T10:18:25.042307Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:1d8959a1fd8e4ff9e374d3859f4d1717be486571c5fd443a1351f1cb7afddb9a
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-015.req.yaml b/specs/system/requirements/SYS-REQ-015.req.yaml
index 0c5e4bb..0e5de45 100644
--- a/specs/system/requirements/SYS-REQ-015.req.yaml
+++ b/specs/system/requirements/SYS-REQ-015.req.yaml
@@ -29,8 +29,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.24161Z"
+    reviewed_at: "2026-05-03T10:18:25.442621Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:994aeb4eae02f5ea074a815004b273dee093aa4cf8609fc5b0a7209eaf9b93f1
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-016.req.yaml b/specs/system/requirements/SYS-REQ-016.req.yaml
index cee6765..20938da 100644
--- a/specs/system/requirements/SYS-REQ-016.req.yaml
+++ b/specs/system/requirements/SYS-REQ-016.req.yaml
@@ -29,8 +29,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.244005Z"
+    reviewed_at: "2026-05-03T10:18:25.767792Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:4e502a5262abe7972bbd3f6d85a626e36ce841919eb4e1da907a74ba252e26f1
 verification:
     assurance_level: B
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-017.req.yaml b/specs/system/requirements/SYS-REQ-017.req.yaml
index bb6e6e7..1a2cfb7 100644
--- a/specs/system/requirements/SYS-REQ-017.req.yaml
+++ b/specs/system/requirements/SYS-REQ-017.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.246158Z"
+    reviewed_at: "2026-05-03T10:18:25.96917Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:ea81003dac2788e41f3731066a5a7d1d57893c1f18f62e2940b3869eceae1d25
 verification:
     assurance_level: B
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-018.req.yaml b/specs/system/requirements/SYS-REQ-018.req.yaml
index 5f43707..be8b5ad 100644
--- a/specs/system/requirements/SYS-REQ-018.req.yaml
+++ b/specs/system/requirements/SYS-REQ-018.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.247711Z"
+    reviewed_at: "2026-05-03T10:18:26.168623Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:4ba3abf833b2fcb5a73034b6138c79407c545cefa59114db9a2db34180a255d3
 verification:
     assurance_level: B
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-019.req.yaml b/specs/system/requirements/SYS-REQ-019.req.yaml
index 8be783f..0f38f5d 100644
--- a/specs/system/requirements/SYS-REQ-019.req.yaml
+++ b/specs/system/requirements/SYS-REQ-019.req.yaml
@@ -29,8 +29,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.249794Z"
+    reviewed_at: "2026-05-03T10:18:26.369095Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:3281d45f056dd08e916f18288c1a66a4b13afc80a732185420324b1d60588eae
 verification:
     assurance_level: B
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-020.req.yaml b/specs/system/requirements/SYS-REQ-020.req.yaml
index cf443f6..5d5c68d 100644
--- a/specs/system/requirements/SYS-REQ-020.req.yaml
+++ b/specs/system/requirements/SYS-REQ-020.req.yaml
@@ -29,8 +29,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.251389Z"
+    reviewed_at: "2026-05-03T10:18:26.568634Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:4cb65f918fa8d1d45ce711583e13f4ff7d9c1ce2918a1c5081da8ed0461907c6
 verification:
     assurance_level: B
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-021.req.yaml b/specs/system/requirements/SYS-REQ-021.req.yaml
index 6c063d8..5a7da01 100644
--- a/specs/system/requirements/SYS-REQ-021.req.yaml
+++ b/specs/system/requirements/SYS-REQ-021.req.yaml
@@ -30,8 +30,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.253121Z"
+    reviewed_at: "2026-05-03T10:18:26.769383Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:7146496cf9e521105332938ce43b9f6242d9a488f1d0d7f92b692970126115d6
 verification:
     assurance_level: B
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-022.req.yaml b/specs/system/requirements/SYS-REQ-022.req.yaml
index 1aa5643..d5ae5b5 100644
--- a/specs/system/requirements/SYS-REQ-022.req.yaml
+++ b/specs/system/requirements/SYS-REQ-022.req.yaml
@@ -30,8 +30,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.254779Z"
+    reviewed_at: "2026-05-03T10:18:26.969349Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:6396672479fe5ba4a7a70c12c19bee2536f761af978205a34976b9b9f590ac44
 verification:
     assurance_level: B
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-023.req.yaml b/specs/system/requirements/SYS-REQ-023.req.yaml
index 6b093ea..282025d 100644
--- a/specs/system/requirements/SYS-REQ-023.req.yaml
+++ b/specs/system/requirements/SYS-REQ-023.req.yaml
@@ -31,8 +31,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.256398Z"
+    reviewed_at: "2026-05-03T10:18:27.170203Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:2ced0839cd7e0ec274ca2828d00dc1624677e92a241fd92baf11b4e7ef0a6cdc
 verification:
     assurance_level: B
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-024.req.yaml b/specs/system/requirements/SYS-REQ-024.req.yaml
index ae0a20c..48e64d4 100644
--- a/specs/system/requirements/SYS-REQ-024.req.yaml
+++ b/specs/system/requirements/SYS-REQ-024.req.yaml
@@ -29,8 +29,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.258682Z"
+    reviewed_at: "2026-05-03T10:16:40.182744Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:136bd7caad59512d18614d978bdee933755925beec60d89cceab7c9771c1f8b3
 verification:
     assurance_level: B
     formalization_status: valid
@@ -46,7 +47,7 @@ history:
     created_by: human:cli
     created_at: "2026-04-14T00:00:00Z"
     last_modified_by: human:cli
-    last_modified_at: "2026-04-18T10:12:51Z"
+    last_modified_at: "2026-05-03T10:13:32Z"
 obligation_class: nominal
 lifecycle:
     change_history:
diff --git a/specs/system/requirements/SYS-REQ-025.req.yaml b/specs/system/requirements/SYS-REQ-025.req.yaml
index 6295224..fd2e989 100644
--- a/specs/system/requirements/SYS-REQ-025.req.yaml
+++ b/specs/system/requirements/SYS-REQ-025.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.260588Z"
+    reviewed_at: "2026-05-03T10:18:27.372694Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:3610a224f56df636f6731b00b9443d83b44ab1d59b7e9e0002a92b5e39383e60
 verification:
     assurance_level: B
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-026.req.yaml b/specs/system/requirements/SYS-REQ-026.req.yaml
index 3801b8a..7097b36 100644
--- a/specs/system/requirements/SYS-REQ-026.req.yaml
+++ b/specs/system/requirements/SYS-REQ-026.req.yaml
@@ -29,8 +29,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.26264Z"
+    reviewed_at: "2026-05-03T10:16:40.365826Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:5426885801a5d658f40be7e9cf1e898f34a7ca0439f4f5cfd6c0e14c201f02fa
 verification:
     assurance_level: B
     formalization_status: valid
@@ -46,7 +47,7 @@ history:
     created_by: human:cli
     created_at: "2026-04-14T00:00:00Z"
     last_modified_by: human:cli
-    last_modified_at: "2026-04-18T10:12:51Z"
+    last_modified_at: "2026-05-03T10:13:31Z"
 obligation_class: malformed_input
 lifecycle:
     change_history:
diff --git a/specs/system/requirements/SYS-REQ-027.req.yaml b/specs/system/requirements/SYS-REQ-027.req.yaml
index 8cf36dd..17fc234 100644
--- a/specs/system/requirements/SYS-REQ-027.req.yaml
+++ b/specs/system/requirements/SYS-REQ-027.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.264516Z"
+    reviewed_at: "2026-05-03T10:18:27.573205Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:00af509b08938a47a5279f4c66e9dfee2d5e49c61fe85f6d19de7362899f8105
 verification:
     assurance_level: B
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-028.req.yaml b/specs/system/requirements/SYS-REQ-028.req.yaml
index b997194..b794d86 100644
--- a/specs/system/requirements/SYS-REQ-028.req.yaml
+++ b/specs/system/requirements/SYS-REQ-028.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.266055Z"
+    reviewed_at: "2026-05-03T10:18:27.771149Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:ebf062c8b6965de324dbbfe6f39f4f1eb1616396e1cc2b3487e726401ae6a795
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-029.req.yaml b/specs/system/requirements/SYS-REQ-029.req.yaml
index bf0ea3c..3ed0a00 100644
--- a/specs/system/requirements/SYS-REQ-029.req.yaml
+++ b/specs/system/requirements/SYS-REQ-029.req.yaml
@@ -27,8 +27,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.267744Z"
+    reviewed_at: "2026-05-03T10:18:27.932137Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:5a1411091599832bc267af29b6352cd8eb21257507b690cc596d57da1239f317
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-030.req.yaml b/specs/system/requirements/SYS-REQ-030.req.yaml
index a887699..6d3743a 100644
--- a/specs/system/requirements/SYS-REQ-030.req.yaml
+++ b/specs/system/requirements/SYS-REQ-030.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.269539Z"
+    reviewed_at: "2026-05-03T10:18:28.092754Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:5a3a7d3de6469ee3c6645e5ffecba61e8f09f685f451437f3c130cdbc5d43202
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-031.req.yaml b/specs/system/requirements/SYS-REQ-031.req.yaml
index 63efe07..27ca335 100644
--- a/specs/system/requirements/SYS-REQ-031.req.yaml
+++ b/specs/system/requirements/SYS-REQ-031.req.yaml
@@ -27,8 +27,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.271261Z"
+    reviewed_at: "2026-05-03T10:18:28.252551Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:2d52e0fd4f8ee27f257d23953264d82f3f573035e586c7ddf0398d7bc5d8a7c7
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-032.req.yaml b/specs/system/requirements/SYS-REQ-032.req.yaml
index c62a8e8..6922e8d 100644
--- a/specs/system/requirements/SYS-REQ-032.req.yaml
+++ b/specs/system/requirements/SYS-REQ-032.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.272999Z"
+    reviewed_at: "2026-05-03T10:18:28.411964Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:93b836f8982466710145f816847c3271671306ba0ed7ea2e9f1a17977f092316
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-033.req.yaml b/specs/system/requirements/SYS-REQ-033.req.yaml
index 4e71dec..f77df16 100644
--- a/specs/system/requirements/SYS-REQ-033.req.yaml
+++ b/specs/system/requirements/SYS-REQ-033.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.274663Z"
+    reviewed_at: "2026-05-03T10:18:28.570048Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:0919990501e68632bbd67c2d16520580605c69e03b617c83c631b9d4f0ff83b1
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-034.req.yaml b/specs/system/requirements/SYS-REQ-034.req.yaml
index 96e2485..f325c7f 100644
--- a/specs/system/requirements/SYS-REQ-034.req.yaml
+++ b/specs/system/requirements/SYS-REQ-034.req.yaml
@@ -29,8 +29,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.276457Z"
+    reviewed_at: "2026-05-03T10:18:28.728109Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:2b3c3dc6603d4d1f733a52e8462d02a95d605b5d7c7de6a017d37ae20f5d02b2
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-035.req.yaml b/specs/system/requirements/SYS-REQ-035.req.yaml
index 2db9ba9..22911fd 100644
--- a/specs/system/requirements/SYS-REQ-035.req.yaml
+++ b/specs/system/requirements/SYS-REQ-035.req.yaml
@@ -30,8 +30,9 @@ traces:
         - mcdc_supplement_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.27977Z"
+    reviewed_at: "2026-05-03T10:18:28.888932Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:fd65733175fa84f535549a887501d1db2360ee4d70340a4a6f66a880f8f02d44
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-036.req.yaml b/specs/system/requirements/SYS-REQ-036.req.yaml
index 6c1da3f..69fc134 100644
--- a/specs/system/requirements/SYS-REQ-036.req.yaml
+++ b/specs/system/requirements/SYS-REQ-036.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.282098Z"
+    reviewed_at: "2026-05-03T10:18:29.095714Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:ee4286310bdd10d7538a12bc1e488e8e1727a9b9de0c6f6fbdad212be830c3b4
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-037.req.yaml b/specs/system/requirements/SYS-REQ-037.req.yaml
index 0e461e1..a223855 100644
--- a/specs/system/requirements/SYS-REQ-037.req.yaml
+++ b/specs/system/requirements/SYS-REQ-037.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.284107Z"
+    reviewed_at: "2026-05-03T10:18:29.254464Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:753e4235486cc2ab5b48706bb76e0c5a72ab7617452b8ad00688d0b9083611e8
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-038.req.yaml b/specs/system/requirements/SYS-REQ-038.req.yaml
index 4d8c548..2f92221 100644
--- a/specs/system/requirements/SYS-REQ-038.req.yaml
+++ b/specs/system/requirements/SYS-REQ-038.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.286376Z"
+    reviewed_at: "2026-05-03T10:18:29.413776Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:944068fc59004a672df4009de4fdf6b82f1448b9488d5a86cb7c0dc2a11bb7e2
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-039.req.yaml b/specs/system/requirements/SYS-REQ-039.req.yaml
index 08adaab..3fcb202 100644
--- a/specs/system/requirements/SYS-REQ-039.req.yaml
+++ b/specs/system/requirements/SYS-REQ-039.req.yaml
@@ -28,8 +28,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.288731Z"
+    reviewed_at: "2026-05-03T10:18:29.573216Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:ad83a1d3152f7d95d711a12a05246a7a69998c6d8ca0e98cc4f3e0a369f7543b
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-040.req.yaml b/specs/system/requirements/SYS-REQ-040.req.yaml
index 1b89780..b92be80 100644
--- a/specs/system/requirements/SYS-REQ-040.req.yaml
+++ b/specs/system/requirements/SYS-REQ-040.req.yaml
@@ -29,8 +29,9 @@ traces:
         - parser_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.290496Z"
+    reviewed_at: "2026-05-03T10:18:29.728996Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:a83d2dcc89315a1b8d9f36bb8652d0984e091f054979d7534a0be7f6f2e4c06d
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-041.req.yaml b/specs/system/requirements/SYS-REQ-041.req.yaml
index 688b9ce..79acf53 100644
--- a/specs/system/requirements/SYS-REQ-041.req.yaml
+++ b/specs/system/requirements/SYS-REQ-041.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.29222Z"
+    reviewed_at: "2026-05-03T10:18:29.88753Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:e666133fe66dc12f4a47d4a6862dca1de1fa44a7fb5ad3fed31439e89a4961f4
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-042.req.yaml b/specs/system/requirements/SYS-REQ-042.req.yaml
index 884bad4..e6b094a 100644
--- a/specs/system/requirements/SYS-REQ-042.req.yaml
+++ b/specs/system/requirements/SYS-REQ-042.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.293857Z"
+    reviewed_at: "2026-05-03T10:18:30.050376Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:25f1d1cebd3d9820a414a480d505e390c2132074113b5d3d0387aa92d84bfcb2
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-043.req.yaml b/specs/system/requirements/SYS-REQ-043.req.yaml
index 9da609b..6d1786d 100644
--- a/specs/system/requirements/SYS-REQ-043.req.yaml
+++ b/specs/system/requirements/SYS-REQ-043.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.29565Z"
+    reviewed_at: "2026-05-03T10:18:30.210471Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:06b25d1c512d31562d56548fc31eedb0a8a906566ff406096e2a28eea847fdbd
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-044.req.yaml b/specs/system/requirements/SYS-REQ-044.req.yaml
index b925938..fd48051 100644
--- a/specs/system/requirements/SYS-REQ-044.req.yaml
+++ b/specs/system/requirements/SYS-REQ-044.req.yaml
@@ -28,8 +28,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.297288Z"
+    reviewed_at: "2026-05-03T10:18:30.37309Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:765468345ff20751045696281c37f034c9e3376fbe672fee4a2dfd6cbb8489c8
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-045.req.yaml b/specs/system/requirements/SYS-REQ-045.req.yaml
index 456e567..dec7584 100644
--- a/specs/system/requirements/SYS-REQ-045.req.yaml
+++ b/specs/system/requirements/SYS-REQ-045.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.298877Z"
+    reviewed_at: "2026-05-03T10:18:30.533728Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:65827b0695011c5c9a3b315cf9fbf12f7691ed3c06259cb1ce220eab7bd6707e
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-046.req.yaml b/specs/system/requirements/SYS-REQ-046.req.yaml
index 48179e0..8da7089 100644
--- a/specs/system/requirements/SYS-REQ-046.req.yaml
+++ b/specs/system/requirements/SYS-REQ-046.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.300507Z"
+    reviewed_at: "2026-05-03T10:16:40.546169Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:2cc48660bc2e73763f9195096e707a0463e31dcbc5346e94601ee9eb7f5514a5
 verification:
     assurance_level: E
     formalization_status: valid
@@ -39,8 +40,8 @@ verification:
 history:
     created_by: agent:claude
     created_at: "2026-04-14T18:00:00Z"
-    last_modified_by: agent:claude
-    last_modified_at: "2026-04-14T18:00:00Z"
+    last_modified_by: human:cli
+    last_modified_at: "2026-05-03T10:13:32Z"
 obligation_class: sentinel_value_boundary
 lifecycle:
     change_history:
diff --git a/specs/system/requirements/SYS-REQ-047.req.yaml b/specs/system/requirements/SYS-REQ-047.req.yaml
index a8b4f35..b834b2d 100644
--- a/specs/system/requirements/SYS-REQ-047.req.yaml
+++ b/specs/system/requirements/SYS-REQ-047.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.302895Z"
+    reviewed_at: "2026-05-03T10:18:30.694118Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:ee0a44069229e2f5c814f5cadc82a3513964a75bbeb2dd9a4395cd84d91017c0
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-048.req.yaml b/specs/system/requirements/SYS-REQ-048.req.yaml
index 11ed662..55dd502 100644
--- a/specs/system/requirements/SYS-REQ-048.req.yaml
+++ b/specs/system/requirements/SYS-REQ-048.req.yaml
@@ -29,8 +29,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.304488Z"
+    reviewed_at: "2026-05-03T10:18:30.857178Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:663674077a44da8a35ebe519781cf8174ec9906316c68ab5e6b92761d2f11a47
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-049.req.yaml b/specs/system/requirements/SYS-REQ-049.req.yaml
index 0c0d681..30afa0a 100644
--- a/specs/system/requirements/SYS-REQ-049.req.yaml
+++ b/specs/system/requirements/SYS-REQ-049.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.305976Z"
+    reviewed_at: "2026-05-03T10:18:31.017349Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:30d6054c2a100d9ebb17a113ee52575852762699c93cefab25e5aecfeb1ca7aa
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-050.req.yaml b/specs/system/requirements/SYS-REQ-050.req.yaml
index 1ebb457..65e5107 100644
--- a/specs/system/requirements/SYS-REQ-050.req.yaml
+++ b/specs/system/requirements/SYS-REQ-050.req.yaml
@@ -28,8 +28,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.307834Z"
+    reviewed_at: "2026-05-03T10:18:31.176835Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:d7f7a9776996cf608051cb50d3aa3256406c24f6ea75ac5a96ff919f618956e8
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-051.req.yaml b/specs/system/requirements/SYS-REQ-051.req.yaml
index 0a33958..4160369 100644
--- a/specs/system/requirements/SYS-REQ-051.req.yaml
+++ b/specs/system/requirements/SYS-REQ-051.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.3098Z"
+    reviewed_at: "2026-05-03T10:18:31.337647Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:428af798b83ee2d46a4e93391a01af8779c412b4b546a7bdd027a532ff68fef6
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-052.req.yaml b/specs/system/requirements/SYS-REQ-052.req.yaml
index 33fe03d..9bdcfae 100644
--- a/specs/system/requirements/SYS-REQ-052.req.yaml
+++ b/specs/system/requirements/SYS-REQ-052.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.311526Z"
+    reviewed_at: "2026-05-03T10:18:31.49654Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:5c670371e049d6c59477040dc47889e147b5f6b6987871e0980d510be684841b
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-053.req.yaml b/specs/system/requirements/SYS-REQ-053.req.yaml
index 451397f..0dcf5af 100644
--- a/specs/system/requirements/SYS-REQ-053.req.yaml
+++ b/specs/system/requirements/SYS-REQ-053.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.313166Z"
+    reviewed_at: "2026-05-03T10:18:31.657749Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:eae2a44e7bee005db94783fb4eb3329ece3ade127311e4d5cf2d81e68ead7973
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-054.req.yaml b/specs/system/requirements/SYS-REQ-054.req.yaml
index 15e7ec3..79af4c1 100644
--- a/specs/system/requirements/SYS-REQ-054.req.yaml
+++ b/specs/system/requirements/SYS-REQ-054.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.316582Z"
+    reviewed_at: "2026-05-03T10:18:31.816044Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:8000eda38b19178c94a3a36a1b7ec126c831787566eb20194769bf5fa905b80c
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-055.req.yaml b/specs/system/requirements/SYS-REQ-055.req.yaml
index 9f24d52..6b5fb36 100644
--- a/specs/system/requirements/SYS-REQ-055.req.yaml
+++ b/specs/system/requirements/SYS-REQ-055.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.318192Z"
+    reviewed_at: "2026-05-03T10:18:31.977344Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:58273ed3db6b6850d2eeafc6b3de5ab038d3f2cb7d676944bd99f4dd42d20712
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-056.req.yaml b/specs/system/requirements/SYS-REQ-056.req.yaml
index 8bcd0e9..9f8ded2 100644
--- a/specs/system/requirements/SYS-REQ-056.req.yaml
+++ b/specs/system/requirements/SYS-REQ-056.req.yaml
@@ -28,8 +28,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.319859Z"
+    reviewed_at: "2026-05-03T10:18:32.137021Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:96298e0214997572255b6995c93603359689dd3b34662b3033dbbd7d08a5f3fc
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-057.req.yaml b/specs/system/requirements/SYS-REQ-057.req.yaml
index 8bd8e13..80b58de 100644
--- a/specs/system/requirements/SYS-REQ-057.req.yaml
+++ b/specs/system/requirements/SYS-REQ-057.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.321415Z"
+    reviewed_at: "2026-05-03T10:18:32.297382Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:c377a2da755f532fa17180543d1b62c5c0762e9eae8bef1256a33dd7eda1c43d
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-058.req.yaml b/specs/system/requirements/SYS-REQ-058.req.yaml
index 3cf930e..345924f 100644
--- a/specs/system/requirements/SYS-REQ-058.req.yaml
+++ b/specs/system/requirements/SYS-REQ-058.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.322981Z"
+    reviewed_at: "2026-05-03T10:18:32.45807Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:83fde4279f84702e52f9aa0a93a7bebef31a1d8be83a89afd956a5411910eb1c
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-059.req.yaml b/specs/system/requirements/SYS-REQ-059.req.yaml
index ec7409b..0aa29ed 100644
--- a/specs/system/requirements/SYS-REQ-059.req.yaml
+++ b/specs/system/requirements/SYS-REQ-059.req.yaml
@@ -28,8 +28,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.324929Z"
+    reviewed_at: "2026-05-03T10:18:32.674641Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:7df829d268b2de87779a41518410c31f57b8f05e3c3ce216b3ff7c08a66fa865
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-060.req.yaml b/specs/system/requirements/SYS-REQ-060.req.yaml
index 95ddb2e..7bd66c5 100644
--- a/specs/system/requirements/SYS-REQ-060.req.yaml
+++ b/specs/system/requirements/SYS-REQ-060.req.yaml
@@ -28,8 +28,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.328049Z"
+    reviewed_at: "2026-05-03T10:18:32.877805Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:a4bc88f1240f27bba665a06fa297bbc8e417b174525bad85e6b980c643f29ae5
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-061.req.yaml b/specs/system/requirements/SYS-REQ-061.req.yaml
index 2571f09..bf0a47d 100644
--- a/specs/system/requirements/SYS-REQ-061.req.yaml
+++ b/specs/system/requirements/SYS-REQ-061.req.yaml
@@ -28,8 +28,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.330213Z"
+    reviewed_at: "2026-05-03T10:18:33.077212Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:235138c95d29db295438eb59545e353fece4cab7d1a10d4a25eb57143a1a6b9f
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-062.req.yaml b/specs/system/requirements/SYS-REQ-062.req.yaml
index 3c83caa..c8a4f9e 100644
--- a/specs/system/requirements/SYS-REQ-062.req.yaml
+++ b/specs/system/requirements/SYS-REQ-062.req.yaml
@@ -28,8 +28,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.331794Z"
+    reviewed_at: "2026-05-03T10:18:33.239346Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:d53cacec93940fd95e5929330a18241d570c71efd4be111519b145663adeeb8d
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-063.req.yaml b/specs/system/requirements/SYS-REQ-063.req.yaml
index 8feafac..17cf19d 100644
--- a/specs/system/requirements/SYS-REQ-063.req.yaml
+++ b/specs/system/requirements/SYS-REQ-063.req.yaml
@@ -28,8 +28,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.333757Z"
+    reviewed_at: "2026-05-03T10:18:33.400192Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:be0a16a8793a861d23790b640b0883fef3bb456854f785abfa9e391654d2d699
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-064.req.yaml b/specs/system/requirements/SYS-REQ-064.req.yaml
index 4a6e9c2..3924206 100644
--- a/specs/system/requirements/SYS-REQ-064.req.yaml
+++ b/specs/system/requirements/SYS-REQ-064.req.yaml
@@ -28,8 +28,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.335626Z"
+    reviewed_at: "2026-05-03T10:18:33.626348Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:8812ff02150cebe73a2e53e014477e52a5ddf33a82dfc536cd6d18692406cb65
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-065.req.yaml b/specs/system/requirements/SYS-REQ-065.req.yaml
index 6fc2103..7b45fad 100644
--- a/specs/system/requirements/SYS-REQ-065.req.yaml
+++ b/specs/system/requirements/SYS-REQ-065.req.yaml
@@ -28,8 +28,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.337537Z"
+    reviewed_at: "2026-05-03T10:18:33.837201Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:0309d672032b8d3c3abcd6dbd5dd0760fc3c5a9ba3750477986f531f222fa27d
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-066.req.yaml b/specs/system/requirements/SYS-REQ-066.req.yaml
index 8787ed5..af500ad 100644
--- a/specs/system/requirements/SYS-REQ-066.req.yaml
+++ b/specs/system/requirements/SYS-REQ-066.req.yaml
@@ -28,8 +28,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.339226Z"
+    reviewed_at: "2026-05-03T10:18:34.000109Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:ae8d0cb45905b340551d2abe403768af6a274839af01bd4fc0c4f3a69dfabb2a
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-067.req.yaml b/specs/system/requirements/SYS-REQ-067.req.yaml
index 0094ba5..ac189bf 100644
--- a/specs/system/requirements/SYS-REQ-067.req.yaml
+++ b/specs/system/requirements/SYS-REQ-067.req.yaml
@@ -28,8 +28,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.340937Z"
+    reviewed_at: "2026-05-03T10:18:34.165092Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:c493c300c95fd17906e61cfc71f7f296b08ed14961e5e751367634192fcc63a4
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-068.req.yaml b/specs/system/requirements/SYS-REQ-068.req.yaml
index fe7ecf2..bff5969 100644
--- a/specs/system/requirements/SYS-REQ-068.req.yaml
+++ b/specs/system/requirements/SYS-REQ-068.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.343749Z"
+    reviewed_at: "2026-05-03T10:18:34.329959Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:4fa0e24cb94337138fccbae387b42f787af89f1d885fcef8c43575795eacca5e
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-069.req.yaml b/specs/system/requirements/SYS-REQ-069.req.yaml
index c3b2cfd..69c95d8 100644
--- a/specs/system/requirements/SYS-REQ-069.req.yaml
+++ b/specs/system/requirements/SYS-REQ-069.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.345303Z"
+    reviewed_at: "2026-05-03T10:18:34.493571Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:1b775e780f879e0952110b600e48e2beda8ae4164b46c6c6fa65139d1f17d7e4
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-070.req.yaml b/specs/system/requirements/SYS-REQ-070.req.yaml
index 2b49b1b..74121e2 100644
--- a/specs/system/requirements/SYS-REQ-070.req.yaml
+++ b/specs/system/requirements/SYS-REQ-070.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.34706Z"
+    reviewed_at: "2026-05-03T10:18:34.657698Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:310db5ed1534d542539d423749e3143cb58e4c48d1adc9baab0e289d93242bf4
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-071.req.yaml b/specs/system/requirements/SYS-REQ-071.req.yaml
index f9f98fe..90f179f 100644
--- a/specs/system/requirements/SYS-REQ-071.req.yaml
+++ b/specs/system/requirements/SYS-REQ-071.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.34892Z"
+    reviewed_at: "2026-05-03T10:18:34.821963Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:b9a3356882d401979c80203ca6c2e36c51fe95bf487770beb25479903df2bca9
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-072.req.yaml b/specs/system/requirements/SYS-REQ-072.req.yaml
index f7b257d..65e80d0 100644
--- a/specs/system/requirements/SYS-REQ-072.req.yaml
+++ b/specs/system/requirements/SYS-REQ-072.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.351032Z"
+    reviewed_at: "2026-05-03T10:18:34.992927Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:909eb877fe993125bf27075e1c1d8f97b7cdcda0b749ee7ea8db62145fe8c309
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-073.req.yaml b/specs/system/requirements/SYS-REQ-073.req.yaml
index d04dfbf..886975f 100644
--- a/specs/system/requirements/SYS-REQ-073.req.yaml
+++ b/specs/system/requirements/SYS-REQ-073.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.353929Z"
+    reviewed_at: "2026-05-03T10:18:35.152785Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:c5e3cbc16032e485bd9cd3649b75c5699e8b9fdd4a7882ab1af72030856de723
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-074.req.yaml b/specs/system/requirements/SYS-REQ-074.req.yaml
index 5181e4d..98535bd 100644
--- a/specs/system/requirements/SYS-REQ-074.req.yaml
+++ b/specs/system/requirements/SYS-REQ-074.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.356819Z"
+    reviewed_at: "2026-05-03T10:18:35.317386Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:f7f18c5dc9c1fe1a020e270f7671bdabd2e0aeee0e47fc617577f99130cf327b
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-075.req.yaml b/specs/system/requirements/SYS-REQ-075.req.yaml
index 6a9616b..13a6573 100644
--- a/specs/system/requirements/SYS-REQ-075.req.yaml
+++ b/specs/system/requirements/SYS-REQ-075.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.358431Z"
+    reviewed_at: "2026-05-03T10:18:35.479255Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:8c37b471c237aa7b4d53ee398e7e9e43c7972d35e8ab291b6f2e05453c51e769
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-076.req.yaml b/specs/system/requirements/SYS-REQ-076.req.yaml
index 6d1b4ca..84d26c1 100644
--- a/specs/system/requirements/SYS-REQ-076.req.yaml
+++ b/specs/system/requirements/SYS-REQ-076.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.360142Z"
+    reviewed_at: "2026-05-03T10:18:35.643785Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:421d94bbba69b8f59333f647362ea893cf7ac5905711d6b2e1caab3c31933efc
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-077.req.yaml b/specs/system/requirements/SYS-REQ-077.req.yaml
index 9dfb5f7..2c11702 100644
--- a/specs/system/requirements/SYS-REQ-077.req.yaml
+++ b/specs/system/requirements/SYS-REQ-077.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.361853Z"
+    reviewed_at: "2026-05-03T10:18:35.807311Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:130dfad53660469ab388ce2be7ec303110a900251e04bf877a601e13d5123b25
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-078.req.yaml b/specs/system/requirements/SYS-REQ-078.req.yaml
index 96e74b4..b201d9e 100644
--- a/specs/system/requirements/SYS-REQ-078.req.yaml
+++ b/specs/system/requirements/SYS-REQ-078.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.363629Z"
+    reviewed_at: "2026-05-03T10:18:35.971358Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:84b2e28cb74f70fe39eaceced24d3685622d96ebfc331b8f86a70c7f4555831b
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-079.req.yaml b/specs/system/requirements/SYS-REQ-079.req.yaml
index eb0c8a2..fee9b8e 100644
--- a/specs/system/requirements/SYS-REQ-079.req.yaml
+++ b/specs/system/requirements/SYS-REQ-079.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.366484Z"
+    reviewed_at: "2026-05-03T10:18:36.134933Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:671c5206f61076de5ec79a0fbe50dff97beb1de03268343c001b4b484d8d15c0
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-080.req.yaml b/specs/system/requirements/SYS-REQ-080.req.yaml
index 4f8d4ac..c5fd594 100644
--- a/specs/system/requirements/SYS-REQ-080.req.yaml
+++ b/specs/system/requirements/SYS-REQ-080.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.36905Z"
+    reviewed_at: "2026-05-03T10:18:36.296855Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:4f9410df801e2775946210f126af4af951fb339a865b5ec906b1eca18cf02921
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-081.req.yaml b/specs/system/requirements/SYS-REQ-081.req.yaml
index 6aae14d..036110b 100644
--- a/specs/system/requirements/SYS-REQ-081.req.yaml
+++ b/specs/system/requirements/SYS-REQ-081.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.37335Z"
+    reviewed_at: "2026-05-03T10:18:36.461205Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:fb0bb7adaa6428d7be271575f914a7b2295b4ceb9e64d4596672a6f7243dbf12
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-082.req.yaml b/specs/system/requirements/SYS-REQ-082.req.yaml
index 4250fd6..0964ae5 100644
--- a/specs/system/requirements/SYS-REQ-082.req.yaml
+++ b/specs/system/requirements/SYS-REQ-082.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.375212Z"
+    reviewed_at: "2026-05-03T10:18:36.623593Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:c2a033dc58a65f881ae221d81a2f7f0580939ff4249b1923f018ea7adf0a299a
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-083.req.yaml b/specs/system/requirements/SYS-REQ-083.req.yaml
index 7a5632b..fe74e75 100644
--- a/specs/system/requirements/SYS-REQ-083.req.yaml
+++ b/specs/system/requirements/SYS-REQ-083.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.381331Z"
+    reviewed_at: "2026-05-03T10:18:36.789124Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:095683c9985f659f8ab158730348931ebda0944028b7620072dc94ff3f2e1573
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-084.req.yaml b/specs/system/requirements/SYS-REQ-084.req.yaml
index 026ddb5..eec35a2 100644
--- a/specs/system/requirements/SYS-REQ-084.req.yaml
+++ b/specs/system/requirements/SYS-REQ-084.req.yaml
@@ -27,8 +27,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.383321Z"
+    reviewed_at: "2026-05-03T10:18:36.950415Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:d592062c7b540ee8248f8a94032209d9c4f5d1539e5db21554242ae2b0861575
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-085.req.yaml b/specs/system/requirements/SYS-REQ-085.req.yaml
index c1fc251..4eb825f 100644
--- a/specs/system/requirements/SYS-REQ-085.req.yaml
+++ b/specs/system/requirements/SYS-REQ-085.req.yaml
@@ -26,8 +26,9 @@ traces:
         - deep_spec_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.38525Z"
+    reviewed_at: "2026-05-03T10:18:37.112896Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:980f5673f7103b2399c83783b294ac395aed7f507bd83532d39d28df4620409d
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-086.req.yaml b/specs/system/requirements/SYS-REQ-086.req.yaml
index 72cf0c3..2df1afb 100644
--- a/specs/system/requirements/SYS-REQ-086.req.yaml
+++ b/specs/system/requirements/SYS-REQ-086.req.yaml
@@ -26,8 +26,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.38869Z"
+    reviewed_at: "2026-05-03T10:18:37.276125Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:a650dec592cffba744893ce15d228f40a52e571ff43d66020c04c28de6783b7a
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-087.req.yaml b/specs/system/requirements/SYS-REQ-087.req.yaml
index b38cbb6..7969b5d 100644
--- a/specs/system/requirements/SYS-REQ-087.req.yaml
+++ b/specs/system/requirements/SYS-REQ-087.req.yaml
@@ -26,8 +26,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.392504Z"
+    reviewed_at: "2026-05-03T10:18:37.39752Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:6bc530484ee1e0e87244e1fd7cf6f61ae167b6a35cdce8911e9e0277c581cf43
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-088.req.yaml b/specs/system/requirements/SYS-REQ-088.req.yaml
index 6a8af69..724bbc9 100644
--- a/specs/system/requirements/SYS-REQ-088.req.yaml
+++ b/specs/system/requirements/SYS-REQ-088.req.yaml
@@ -26,8 +26,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.394238Z"
+    reviewed_at: "2026-05-03T10:18:37.518269Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:b73f132c392dc6ccd367a2dc2b94c95e5dd7768bb6134f6d12d6665bca49f0b9
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-089.req.yaml b/specs/system/requirements/SYS-REQ-089.req.yaml
index 7112616..1dbd3ea 100644
--- a/specs/system/requirements/SYS-REQ-089.req.yaml
+++ b/specs/system/requirements/SYS-REQ-089.req.yaml
@@ -27,8 +27,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.395928Z"
+    reviewed_at: "2026-05-03T10:18:37.640923Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:951c5bc5534f5b014934ce485832e33953bf29adbe8d81a04fd78dffddd20940
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-090.req.yaml b/specs/system/requirements/SYS-REQ-090.req.yaml
index 543fb8f..df6eba9 100644
--- a/specs/system/requirements/SYS-REQ-090.req.yaml
+++ b/specs/system/requirements/SYS-REQ-090.req.yaml
@@ -26,8 +26,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.397946Z"
+    reviewed_at: "2026-05-03T10:18:37.761879Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:6f4cf035d2a3502862fac6765db8cb9cf4e98a2dfa013b66dfed2d2ab8dda6c7
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-091.req.yaml b/specs/system/requirements/SYS-REQ-091.req.yaml
index 8df7a22..de15e72 100644
--- a/specs/system/requirements/SYS-REQ-091.req.yaml
+++ b/specs/system/requirements/SYS-REQ-091.req.yaml
@@ -26,8 +26,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.39952Z"
+    reviewed_at: "2026-05-03T10:18:37.882313Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:c1d382087608ecf2e5be46fa37db4c065e29bd078fa1ffd8c8b10c6d5990baec
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-092.req.yaml b/specs/system/requirements/SYS-REQ-092.req.yaml
index 944002b..a843ac5 100644
--- a/specs/system/requirements/SYS-REQ-092.req.yaml
+++ b/specs/system/requirements/SYS-REQ-092.req.yaml
@@ -27,8 +27,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.401217Z"
+    reviewed_at: "2026-05-03T10:18:38.004764Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:c225bbc135f8b37ed381616150fd5c7053fac23e2d242c8684457fd52c40a019
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-093.req.yaml b/specs/system/requirements/SYS-REQ-093.req.yaml
index c720ad8..c392f26 100644
--- a/specs/system/requirements/SYS-REQ-093.req.yaml
+++ b/specs/system/requirements/SYS-REQ-093.req.yaml
@@ -27,8 +27,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.402978Z"
+    reviewed_at: "2026-05-03T10:18:38.127532Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:e99e0a452da7c646d0f8aac02d031b1ce7c72d2a5ee4882a6cc7b603ed0774db
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-094.req.yaml b/specs/system/requirements/SYS-REQ-094.req.yaml
index f11cd73..1cc6d27 100644
--- a/specs/system/requirements/SYS-REQ-094.req.yaml
+++ b/specs/system/requirements/SYS-REQ-094.req.yaml
@@ -28,8 +28,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.40471Z"
+    reviewed_at: "2026-05-03T10:18:38.249902Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:59d6875acd369892d68e20d8798a6222bc0d98bd1b7dcdfa6d4881f26db42226
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-095.req.yaml b/specs/system/requirements/SYS-REQ-095.req.yaml
index 38f4661..8fce170 100644
--- a/specs/system/requirements/SYS-REQ-095.req.yaml
+++ b/specs/system/requirements/SYS-REQ-095.req.yaml
@@ -28,8 +28,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.406694Z"
+    reviewed_at: "2026-05-03T10:18:38.370944Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:a1da1cea358072c417beb713121da894754d7a4ed18d07babca09eef1c2a84c6
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-096.req.yaml b/specs/system/requirements/SYS-REQ-096.req.yaml
index 318265e..9cb6df9 100644
--- a/specs/system/requirements/SYS-REQ-096.req.yaml
+++ b/specs/system/requirements/SYS-REQ-096.req.yaml
@@ -27,8 +27,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.408545Z"
+    reviewed_at: "2026-05-03T10:18:38.490333Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:91d3e28e06447ec39c239ef32f5b347e913d39d66db2d8a6661700a202690b8d
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-097.req.yaml b/specs/system/requirements/SYS-REQ-097.req.yaml
index 131be69..6bfd24f 100644
--- a/specs/system/requirements/SYS-REQ-097.req.yaml
+++ b/specs/system/requirements/SYS-REQ-097.req.yaml
@@ -28,8 +28,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.411835Z"
+    reviewed_at: "2026-05-03T10:18:38.610416Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:9b3260afad5ffc70de237d38fca5f6649131472ba0b1ddbeea5dc40b141c5a15
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-098.req.yaml b/specs/system/requirements/SYS-REQ-098.req.yaml
index b74fde9..5c2bd09 100644
--- a/specs/system/requirements/SYS-REQ-098.req.yaml
+++ b/specs/system/requirements/SYS-REQ-098.req.yaml
@@ -28,8 +28,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.413785Z"
+    reviewed_at: "2026-05-03T10:18:38.742786Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:1b47bc8afa2b20ec55cec068fcb6a5375ec1b2100779c5d28de568dad73bcbf5
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-099.req.yaml b/specs/system/requirements/SYS-REQ-099.req.yaml
index 13492fc..7e9f52d 100644
--- a/specs/system/requirements/SYS-REQ-099.req.yaml
+++ b/specs/system/requirements/SYS-REQ-099.req.yaml
@@ -28,8 +28,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.416614Z"
+    reviewed_at: "2026-05-03T10:18:38.864508Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:49efb1563e56cd612ba56e8209553e60126cf8e906c6bb134d80a8b00350fdbf
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-100.req.yaml b/specs/system/requirements/SYS-REQ-100.req.yaml
index f1da6f1..dbc0246 100644
--- a/specs/system/requirements/SYS-REQ-100.req.yaml
+++ b/specs/system/requirements/SYS-REQ-100.req.yaml
@@ -26,8 +26,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.418352Z"
+    reviewed_at: "2026-05-03T10:18:38.986143Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:1598bef15f860ede4843070a780d3aec881c349afe36039514861b7a6c072113
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-101.req.yaml b/specs/system/requirements/SYS-REQ-101.req.yaml
index aaadce3..480ffc6 100644
--- a/specs/system/requirements/SYS-REQ-101.req.yaml
+++ b/specs/system/requirements/SYS-REQ-101.req.yaml
@@ -27,8 +27,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.420041Z"
+    reviewed_at: "2026-05-03T10:18:39.110041Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:54769c14573e841ffa91595416b78302c7abf47c63ab248256b71ac2bcb7cb12
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-102.req.yaml b/specs/system/requirements/SYS-REQ-102.req.yaml
index e138365..454a445 100644
--- a/specs/system/requirements/SYS-REQ-102.req.yaml
+++ b/specs/system/requirements/SYS-REQ-102.req.yaml
@@ -28,8 +28,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.422612Z"
+    reviewed_at: "2026-05-03T10:18:39.233429Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:79ced44babf8149442cf7ae26cba97f5a8dbfcfd020371ebe06d27b19b8bd0f9
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-103.req.yaml b/specs/system/requirements/SYS-REQ-103.req.yaml
index d17b451..19136be 100644
--- a/specs/system/requirements/SYS-REQ-103.req.yaml
+++ b/specs/system/requirements/SYS-REQ-103.req.yaml
@@ -26,8 +26,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.424115Z"
+    reviewed_at: "2026-05-03T10:18:39.353897Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:5937aebf878020cb16d7cebd9bad15aedd21b58fd13d76df5d55a04c18e9895c
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-104.req.yaml b/specs/system/requirements/SYS-REQ-104.req.yaml
index 94e9b84..31aefc9 100644
--- a/specs/system/requirements/SYS-REQ-104.req.yaml
+++ b/specs/system/requirements/SYS-REQ-104.req.yaml
@@ -26,8 +26,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.427271Z"
+    reviewed_at: "2026-05-03T10:18:39.47434Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:709f182112b42570511605a0022675208f2034a3a026060b607bb2e0fbd5fa5e
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-105.req.yaml b/specs/system/requirements/SYS-REQ-105.req.yaml
index 0bc342b..4d6c263 100644
--- a/specs/system/requirements/SYS-REQ-105.req.yaml
+++ b/specs/system/requirements/SYS-REQ-105.req.yaml
@@ -27,8 +27,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.429295Z"
+    reviewed_at: "2026-05-03T10:18:39.597319Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:0be811efba0d173b7c213400b0c3c0161a5314fd8f776214e429dbdc2695c6d5
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-106.req.yaml b/specs/system/requirements/SYS-REQ-106.req.yaml
index dd4e32e..c269b81 100644
--- a/specs/system/requirements/SYS-REQ-106.req.yaml
+++ b/specs/system/requirements/SYS-REQ-106.req.yaml
@@ -29,8 +29,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.43084Z"
+    reviewed_at: "2026-05-03T10:18:39.720692Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:9fead2ef259accb391654b859fa2e5e60062cff11a49882eb0cc0ea248a3c2c3
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-107.req.yaml b/specs/system/requirements/SYS-REQ-107.req.yaml
index 515eccc..7756b1a 100644
--- a/specs/system/requirements/SYS-REQ-107.req.yaml
+++ b/specs/system/requirements/SYS-REQ-107.req.yaml
@@ -29,8 +29,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.432288Z"
+    reviewed_at: "2026-05-03T10:18:39.841954Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:833f4859c5f5916d76b2b0f30434583f7009bc0de5387bbdf484fe943bd1a584
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-108.req.yaml b/specs/system/requirements/SYS-REQ-108.req.yaml
index 80823cd..293a504 100644
--- a/specs/system/requirements/SYS-REQ-108.req.yaml
+++ b/specs/system/requirements/SYS-REQ-108.req.yaml
@@ -26,8 +26,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.433955Z"
+    reviewed_at: "2026-05-03T10:18:39.962611Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:f5af289defb5e0ebefd037f7a5a9f0cb92099240adc5251c53caf11aee5a0034
 verification:
     assurance_level: E
     formalization_status: valid
diff --git a/specs/system/requirements/SYS-REQ-109.req.yaml b/specs/system/requirements/SYS-REQ-109.req.yaml
index b6ec394..540126e 100644
--- a/specs/system/requirements/SYS-REQ-109.req.yaml
+++ b/specs/system/requirements/SYS-REQ-109.req.yaml
@@ -27,8 +27,9 @@ traces:
         - obligation_property_test.go
     documented_by_extra:
         - README.md
-    reviewed_at: "2026-04-27T06:25:19.43595Z"
+    reviewed_at: "2026-05-03T10:18:40.088506Z"
     reviewed_by: human:leonidbugaev
+    reviewed_fingerprint: sha256:3cc8694bf0ba2db68e513c1006f8b014b685aa3b8b1d7f654932f8e92079b7de
 verification:
     assurance_level: E
     formalization_status: valid