v4.4.1

• Fixed (#761): the legacy replay trace object wrapper is now exactly {"events": [...]} —
  a misspelled key (for example eventz), a non-array events value, or extra keys are
  rejected with the wrapper diagnostic instead of being silently tolerated. Focused native
  accepting and rejecting contracts pin the wrapper and its full public projection, and a
  new liveness-witness replay matrix rejects isolated state, action, and loop corruptions
  of every leadsTo lasso case the retired Python comparison covered.
• Fixed (#786): the frozen Python compatibility reference now lets an explicit
  inline implements action correspondence override the same requirements-process
  auto map, so the manual dialect-conformance corpus no longer rejects a valid
  arity-changing refinement mapping.
• Fixed (#826): unresolved indexed init writes now conservatively collide with every concrete key on the same logical map root instead of silently accepting aliasing writes with equal values.
• Fixed (#832): native fslc check now fails closed for compose alias and typed
  binder resolution gaps that verify already rejected. A declared alias no
  longer authorizes a nonexistent qualified type such as core.NoSuchType, and
  an undeclared alias-shaped expression in an init if condition receives the
  same type check as an assignment right-hand side. Unknown typed binder names
  are also rejected uniformly in properties, action postconditions, and init.
  Errors retain the author's spelling and source location; valid imported types,
  binder types, and state conditions remain accepted.
• Fixed (#904): legacy solver-free BFS now excludes intended terminal states from deadlock reporting while preserving true deadlocks, matching explicit BFS and symbolic BMC.
• Required (#742): merge readiness now rejects Git-tracked citations to missing
  docs/DESIGN-*.md sections, including colon and explicit-section forms, without
  letting untracked documents satisfy them; calibrated folded, list-tail, historical,
  and accepting controls preserve the boundary.
• Required (#746): the five frozen-Python and DESIGN-index coupled-change metatests now run in the required pre-merge automation lane while remaining outside the Rust-native product gate.
• Required (#761): native Rust tests now bind every corpus verify result class to
  its exact public process exit code; pin the business, requirements, and governance
  induction CLI contracts; exercise all nine leadsTo case-by-corruption replay cells
  with exact diagnostics; compare the complete legacy object-wrapper envelopes
  while rejecting wrong keys, value types, and extra root keys; compare the
  complete stable refine envelope projection with a live, reasoned exclusion for
  solver-selected implementation traces; and own all sixteen stable induction
  envelope/exit cases with live exclusions and negative controls before the Python
  parity harnesses are retired.
• Required (#898): Merge readiness now runs ShellCheck with masked-return analysis and fail-closed tracked-script enumeration, plus a calibrated direct-syntax Bash-version guard lint that scans expansions in unquoted heredocs, ignores literal heredoc data, and documents its dynamic-execution boundary.
• Required (#761): the sixteen induction CLI cases the retired Python parity harness compared
  are now owned by a native golden contract (induction_cli_contract.rs) — full stable
  envelopes with reason-coded, live-hit-checked exclusions, a calibrated cache-mode control,
  and an idempotent golden regeneration path.
• Required (#761): refinement corpus parity now compares the full stable projection of every
  corpus envelope against a checked-in golden with reason-coded exclusions and a
  dead-exclusion check, replacing the result/kind/exit-only assertion the retired Python
  harness was stronger than.
• Documented (#757): recorded the first natural production partial re-run — a GitHub-side
  artifact-service transient failed one test shard on a docs-only PR, gh run rerun --failed
  re-ran only that shard, and the aggregator accepted the mixed-attempt cohort
  (attempts=1,1,2), recovering in one shard's time instead of a full three-shard re-run.
• Documented (#761): recorded all 17 Python/Rust parity-harness dispositions and deletion preconditions without deleting a harness, including seven native-owner gaps, the full-envelope helper dependency, the parked Phase-3 comparison, three native-migration candidates, and five bounded manual controls.
• Documented (#904): accepted the #761 native BFS/BMC migration plan, including the
  checked 20-model decision matrix, bidirectional witness validation, terminal-aware
  deadlock repair, rejecting controls, and safe Python-harness and helper-binary
  retirement order.
• Required (#906): the induction contract golden is now part of the release-commit
  regeneration set. It records each envelope's versions block, so a version bump made the
  complete product gate fail comparing the previous version against the new one; docs/RELEASE.md
  step 6 now names its UPDATE_INDUCTION_CLI_CONTRACT regeneration and
  is_release_bump_path names the golden, keeping the release commit exempt from a
  fragment for that path.

v4.4.0

• Changed (#760): native CLI tests now cover deterministic DOT and Mermaid
  analysis export, DOT escaping from valid FSL input, and rejection of non-graph
  export requests.
• Fixed (#617): Normalize Windows source-path separators in the optional-verdict census so classifications and consumer checks remain live across platforms.
• Fixed (#741): tools/build_site_reference.py now rejects a docs/LANGUAGE.ja.md that
  reorders ## sections relative to docs/LANGUAGE.md while keeping the section count equal.
  render_language_tree() previously compared only len(ja_sections) == len(en_sections) and
  then paired the two files positionally, so a same-count reorder passed generation silently and
  attached a Japanese section body to the wrong English anchor and blurb — exactly the drift
  docs/DESIGN-docs-site.md D7 and this tool's own docstring already claimed was caught. The
  fix checks each positional pair's leading numeric section prefix ("2" from "2. Types"/
  "2. 型") and raises SystemExit naming both headings and the position on a mismatch, needing
  no new maintained ja/en heading-name table. That per-position check is only sound if
  docs/LANGUAGE.md's own numbers are unique, so a second assertion now rejects a duplicated
  English section number directly, naming the duplicate, instead of leaving uniqueness an
  unstated precondition. Rejecting controls (a same-count reordering fixture and a duplicate-number
  fixture) and an accepting control (the real, untouched files) are all in
  tests/test_site_reference_snapshot.py.
• Fixed (#757): sharded Rust and semantic-mutation artifacts now use stable logical names so a failed
  shard can be rerun without discarding successful peers. Provenance, checksums, shard identity, and
  exact-union controls reject incomplete or incompatible mixed-attempt cohorts.
• Fixed (#762): restore the native root CLI-help contract formatting while retaining concise summaries for every top-level command.
• Fixed (#786): Prove the native-only enum abstraction refinement exclusion by neutralizing only its registered block and reject stale or shadowed registry entries.
• Fixed (#795): failed trusted Actions cache-budget audits now maintain one deduplicated issue and close it after recovery.
• Fixed (#818): a compose document with an undeclared component alias inside a
  top-level init block's forall binder no longer panics past the public
  API boundary. rewrite_compose_statements now returns Result and its
  caller in lower_compose propagates with ?, so fsl_core::parse_kernel_source
  returns Err(CoreError) with the "unknown alias" message instead of the
  process aborting. A rejecting control exercises the reproduction through
  parse_kernel_source; an accepting control confirms a correctly declared
  alias used in a forall binder still lowers successfully.
• Fixed (#821): the explicit-engine init duplicate-write check now rejects a forall i { m[i] = ... } write that overlaps a later flat m[K] = ... write to the same concrete key K,
  whether or not the two values agree. It previously tracked forall-indexed writes at
  whole-variable granularity while flat writes were tracked per key, so an overlapping flat
  write with an agreeing value was silently accepted and one with a conflicting value fell
  through to the unrelated "init constraints are unsatisfiable" diagnostic instead of the
  duplicate-write rule's own message.
• Fixed (#822): Offer use in LSP completion and enforce reasoned parity with rename-validation keywords.
• Fixed (#840): Cache-budget audit wiring validation now reports malformed sibling workflows without a traceback.
• Fixed (#843): fslc testgen no longer bakes a Monitor rollback as a conformance expectation. The
  fixed-seed walk is a concrete Monitor run capped at 100 steps and independent of
  --depth, so it could reach a violation the bounded verification testgen runs
  first proved absent within depth; the violating StepResult was discarded and
  the rolled-back (unchanged) state was recorded as that step's expected. A
  conforming implementation failed the generated test, an implementation that
  silently did nothing passed it, and --target pytest -- which drives the walk live
  -- reached the opposite conclusion from the five baked targets on the same input.
  The walk now fails closed, reporting the violation with the same
  result:"violated" envelope, exit code, property, step, and replayable trace
  verify reports, and writing no harness.
• Fixed (#846): the Rust workspace is clean again under clippy 1.98.0, whose
  new deny-by-default manual_is_variant_and and chunks_exact_to_as_chunks
  lints turned main red with no repository change, because every CI job uses
  the unpinned dtolnay/rust-toolchain@stable. Both rewrites are
  semantics-preserving. CI named only two sites, since cargo aborts at the first
  failing crate; enumerating with --keep-going found four, and the fix was
  also checked against the pinned 1.88.0 MSRV that release.yml uses so
  as_chunks cannot break the release build after PR CI passes on stable.
• Fixed (#847): Scheduled and manually dispatched product-gate failures now reconcile through the post-merge CI reporter.
• Fixed (#851): Cache-budget audit workflow-name validation now rejects case-only,
  surrounding-whitespace, and compatibility-Unicode collisions with the reporter source.
• Fixed (#855): map-key diagnostics now explain when a const shadows a member of
  the map key enum and advise renaming one of the colliding declarations.
• Fixed (#856): Replaced workflow line scanners with required PyYAML-backed audits that preserve source diagnostics, reject ambiguous YAML, and pin the privileged post-merge reporter checkout and execution shape.
• Fixed (#857): rust tests and rust checks have cold-build margin. A cold
  rust tests shard was measured at 30m04s against its 30-minute budget and was
  cancelled, turning the aggregate rust workspace required context red;
  docs/DESIGN-ci.md had recorded that outcome as an unobserved risk. The budgets
  move to 45 and 30 minutes, sized from measured cold durations (24m59s / 27m12s /
  30m04s for the shards, 16m35s for rust checks) against warm baselines of
  9-11m and 2m. #747 records why cold builds recur: two concurrent pull requests
  exceed the 10 GiB Actions cache ceiling and evict each other, so a budget with
  no cold margin turns a routine eviction into a failed required context.
• Fixed (#858): the public types that carry a verification outcome are now #[must_use] on the
  type rather than only on the functions returning them. Result is already
  #[must_use], so monitor.step(x).map_err(..)?; satisfied the compiler while the
  inner StepResult -- which owns violation -- was dropped as a statement value;
  annotating the function is redundant against Result and closed nothing. With the
  attribute on the type, cargo clippy -- -D warnings rejects the discard where
  the outcome is returned directly, which is the shape behind the testgen walk
  bug. It does not reach an outcome wrapped in Option: #[must_use] does not
  propagate through Option, and Option is not itself #[must_use], so a
  -> Result<Option<Outcome>, E> signature stays undetectable by this mechanism
  (issue #868).
• Fixed (#860): recognize integer constants as distinct concrete keys when checking init coverage for integer-keyed maps.
• Fixed (#861): make the release Linux linkage guard reject binaries dynamically linked to libz3, with accepting and rejecting ldd fixtures. The separate GLIBC behavioral-control finding is tracked in #865.
• Fixed (#862): Map<Int, V> is rejected at check time in every grammar-reachable type position, preventing verification from materializing an unbounded key domain.
• Fixed (#868): Detect discarded optional verification verdicts through direct and source-declared alias return types, and assert expected bounded-liveness observations.
• Fixed (#871): Corrected the release-linkage calibration to name both conditions
  behind the former hole: ! exempted the failing pipeline from errexit, and
  the final clean iteration then supplied the loop's status.
• Fixed (#873): generated cargo-mutants liveness exclusions now derive their
  line-scoped expressions from the maintained source anchors instead of requiring
  hand-copied line numbers.
• Fixed (#875): causal expectation replay now reports a within 0 liveness
  violation found in the initial state instead of returning a false pass.
• Fixed (#882): the generated cargo-mutants configuration's freshness check no longer fails unconditionally on a CRLF checkout. mutants.toml and its template are pinned to LF via .gitattributes and the comparison normalises line endings, so the gate's verdict does not depend on checkout configuration. Found by the promotion-only Windows solver lane after #880 merged, because that lane is skipped on pull requests.
• Fixed (#883): text checkouts are pinned to LF and #858's source-inspection control normalises CRLF reads, so its adjacent-line assertions do not depend on checkout configuration.
• Required (#802): cache-budget audit workflow wiring now has parsed-YAML calibration controls for every validator rejection and diagnostic CLI input failures.
• Required (#812): mutate now preserves malformed causal parser diagnostics through an executable error-envelope parity control.
• Required (#845): cache-budget audit workflow-name uniqueness now blocks main
  merges through merge readiness.
• Required (#850): Native CLI regression coverage now detects incorrect failed-link
  identities and composed action maps in multi-link fslc refine chains.
• Required (#865): Added accepting and rejecting fixture controls for the Linux
  release GLIBC ABI guard. The required product gate now exercises the deployed
  guard with compliant GLIBC_2.39 and rejecting GLIBC_2.40 `...

v4.3.0

• Fixed (#753): git apply silently skips every file in a patch, and exits zero, when the
  fault-operator scratch checkout is not its own git repository root -- git resolves the
  scratch to the enclosing repository, where everything under it lives beneath rust/target/
  and is git-ignored (Skipped patch '<path>'., exit 0). The scratch then compiled
  unfaulted, every detector passed because there was nothing to detect, and the harness
  recorded that as a detector gap. sync_scratch guarded this with [ -e "$scratch/.git" ],
  which tests the wrong property: an empty or partial .git from a restored CI cache
  satisfies it and suppresses the repair, which is why the failure appeared only in CI and
  varied run to run. The guard now requires git rev-parse --show-toplevel inside the scratch
  to equal the scratch, and git apply --verbose turns a Skipped patch line into a nonzero
  status.

• Fixed (#753): the implementation fault-operator harness now witnesses that a fault
  reached what it measured instead of inferring it. A primary still passed under the fault verdict has two causes with different owners -- the detector does not cover the
  seam (a real gap) or the detector never saw the fault (a harness defect) -- and
  tools/run-fault-operators.sh previously reported the first whenever the second was
  true, because it treated a zero-exit git apply plus a clean build as proof of arrival.
  The symptom was the same operator returning different verdicts on different runs of one
  revision, which made unrelated pull requests unmergeable through the semantic mutation
  required context. Two fail-closed witnesses now run before any verdict: every file a
  patch names must differ byte-for-byte from the pristine copy after the patch applies,
  and, of the two artifacts a detector can execute -- the test harness binary, read back
  from cargo's own Executable <target> (<path>) line, and the fslc executable a
  detector may spawn via env!("CARGO_BIN_EXE_fslc") -- at least one must differ from the
  digest recorded for it under the no-op control. Both are checked because an operator's
  fault normally reaches exactly one: a patch under rust/fslc/tests/** changes the test
  binary, a patch under rust/fslc/src/** changes fslc. A byte-identical pair cannot
  arise from compilation nondeterminism, so the binary witness fires only on real artifact
  reuse.
  The source witness carries its own negative control,
  rust/fslc/tests/fault_operators/controls/identical-after-apply.patch, a hunk that
  applies cleanly while leaving the file unchanged and must be refused; the binary witness
  is calibrated by live mutation and has no fixture, recorded as such in
  docs/DESIGN-conformance-harness.md.

• Decided (#737): the shared-edit merge-conflict spike closes as GO for CHANGELOG
  fragments only (C1) and NO-GO for fragmenting the contract documents (C2), recorded
  in the new accepted docs/DESIGN-changelog-fragments.md. The load-bearing evidence is a
  replay of history at d72ac8d: of 22 genuinely concurrent branch pairs (interval overlap
  plus git merge-base --is-ancestor false both ways, conflicts detected with
  git merge-tree --write-tree), 16 conflict, CHANGELOG.md is a conflicting file in 16 of
  16, and the three current-era conflicts have it as the only conflicting file — while
  fragmenting docs/LANGUAGE.md/docs/LANGUAGE.ja.md/skills/fsl/reference.md resolves
  zero additional pairs (every contract-document conflict co-occurs with an implementation
  conflict in one early-Python cluster), which is #737's own no-go condition, and would put
  a generated layer upstream of the required site reference freshness check. The record
  carries the six fail-closed negative controls (missing or empty fragment, duplicate id,
  order determinism plus conformance on both the category and id sort components,
  unaggregated-at-release plus bidirectional direct-edit, aggregation conservation against
  silent entry drops and against truncation, and fragment-name conformance), each with a
  calibrated rejecting fixture and named diagnostic, the six migration sites, the rollback
  method, and the reversal condition. <category> follows this repository's bullet
  lead-word convention, not Keep a Changelog's: the measured [Unreleased] body has zero
  ### subheadings and already uses Documented and Decided, so the aggregator emits
  bullets rather than introducing subheadings. Implementation is deliberately not included. The LANGUAGE.md /
  LANGUAGE.ja.md section-alignment enforcement is untouched by C1; a pre-existing
  count-only gap in that enforcement found during the evaluation is tracked as #741.

• Documented (#738): the command-family extraction spike's result as re-evaluation evidence in
  docs/DESIGN-rust-components.md. Section 10's first trigger — three unrelated command changes
  failing on fslc orchestration coupling — has fired (the exit-code chain alone supplies five)
  and is adjudicated: the harmful coupling is one contract policy implemented at more than one
  site, which a vertical command-family split cannot remove, so further family extraction is
  no-go and a new crate is rejected for lack of independent version/dependency/consumer evidence
  (C1 remains the selected candidate). The one executed extraction (causal.rs, #393 / PR #440)
  produced zero confirming samples and two counter-shaped ones in 13 days — both workspace-wide
  refine changes, so the falsifier section 8 already named appeared in shape while the effect
  stays unconfirmed, not disproven; the response that measurably worked is policy single-owner
  extraction (spec_load.rs, outcome.rs, literate_access.rs): after 743bc7a gave spec-load
  classification one owner, main.rs involvement fell 379 → 179 → 16 lines across its follow-up
  series. Section 8 records the discriminator the spike leaves behind, and it is stated in terms of
  implementation sites, not call sites — one contract policy implemented at more than one site is
  harmful coupling; an arm that only calls into a single library owner is cohesion, however many arms
  call it. That distinction is the whole rule: counting call sites makes every centralized policy look
  coupled, because centralizing is what produces callers, and counting only recurrence misses a policy
  whose arms were mismatched from birth, does not capture Case C, and returns both verdicts on a
  history where a duplicated policy was later centralized. Touch rate and line count discriminate
  nothing (post-extraction main.rs churn median 29 lines, 26 of 50 commits at wiring scale). The
  negative control is c455e50 (#697), which the rule rejects: it touches main.rs, spans three
  crates and changes concrete-verification behaviour, yet its policy — CONCRETE_PROBE_BUDGET
  governing the single find_boundary_violation — is defined once and merely referenced from four
  call sites, with the budget value appearing nowhere else in rust/ outside a test comment, an
  11-line wiring change in main.rs, and no later fix landing on a second arm. 64bfb55 is
  explicitly not the control: two of its three defects are multi-site policies, so by this rule it
  contains coupling — the rule working, not failing — and two claims made for it are withdrawn, the
  single-file pickaxe over a symbol the broken copy never contained, and the false assertion that it
  deleted a duplicated hint string (git show 64bfb55^:rust/fslc/src/main.rs has no coverage_hint
  occurrence). Also recorded: the accepting/rejecting controls a future extraction would have to
  calibrate, and the measurable changed-owner rollback rule any future extraction PR must carry.
  Documentation only; no Rust behavior changed.

• Fixed (#720 Finding 1): rust-tests' cargo-nextest --partition count:K/3 balanced pre-merge
  shards by test count, not wall clock, so five binaries holding ~77% of the suite's sequential time
  (refine_corpus_parity, explicit_engine, injection_detector_matrix, corpus_check_sweep,
  issue_226_auto_engine) could land unevenly across shards — measured spreads of 2.2x and 3.1x
  between the fastest and slowest shard on two runs of the same commit, now both
  recorded in docs/DESIGN-ci.md (previously only the 2.2x run was). check_rust_tests in tools/check-native-integration.sh now
  pins those five binaries to specific shards via a checked-in
  tools/rust-test-shard-groups.txt and cargo nextest's binary_id(=…) filterset, unpartitioned,
  while every other test still goes through the original count-partition, scoped to exclude every
  pinned binary. Coverage cannot silently drop: an unlisted binary simply falls into the
  count-partitioned leftover as before, and tools/check-shard-union.sh's existing full.txt/shard.txt
  guard needed no shape change to keep validating the result. Added check-shard-union.sh check-groups, a narrower guard that fails closed if the grouping file pins a binary-id the live
  workspace no longer has or pins one binary to two shards, plus new accepting/rejecting selftest
  cases (including a whole-binary-dropped fixture) wired into the existing merge readiness / automation contracts lane. .github/workflows/ci.yml is unchanged — the required rust workspace
  context, its if: always() aggregator, and the shard-union contract all keep their exact shape.
  Measured, and the second form delivers: the slowest shard — the only quantity
  rust workspace waits on — fell from 15.6 min to 12.2 min and the spread from 3.1x to 1.17x
  (warm-cache runs 31076668077 and 31081427765 attempt 2; shard wall clocks 12.2 / 10.85 / 10.46 min,
  clean shard union on both). The first form delivered ~0.1 min and this entry previously said so;
  two measured defects explain the gap. The cost model was wrong twice: packing by each binary's
  sequential total, then...

v4.2.0

• Fixed native Rust business-dialect precedence policies so every <Entity> reaching ... must have passed through ... lowers to deduplicated history
  state, transition updates, the attributed no-bypass invariant, and its
  dominated-set stability invariant. Native BMC, induction, and explicit-state
  regressions now fail if the lowering is hollowed back into a no-op (#681).
• Hardened semantic migrations against another hollow accepted construct:
  behavior-bearing variants now require executable or fail-closed controls,
  the precedence bypass gallery and a curated implementation fault operator
  calibrate native detection, all four business policy variants have native
  rejecting controls, and both agent harnesses retain soundness findings until
  they are fixed or linked to an issue; the merge-readiness automation lane
  executes that harness contract on every pull request (#681).
• Accepted the measured correlated-saga-history design: retain one-hot event
  flags as current-transition observations and add a dedicated
  correlation-indexed six-phase saga map in a follow-up. The maintained
  two-correlation fixture measures the three candidates as ×1 reused effect
  state, 32 sticky-event valuations versus 6 one-hot valuations, and 36
  dedicated saga-progress valuations; a negative control proves global sticky
  flags alias correlations (#662).
• Reached Seq pop/head/at/index operations are now uniformly
  partial_op violations in property context across Monitor BFS, explicit
  verification, native/browser symbolic BMC, and CLI rendering. The contract
  includes terminal and leadsTo, so neither can turn an undefined Seq read
  into a solver-selected deadlock decision or vacuously false antecedent.
  Symbolic phantom slots can no longer fabricate a property verdict or
  reachable witness; property-context / and % zero totalization is
  unchanged (#650).
• Native BMC now distinguishes structurally impossible reachable targets
  from depth-limited ones. over_constrained entries carry an irreducible
  blocking_requires set computed in an independent solver session, so path
  UNSAT cannot poison the classification and diagnostic queries cannot perturb
  native/browser witness projection (#634).
• Fixed fslc typestate silently omitting locally guarded read/query actions.
  They now appear as explicit state-preserving self-loops, and generated
  TypeScript preserves the caller's exact phantom state instead of widening a
  multi-state guard (#635).
• Bounded LSP workspace discovery now scans only direct siblings for a document
  opened outside every registered workspace root, preventing an arbitrary
  parent such as /tmp from becoming an unbounded recursive index while
  preserving explicit workspace and sibling cross-file behavior (#623).
• fslc explain counterfactual weakening now evaluates only the invariant and
  reachable outcomes it actually reports, and explicitly marks liveness as
  skipped. Quantified leadsTo checks no longer multiply every safety mutant's
  runtime while their results are discarded (#633).
• Added a calibrated vacuous_deadline lane that proves a generated deadline's
  age remains zero across every transition, catching state-changing urgent
  handlers that evade the narrower global urgency_freeze proof. The SLA worker
  example now consumes slack and fails when its deadline is tightened (#632).
• Added the M13 FSL Logic Test (#673): deterministic valid finite models now
  carry stable seed/case IDs, a single-case replay command, machine-coupled
  generation/dialect/metamorphic inventory, and named concrete-versus-symbolic
  agreement edges over verdicts, clean-run reachables/action coverage, exact
  witnesses, replay, and successor admission. PR and scheduled tiers emit a
  fail-closed completeness report; scheduled evidence spans three seeds and
  three depths (1,152 cases), delayed violations carry nontrivial actions, and
  a comparator corruption control exercises structural shrinking and minimized replay, while a deduplicated corpus owns
  future real disagreements. Generation volume does not promote public
  assurance or change product output.
• Added the M13 soundness-critical semantic mutation gate (#672). A pinned
  cargo-mutants 27.1.0 pilot now mutates exact P2 bounded-verification,
  witness projection/replay, identity/location, and result-fold decisions;
  reviewed semantic operators cover unknown/backend failures, inclusive
  depth, witness omissions, replay bypass, and false-success folds that
  generic token mutation cannot express. Pull requests run changed-scope
  mutants plus every curated control, with the detector package named
  explicitly even when a diff selects only fsl-verifier; product events run
  the complete accepted scope. Survivors, timeouts, stale seams, missing output,
  and stale equivalence records fail closed; this calibrates detection power
  without promoting any public assurance class or changing product output.
• Added CI-internal Triangulated Assurance (#670): a federated, fail-closed
  registry now requires one raw observation, two explicitly independent
  semantic lineages, all three executable agreement edges, positive/negative
  calibration, and honest scope. Initial pilots cover compound native outcome
  conservation, symbolic-witness/concrete-replay identity (including
  state/step/kind/location corruption controls), and token-based dialect
  dispatch across the syntax library, CLI, and LSP. A calibrated common-mode
  fault executes a production-classifier substitution for the registered P1
  independent observer and declares its shared model lineage; no public
  assurance class, JSON field, or exit code changes.
• Fixed raw fsl_verifier::verify_bounded* calls bypassing the automatic
  action-context partial-operation check. Symbolic BMC now reports replayable
  partial_op evidence for ordered guards, reached action bodies, and
  ensures, including selected-property, supplied-state, and nondeterministic
  init paths; native CLI and Worker no longer source partial_op from their
  separate concrete boundary pre-scan (#651).
• Fixed domain saga lowering so effect-owned outcome events cannot bypass the
  effect correlation guard through weaker generated observation actions. Three
  observation actions disappear from generated kernels (#640).
• fslc domain check now preserves the nested kernel's warnings and
  action_coverage, so vacuity and generated-action coverage diagnostics remain
  visible to domain users instead of being dropped by the stable projection
  (#641).

v4.1.0

• Semantic Assurance Matrix slices 2/3 add source-derived expr (24
  Expr + 4 AggregateKind rows), types (9 TypeRef + 3 TypeDef
  rows), and dialects (all 10 frontends! keywords) axes for issue #537
  C3. A 25-model deterministic C6 family now checks all evaluator-reachable
  expression variants and all type rows across Monitor BFS / explicit / BMC,
  with a known-violating paired control for every model, while Call/Stage,
  standalone refinement checks, and the Worker's missing agent path are
  recorded with fail-closed evidence.

• rust/fslc/tests/typed_agreement.rs introduces the C6 typed generative /
  metamorphic cross-engine agreement suite (issue #537 C6 slice 1, issue
  #648, docs/DESIGN-conformance-harness.md "Typed generative / metamorphic
  agreement"): a deterministic structural generator (15 domain-axis models

  • 4 operation-axis models, no randomness) builds checked KernelModels
    and compares Monitor BFS / explicit / BMC verdicts, replay, and successor
    admission, plus seven metamorphic relations (alpha rename, BOM/trivia,
    inline-vs-explicit init, disjoint assignment reorder, domain-size
    boundary, short-circuit/partial/Euclidean duality, entity/number sugar vs
    lowered type) each with a positive test and a negative control. Two
    confirmed cross-engine findings are recorded as re-measured, self-retiring
    exclusions rather than normalized away: verify_bounded's symbolic Seq
    encoding treats an out-of-range head() read in property context as
    defined with an out-of-bound value instead of undefined (a spurious
    violated/invariant, disagreeing with the concrete engines' correct
    error); and verify_bounded alone never performs LANGUAGE.md's automatic
    "Partial operations" check in action context at all (the CLI's
    --engine bmc classification comes from a separate concrete pre-scan,
    find_boundary_violation, not the solver).

• corpus_expectation_manifest.rs and evidence_corpus_manifest.rs give every
  declared examples/gallery/{valid,errors,adversarial} fixture and every
  causal/agent/ai_component evidence-only document exactly one native
  owner (issue #645, #537 C4 residual). 12 of ~38 declared gallery fixtures had
  never been run by any native test — tests/test_gallery.py was the only
  oracle, and it is frozen-Python, outside tools/check-native- integration.sh — and nothing walked the corpus for an unregistered
  causal/fsl-ai document. All reproduce their declared result/kind/exit
  natively; no defect surfaced. corpus_check_sweep.rs's
  every_corpus_spec_checks_ok_or_declares_its_error no longer duplicates the
  check-targeted half of that claim, now owned by the new manifest instead.
  A shared rust/fslc/tests/support/mod.rs replaces the corpus-walk helpers
  corpus_check_sweep.rs and refine_corpus_parity.rs each carried their own
  copy of.

• rust/fslc/tests/assurance_matrix.rs introduces the federated Semantic
  Assurance Matrix skeleton (issue #537 C3 slice 1,
  docs/DESIGN-assurance-matrix.md): axis modules under tests/assurance/
  own their rows (read from existing single-owner registries, never copied)
  and declared columns; every (row, column) cell carries a
  machine-rechecked citation (path + anchor, re-read from the working tree
  each run); blank required cells and stale/fabricated citations fail CI;
  negative controls prove both checks can actually fail. Slice 1 axes:
  outcome_kind (7 Monitor kinds × Monitor/CLI), violation_kind (12
  engine kinds × BMC/induction, #646), and properties (5 KernelModel
  property kinds × BMC/explicit/induction/replay).

• fsl-verifier's free-form Violation.kind strings (BmcViolation/
  InductionCti/RankFailure) are now single-owned in
  rust/fsl-verifier/src/violation_kind.rs instead of scattered string
  literals (#646). Reading the emission sites directly (not transcribing
  issue #646's own citation list) found 12 live values, not the 9 the issue
  named — pending_not_preserved, non_decreasing_helpful_action, and
  non_helpful_action_increases_measure had no exercising fixture anywhere
  in the corpus before this change. No emitted JSON violation_kind value
  changes by a single byte. Part of #537 C3 slice 1
  (docs/DESIGN-assurance-matrix.md).

• The kernel AST projection no longer re-serializes every subtree, and is named
  for what it is: python_ast is now kernel_ast_v1 (#622). json! calls
  serde_json::to_value on each interpolated operand, and the operands were
  already-built Value children, so every level deep-copied the subtree below
  it — O(depth) stack and O(n²) time per level, spent inside
  recursion::guard rather than around it, which is why #620's guard could not
  see it. Nodes are now built with Value::Array(vec![...]). The name was
  history, not contract: the tagged-array shape came from the frozen Python
  reference, but the shape is now the input to fsl-kernel-ast-v1+sha256, which
  two digests hash (approval::spec_digest,
  document_digest::spec_digest_from_kernel). Deleting or reshaping it would
  drift every approval record already in a user's repository; renaming the
  function changes nothing a user can observe.

• PredicateExpander::expand_expr and public_kernel::expr_json are now
  guarded too, bringing the #620 table to ten cycles (#622). Neither was
  reachable by the #620 witness, whose depth lived in a refinement mapping; a
  second generator that puts the same depth inside an invariant — the shape
  the digests actually project — aborted both immediately. expr_json is the
  more interesting of the two: it called the already-guarded infer_type once
  per level, so the guard ran every level, and the crash still landed in
  stacker::_grow itself, because the check happens on entry and this frame is
  large enough that the stack could fall from above the red zone to below what
  growing it costs. A guard on a called function is not a guard on the calling
  cycle. fslc check, document claims, and kernel now complete on a
  2000-deep invariant.

• Byte-identity was proven by differential sweep, not self-consistency: the
  pre-change and post-change binaries were run over all 211 corpus specs under
  document claims, analyze, and testgen, comparing stdout byte for byte —
  633 comparisons, 0 mismatches. The sweep's own control came first and mattered:
  run against itself the old binary disagreed with itself on 14 files, because
  testgen stamps wall-clock elapsed_s/check_elapsed_s into its envelope.
  Those two keys are blanked; nothing else is normalized.

• tools/run-fault-operators.sh no longer measures a previous run's fault.
  The scratch checkout shares one CARGO_TARGET_DIR across steps, and rsync -a
  restores the reverted sources with the worktree's mtimes -- which can be older
  than rlibs that an operator step compiled with its patch applied. Cargo then
  judged those crates fresh and linked the faulted rlib into the no-op control's
  binary, so a warm run reported a detector red for a fault that was no longer
  in the source. Every sync_scratch now touches the files any patch names
  (taken from the diffs' +++ b/ headers), which puts cargo's mtime comparison
  on the side of rebuilding without discarding the rest of the warm cache.
  Reproduced deterministically -- cold run green, every warm run red,
  cargo clean -p fsl-syntax green again -- and verified by restoring clean
  sources into a fault-built scratch: before the fix cargo recompiled nothing
  and the rebuilt binary still aborted on the #620 witness (exit 134); after it,
  fsl-syntax recompiles and the witness exits 0. This is the second
  scratch-fidelity defect in this harness after the .git marker (#611), and
  the first to be caught by the no-op control rather than by inspection --
  a harness that trusted its cache would have called the operator calibrated
  while measuring the fault itself.

• Recursion over a spec's expression structure now grows the stack instead of
  aborting the process (#620). #617 made every platform agree on an 8 MiB
  stack; it did not make the recursion bounded, and a generated 160-stage
  refinement trio still killed fslc with has overflowed its stack — exit
  134, no JSON envelope, no exit code the outcome contract could read. The
  fix is stacker::maybe_grow at each recursion cycle entry, not a depth
  limit: a limit would put an arbitrary constant into the language contract
  and reject legitimate machine-generated specs, and this class was found by
  exactly such a spec. Every current answer is preserved and none is added.
  The measurement in #620 named two sites; a debugger's innermost frame only
  shows whichever site ran out first, so guarding one exposed the next, six
  rounds over. Eight cycles across three crates are now guarded —
  SyntaxParser::expression, SyntaxExpr::into_kernel,
  SyntaxExpr::render_source, Expr::kernel_ast_v1 (fsl-syntax),
  elaborate_enum_conversions, infer_type, validate_expression
  (fsl-core), and eval (fsl-verifier) — behind one
  fsl_syntax::recursion::guard that owns the red zone and segment size, so a
  future site cannot pick its own constants. Six of the eight are
  crash-witnessed; render_source and infer_type are not, and each says so at
  its definition together with the N at which it was observed to survive
  unguarded, so a reader can tell a measured guard from a speculative one.
  refine now proves a 1000-stage trio (a 2000-long right-nested if chain)
  that previously aborted at 160, and check/fmt return their ordinary
  envelopes on the same file.

  The invariant is not fully met, and #622 tracks the rest. Expr::kernel_ast_v1
  builds its result with json!, which calls serde_json::to_value on each
  already-built child and re-serializes the whole subtree — O(depth) stack per
  level, inside the guard rather tha...

v4.0.0

Changed

• Pull requests into main now run the complete Linux product evidence — rust workspace
  and WASM — instead of deferring it to after the merge. Only the cross-platform
  native Z3 4.16 matrix (macOS, Windows) stays post-merge under FSL_OPTIMISTIC_CI. The
  bounded merge readiness lane is kept as a sub-minute fail-fast check; adding
  --all-targets to its cargo check was tried and reverted after measuring 12m42s in
  CI, since rust workspace now compiles and runs those targets on the same pull
  request. 103 of the repository's 124
  integration test files live in fslc, fsl-tools, fsl-verifier and fsl-lsp, none of
  which merge readiness runs, so that evidence only reached main post-merge
  (docs/DESIGN-ci.md).

Fixed

• fslc ai check now rejects duplicate dataset and evaluator declaration
  names, which the frozen reference has always rejected
  (src/fslc/ai_project.py:237-241). Native validated only three of the five
  declaration kinds, so a project declaring dataset Shared twice exited 0 and
  reported datasets: ['Shared', 'Shared']. Because a dataset X reference
  resolves by name, two declarations sharing one made resolution depend on
  declaration order — the false green was silently picking a winner, not merely
  echoing a name twice (#571).
• Native now emits kind:"name" for name-resolution failures instead of
  collapsing them into semantics, making every member of the
  docs/DESIGN-v1.md §7.2 closed set reachable. duplicate state variable,
  duplicate enum member, duplicate def, duplicate parameter in def,
  def ... parameter is shadowed by binder, and undefined predicate were all
  reported as semantics, sending an agent following the §8 repair protocol
  down the wrong branch. CoreError and ModelError now carry the
  classification the frontend already determined, and it survives through
  SpecLoadError to the one renderer — the same direction as #484, rather than
  adding patterns to the message-string classifier, which has no text these
  diagnostics share and would silently reclassify them on any wording change.
  Messages are byte-identical and no other kind moves.
  examples/gallery/errors/name_duplicate_state_variable.fsl is the corpus
  golden the classification never had; its absence is why this survived #484 and
  #555. Its loc now names the redeclaration rather than the first binding:
  the diagnostic carried no span of its own, so it fell back to the
  message-derived heuristic, which finds the earlier x and pointed a repair
  agent at the innocent declaration (#565).
• A duplicate enum member diagnostic now points at the repeated member rather
  than the first declaration of that name. SpecItem::Enum carried no
  per-member span, so the report fell back to source_diagnostic's
  message-derived heuristic — the first token matching the quoted name — which
  for a duplicate is the earlier, innocent declaration by construction. For
  enum E { A, B } enum F { B, C } it named B in E (2:15) instead of the
  redeclaration in F (3:12). A loc that exists but names the wrong construct
  is worse than none: docs/DESIGN-v1.md G2 assumes the position is correct.
  SpecItem::Enum now carries member_spans positionally parallel to
  members, the same shape SpecItem::Struct gained in #555 and the same the
  domain surface already used, and the diagnostic attaches the offending
  member's own span (#576).
• The native<->Worker parity corpus's unsupportedDocuments exclusions in
  rust/fsl-wasm/test-browser.mjs are now self-retiring. The map excluded 32
  refinement/agent/causal documents from the comparison and recorded only a
  document type, so if the Worker ever gained a verb for one of them the
  exclusion would keep suppressing the comparison forever -- the shape that
  left #556's divergent path with zero corpus coverage. Each entry now carries
  the measured reason it holds, and every excluded document is probed on the
  Worker alone: the recorded premise is that the Worker cannot analyze it, and
  the day that stops being true the harness fails and names the entry to
  remove. The compared-pair count is unchanged at 351 -- no exclusion was
  retired and no document newly compared -- and the run now also reports
  exclusionProbes. This stays a capability exclusion, not a
  tolerated-difference allowlist: the envelopes are still not compared for
  these documents and no verdict, location, or exit-code difference is
  allowlisted (#568).
• The 28 refinement-typed entries in rust/fsl-wasm/test-browser.mjs's
  unsupportedDocuments exclusion map are retired; the compared native<->Worker
  parity corpus grows from 359 to 415 cases and exclusionProbes drops from 32
  to 4 (agent + 3 causal only). The exclusion premise was measured stale: #574
  gave native and the Worker one shared classifier (kernel_load_error) for a
  document whose top level parses but is not Kernel-shaped, so check/verify
  on every refinement document in the corpus now produce byte-identical
  semantics/"spec has no state block" envelopes on both surfaces -- the
  exclusion was suppressing zero divergence. specs/cart_refines.fsl is now
  asserted by name to remain a compared parity case, the same way
  duplicateWriteCase/governanceErrorCase are, so a future silent
  re-exclusion fails loudly instead of only showing up as a quiet drop in
  parityCases.length (#577).
• Every parity-corpus exclusion is now checked to have native answer
  non-error, before the Worker launches. This closes the blindness that let
  the 28 retired entries go stale: #568's probe tests only the Worker side
  (result !== "error"), which detects agreement only when native answers
  non-error — agreement then forces the Worker non-error too. Native
  answered error for all 28 refinement documents, so two sides erroring
  looked identical whether or not the errors matched, and the probe stayed
  green for weeks. Native answers non-error for all 4 surviving exclusions
  (ok for agent, causal_model_checked for the 3 causal), so the cheap
  Worker-only probe is sound for them — and the day an exclusion is added
  whose native side errors, this assertion names it instead of silently
  reverting the corpus to that blind state. Full envelope comparison was
  evaluated and rejected: the causal envelope carries no versions block, so
  validateEnvelope throws before any comparison, which is a normalizer
  rejection rather than a verdict. The assertion runs in the candidate loop
  rather than beside the Worker probe because it depends on nothing but
  native, turning a ~6-minute failure into a sub-second one (#577).
• The browser parity harness no longer embeds a developer's absolute path.
  rust/fsl-wasm/test-browser.mjs hardcoded one machine's
  /Users/<name>/Library/Caches/ms-playwright/chromium_headless_shell-1208/...
  Chrome, the only committed line in the repository containing an absolute home
  path, which AGENTS.md forbids. Playwright installs each build under its own
  version directory and has changed the internal layout between them — both
  chrome-mac/headless_shell and
  chrome-headless-shell-<platform>/chrome-headless-shell exist on a machine
  with two builds installed — so the version, the platform directory, and the
  binary name are all discovered rather than spelled out, newest build first
  (#583).
• A dropped or half-open Chrome DevTools Protocol connection no longer hangs
  the browser gate forever. cdp() returned a promise that only the message
  listener could ever settle, with no timeout and no socket close/error
  handler, so a response that never arrived hung Node indefinitely; the
  surrounding for (attempt < 360) loop is not a bound when a single await
  inside it never returns. Because the hang left the process to be killed
  externally, the finally that terminates Chrome and removes the profile
  directory never ran: an orphaned chrome-headless-shell (parent gone,
  4h13m old) and seven leaked profile directories were measured on one machine,
  and an orphan over two hours old blocked a later gate. cdp() now times out
  naming the method, and both socket close and error reject every
  outstanding request, so the failure is loud and the cleanup runs (#584).
• rust/fsl-wasm/web/cases.mjs no longer claims its smoke cases are compared
  against native. The native comparison keyed on them (nativeVerdict) was
  removed in d30f456 when the corpus-wide parity run replaced it, but the
  now-unused import { cases } in test-browser.mjs and the header comment
  promising "the parity comparison stays honest" both survived, so the file
  documented a check that no longer existed. The import is removed and the
  comment states what is true: these 9 inline sources are Worker smoke cases
  checked in the browser against their own expected, and the 415-case corpus
  comparison supersedes the removed one (#585).
• A kernel-stage failure inside a use ... from component now reports the
  parent's use declaration as its loc, and names the component's own path
  and position in the message. The two used to be mixed: the path came from the
  parent (source_file) while the line and column came from the component's
  parser, so check on
  examples/gallery/errors/semantics_compose_component_parse_failure.fsl
  reported …:7:18 — and line 7 of that file is a comment. A location in the
  wrong file is worse than none, and docs/DESIGN-v1.md G2 requires the output
  JSON alone to say where the problem is. loc is {line, column} with no
  file in all five of its docs/DESIGN-v1.md examples, so it can only mean a
  position in the file the envelope is about; the use declaration is that
  position, and it is also the line to look at first. The message now reads
  `component "" failed to parse ( at ::<c...

v3.1.0

Fixed

• Native induction CTIs now emit the documented heuristic suggested_invariants for monotone
  scalar and uniformly initialized Map counters without changing the proof verdict; quantified Map
  suggestions choose a collision-free binder so the emitted expression remains reusable (#337).
• Native induction lemma handling accepts candidates for selected invariant and trans properties,
  proves each candidate without original user properties, then uses and recommends only the first
  independently proved candidate excluding each successive CTI (#336).
• fslc scenarios now emits the shortest replayable action-coverage trace even
  when the covered action reaches a terminal state before the requested depth,
  including requirements transitions guarded by Bool inputs (issue #405).
• fslc mutate --by-requirement now attributes acceptance and forbidden kills
  through explicit requirement annotations on the failed trace declaration
  instead of reporting the linked requirement as empty_formalization (issue
  #407). Explicit requirement relations are preserved even when their ID equals
  a trace-case ID, while synthetic case relations remain excluded. Duplicate
  acceptance or forbidden IDs are rejected so attribution is unambiguous.
• fslc mutate now adjudicates singleton bound mutants whose empty domain
  produces no action instances instead of panicking in bounded verification;
  overflowing integer and bound neighbors are omitted (issue #406).
• Explicit domain-effect success_event, failure_event, and timeout_event
  roles now override event-name heuristics, ambiguous cross-role assignments
  fail closed, and completion, retry eligibility, Monitor/BFS execution, and
  symbolic verification share the same lowered status (issue #409).
• fslc lint now classifies business policy/goal satisfies CTRL-*
  operands as control references, recursively expands directory inputs into a
  sorted list of unique physical .fsl files even when operands repeat or alias
  one another, and continues to report nested FSL parse errors instead of silently
  skipping them (issues #385 and #386).
• fslc fmt now preserves canonical hyphenated IDs in business control,
  policy, goal, and satisfies positions while retaining normal spacing around
  arithmetic subtraction (issue #387).
• docs/LANGUAGE.ja.md now carries the Japanese translation of the
  "Literate Markdown FSL" subsection added to docs/LANGUAGE.md §7 by the
  literate Markdown feature, so docs/intro/language.ja.html documents the
  .md input support instead of silently omitting it (issue #346).
• Documentation for the depth-4 underspecification probe (divergent_choice,
  unconstrained_effect) now matches the native implementation: a solver-free
  explicit-state BFS over the runtime Monitor, not symbolic BMC/Z3.
  docs/DESIGN-underspecification.md, docs/DESIGN-analysis.md,
  docs/LANGUAGE.md/docs/LANGUAGE.ja.md, and skills/fsl/reference.md are
  corrected; the evidence_basis:"bounded_bmc" schema enum value is retained
  unchanged as frozen v0 vocabulary for "backed by a bounded reachability
  witness", so no output or schema contract moves (issue #318).
• Mutation documentation no longer overstates the score: kill_rate = killed / (killed + survived) is now defined everywhere as bounded
  mutant-set sensitivity — dependent on the operator mix, --max-mutants
  cap, --depth, and the verify/acceptance/forbidden/refinement oracle — not
  a production defect-detection rate, spec-correctness probability, or
  completeness measure. Survivors are documented as a review queue
  (equivalent mutants, dead-at-baseline behavior, beyond-depth effects, or
  genuine under-constraint) instead of "a place where an invariant is
  missing", and empty_formalization/per-requirement kills as observed lower
  bounds within the chosen mutant set and depth. Aligned across
  docs/LANGUAGE.md, docs/LANGUAGE.ja.md, docs/DESIGN-mutate.md,
  README.md, skills/fsl/reference.md, and the generated site reference; a
  new rust/fslc/tests/mutation_docs_contract.rs regression keeps the
  stronger survivor claim from returning (issue #338).

Changed

• The native installer no longer clones the repository into ~/.fsl. It now
  installs an exact-tag, checksummed CLI/LSP pair under the user data directory,
  atomically activates the complete payload, safely migrates recognized Python
  2.7 links, and rejects binaries whose reported version differs from the
  Release tag. Agent Skills are packaged as a checksummed Release asset; the
  v3.0.0 compatibility path verifies a pinned tag-archive checksum and extracts
  only the six installed skills.

Added

• Causal portfolio ledger (Phase 5, issue #364): fslc causal ledger model.fsl [--plans ... --evidence ... --lifecycle ... --as-of ...]
  integrates claims, validation plans, evidence, and observations into
  a per-claim projection with 12 deterministic attention reasons
  (validation_plan_missing, current_evidence_missing,
  observation_not_directional_support, etc.). New
  fsl-causal-validation-plan.v0 schema for immutable plan artifacts
  with claim pins, design, scope, observation window, measurements,
  and opaque external refs. Plan lifecycle reuses
  fsl-causal-evidence-lifecycle.v0. CLI envelope:
  causal-ledger.v0 (inventory 38). Every claim appears regardless of
  plan/evidence; retired claims have no attention; output is byte-stable.
• Causal observation bridge (Phase 4, issue #360): fslc causal observe-expectations model.fsl --from-log events.jsonl --mapping log_mapping.fsl --scope scope.json --period-start ... --period-end ...
  replays compiled expectations against a production JSONL log using the
  solver-free BoundedLivenessMonitor. Generates per-expectation
  fsl-causal-evidence.v0 artifacts with design: "observational",
  support: "inconclusive", assurance: "replay-observed", and matching
  lifecycle records. Pass/violated verdicts never change claim
  formal_assurance or causal_support. Nonconformant logs,
  missing scope/period, and mapping failures are fail-closed.
  CLI envelope schema: causal-observation.v0 (inventory 36).
• Causal expectation lowering (Phase 3, issue #323): explicit expectation
  declarations (trigger action or inline predicate, response predicate,
  within N clock <name>, derived_from_claim) compile — fail-closed on
  missing/foreign clocks, fractional tick conversion, unresolved references,
  or non-kernel targets — into ordinary leadsTo ... within ticks properties
  on the imported spec; action triggers become one-step pulse ghosts that
  never change guards. fslc causal verify-expectations model.fsl [--depth K] (causal-expectations.v0) reports pass/violated with
  assurance: "bounded"; pass and violated goldens both hold the central
  invariant that the derived claim's formal_assurance stays "not_run"
  and its causal_support is untouched — derived_from_claim is
  traceability only, and the legacy supports field is a parse error. A
  generated property is semantically identical to the hand-written pulse
  encoding (asserted by test), and there is deliberately still no
  causal verify alias.
• Causal evidence plane (Phase 2, issue #322): fslc causal analyze --evidence artifact.json [--lifecycle chain.json] [--as-of YYYY-MM-DD] validates
  fsl-causal-evidence.v0 artifacts (closed design/support vocabularies,
  claim ID + content-version pins, scope tokens, ISO-8601 periods, canonical
  sha256 artifact_digest) and independent append-only
  fsl-causal-evidence-lifecycle.v0 digest chains, fail-closed on
  schema/digest/chain violations. A new causal_evidence_graph projection
  (and the causal-review profile) overlays a deterministic per-claim
  causal_support — untested | supported | challenged | inconclusive | mixed | unsupported_by_current_evidence — counting only artifacts that pin
  the current claim version with subsumes scope, declared freshness, an
  active lifecycle, and an observation window at least the claim's minimum
  lag; one source lineage is one vote and staleness is judged only against an
  explicit --as-of date. Sixteen evidence/measurement review findings
  (evidence_scope_mismatch, evidence_window_shorter_than_lag,
  duplicate_evidence_source, unobserved_mediator,
  unsupported_assumption_chain, ...) join the causal-review profile, all
  formal_status: "not_a_violation". Evidence never changes a claim's
  formal_assurance: "not_run" — the two axes stay orthogonal by contract
  and by test. Ships three new schemas under schemas/fslc/causal/, a
  digest-stamped example artifact + lifecycle chain under
  examples/causal/evidence/, and docs/skills updates.
• fslc causal check|analyze|diff (Phase 1 of the review-only causal profile,
  docs/DESIGN-causal.md): a standalone causal <Name> { ... } document —
  parsed outside the dialect registry via a pre-dispatch sniff, so the frozen
  Python DIALECT_KEYWORDS parity gate does not move — is typed into a
  CausalModel (roles, measurement bindings resolved against imported
  kernel/business specs, closed scope vocabulary, claim content versions and
  the active|retired lifecycle, clock mappings, fail-closed well-formedness
  diagnostics including causal_instantaneous_loop and
  causal_unacknowledged_feedback). causal analyze emits deterministic
  causal_graph / causal_timeline / causal_traceability_graph
  projections (JSON/Mermaid/DOT; SCC-condensed, Dijkstra-exact earliest
  first-pass, upper-bounded latest through feedback, capped representative
  paths with truncation metadata) and a causal-review profile with 15
  structural/temporal findings, all formal_status: "not_a_violation" with
  do_not_assume. causal diff compares stable claim IDs and content
  versions, flags missing version bumps, retired-claim reactivation, and
  retired-hy...

v3.0.0

Changed

• Native v3 releases now assemble and validate all four CLI/LSP pairs, checksums,
  VSIX, and Kernel bundles before one tag-only publication step. Release actions,
  the Rust toolchain, and the VSIX packager are pinned; publication verifies a
  remote draft inventory before making it public, and manual dry runs validate
  the same assembled unit without publishing it. Native crates and release
  builds require Rust 1.88 or newer.
• The installer rejects unsupported Intel macOS, pins repository content and
  binaries to the same latest Release tag, and stages both checksummed native
  binaries before replacing either installed command. Linux artifacts now have
  an explicit Ubuntu 24.04 / glibc 2.39 baseline. All native targets build the
  vendored Z3 4.16 source so the distributed binaries do not require libz3 or
  z3.dll at runtime. macOS builds use the Clang 17 runner required by Z3 while
  retaining a macOS 14 deployment target, and CI timeouts accommodate clean Z3
  source builds on every supported runner.
• Release distribution checks now run in the authoritative native Rust gate;
  the redundant Python-only release workflow test was removed.
• Native fslc verify cache keys now use a build-time implementation fingerprint instead of
  hashing the full executable on every invocation, and CLI preparation reuses its validated
  KernelModel across property selection and engine dispatch. Cache schema v2 invalidates old
  entries fail-closed while removing the engine-independent fixed cost found in issue #349.

Added

• Documented a rationale convention for preserving a declaration's "why" in
  the checked model instead of only in // comments (lexer trivia): use the
  existing @kind(id, text?) to classify and explain a declaration in one
  line, and the recommended custom namespace @doc.rationale("...") for a
  short rationale that isn't a classification. No grammar, IR, or schema
  change; multi-sentence narrative keeps living in comments, and generic
  annotations are not currently projected through JSON, LSP, or the audit ledger. See
  docs/LANGUAGE.md §13.1.2 (mirrored in docs/LANGUAGE.ja.md),
  docs/DESIGN-annotations.md, and skills/fsl/reference.md.
• fslc lint now enforces a built-in, kind-aware canonical ID policy and accepts
  an explicit --project fsl-project.toml override. Requirement, acceptance,
  forbidden, policy, goal, control, model, and assumption IDs have distinct
  default templates; project tables can replace individual kinds while retaining
  all other defaults. Results record the resolved policy, invalid configuration
  fails closed, zero-padded numeric ID components retain their exact source
  spelling through parsing/lowering, and ID findings are deliberately non-machine-applicable so
  migrate never guesses cross-artifact renames. Typed @requirement annotations
  are the canonical declaration-link syntax; legacy "ID: text" metadata remains
  migration input.
• docs/intro/language.ja.html now renders from a new, section-aligned Japanese
  translation, docs/LANGUAGE.ja.md, instead of reusing the English docs/LANGUAGE.md
  body verbatim. FSL keywords, fslc commands/flags, diagnostic/result identifiers,
  JSON, and fenced code blocks stay untranslated and byte-identical to the English
  source; only headings and prose are Japanese. tools/build_site_reference.py fails
  loudly if the two files' ## section counts drift out of 1:1 alignment, and page
  anchors/SECTION_BLURBS lookups stay keyed off the English heading so cross-page
  links are unaffected. This supersedes the earlier "no translation" stance (see
  docs/DESIGN-docs-site.md D7); docs/LANGUAGE.ja.md now moves alongside
  docs/LANGUAGE.md under the "a language feature moves all of its files together"
  rule (AGENTS.md).
• Literate Markdown FSL: fslc check, fslc verify, and fslc scenarios now
  accept .md files containing ```fsl fenced code blocks directly. Lines
  outside fsl blocks are blanked in place so that diagnostic positions (line
  numbers, columns, counterexample locs) point to the original Markdown
  document. Multiple fsl blocks form one compilation unit; files without fsl
  fences are rejected with a clear diagnostic. Fence detection follows the
  CommonMark grammar (backtick or tilde runs of length >= 3, matched by
  character and length), so a non-fsl fence can safely contain a literal
  ```fsl example. The verify cache key is stable across repeated runs of
  the same document (issue #193).
• fslc-lsp is now a native Rust language server backed directly by the authoritative
  syntax, core, and analysis implementation. Existing diagnostics, navigation, symbols,
  rename, semantic tokens, completion, hover, and code actions no longer require Python;
  corpus/index coverage and stdio lifecycle tests run in the Rust workspace (issue #310).
• Required product CI now has one Rust-native integration entrypoint covering the workspace,
  dependency boundaries, CLI/schema contracts, native/browser agreement, and WASM. The redundant
  Python CLI parity job and its frozen-surface exception snapshot are removed; compatibility Python
  tests remain explicit manual evidence. FSL source locations, testgen templates, and generated
  artifact digests are portable across the supported native runner matrix (issue #307).
• fslc analyze --projection code_audit --code <path> now maps checked
  executable Kernel requirement targets to a closed, language-independent
  @fsl.trace annotation convention. Deterministic JSON reports complete,
  partial, missing, orphan, and target-mismatch coverage without presenting
  structural claims as proof; versioned input/output schemas and a compliant
  fixture define the public contract (issue #222).
• Replay-trace schema 1.2.0 opts into solver-free bounded leadsTo
  monitoring over initial, action, and stutter observations. Inclusive deadline
  failures carry property/binding/timing evidence; successful output separates
  safety from bounded liveness, preserves finite-prefix pending, and names
  unchecked unbounded properties. Native BMC and a test-only Python oracle
  cross-check the monitor, and positive/overdue NFR fixtures ship in both Public
  Kernel release bundles (issue #225).
• Replay-trace schema 1.1.0 adds explicit action: null observation points.
  Equal-state stutters preserve the projected action trace; reported transient
  implementation states are nonconformant while unreported intermediates are
  outside invariant judgment. Replay now delegates action outcomes, partial
  guards, and rollback to Monitor::attempt, with differential fixtures in both
  Public Kernel release bundles (issue #224).
• fslc replay --trace now consumes the closed replay-trace.v1 external
  compiler contract: trace/Kernel versions, exact spec action/parameters,
  canonical ticks, complete typed initial and post-action state, and optional
  opaque producer timestamps. Typed observation differences return leaf-level
  nonconformance while malformed/incomplete contracts fail closed. Positive and
  negative goldens plus the schema ship in both Public Kernel release bundles;
  legacy action-only arrays/{events} remain an explicit unversioned adapter
  (issue #221).
• fslc lint now reports edition-aware diagnostics with stable taxonomy,
  severity, spans, canonical replacements, and machine applicability. fslc migrate is dry-run by default and --write atomically applies only a fully
  parsed, checked, location-free Public-Kernel-equivalent file set. Shared
  formatter edits cover legacy enums/operators and quantifiers; typed metadata,
  unambiguous local action correspondences, and implicit defaults use semantic
  planners. Unsafe comment movement, branch/duplicate mappings, and invalid
  && are explicit refusals. The native LSP exposes applicable diagnostics
  as quick-fix Code Actions (issue #249).
• fslc fmt now formats one registered FSL document or stdin to canonical
  stdout without mutating it; --check accepts multiple paths and reports a
  machine-readable 0/1/2 result. A lossless token/trivia tree preserves line
  comments, blank lines, raw spelling, spans, and annotation attachment while
  domain enum/logical and quantifier legacy forms normalize to accepted
  equivalents. Corpus-wide idempotence and location-free semantic round trips
  cover every registered dialect; opaque agent bodies and ambiguous
  comment-bearing structural rewrites fail at exact spans (issue #248).
• fslc verify --engine auto composes the explicit-state and BMC engines:
  explicit runs first (faster, and can prove closure: true) and falls back
  transparently to BMC exactly when explicit cannot decide the spec on its
  own (an unsupported feature such as leadsTo or nondeterministic init, or
  unknown_budget). Every result carries engine: "explicit"/"bmc" naming
  whichever engine decided, and a fallback additionally carries
  engine_fallback: {from, reason, kind} so a caller can distinguish a
  bounded BMC verdict from an unbounded explicit one, and a permanent
  unsupported-feature gate from a transient budget one, without parsing
  prose. auto shares verdict-cache entries with plain --engine explicit/bmc runs of the same spec — the cache key is always the engine
  that actually decided, never auto itself — and does not change the
  default engine or extend to any other subcommand's --engine option
  (Rust-only, issue #226).
• Finite quantifiers, count, sum, unique, and exactlyOne now share one
  Binder/Aggregate IR across typed, range, Set, and Seq domains. Optional
  filters use one scope/type-check path; empty aggregates are zero and Seq
  duplicates preserve positional multiplicity. Legacy colon quantifiers remain
  detectable as non-canonical input, business/requirements KPI declarations
  survive as typed metadata projections, and collection aggregates normalize to
  exis...

v2.7.0

v2.7.0 — LSP hover, references, completion, and semantic tokens (#97)

v2.6.3

v2.6.3 — propagate bounds overrides into inline implements abstract (…