KERN v2.4.0 — Hardcore Audit & C-ABI Hardening

KERN v2.4.0 completes the industrial hardcore audit: five destructive
checks aimed at the failure modes that normal tests never reach, plus the
human-facing features that make the tool usable without writing SMT-LIB by hand.

Security & robustness (found REAL defects)

• Deep Nesting Bomb (#98). parseList recursed without a depth limit. Measured:
  '(' * 50 000 survived, '(' * 2 000 000 → terminated with signal SEGV.
  Solver output is untrusted input, so this was a denial of service from a single
  .smt2 file. Fixed with ParseError.TooDeep + MAX_SEXP_DEPTH = 4096.
• NULL pointers in the C-ABI (#99). C callers can pass NULL where Zig's
  [*]const u8 cannot represent it; img[0] on NULL crashed the caller's
  process. Fixed with isNull() (@intFromPtr) in all 8 exported functions.
  Verified by tests/c_abi_test.c built with
  zig cc -Wall -Wextra -Werror -pedantic -std=c11 — 20/20.
• Header type mismatch (#100). Strict flags rejected passing
  unsigned char[64] to kern_localize, which was declared char *out_buf
  while every other function used unsigned char *. Header aligned.
• Memory leak under partial OOM (#101). try out.append(try allocator.dupe(...))
  in extractAsserts leaked the duplicate when append failed. Found by
  std.testing.checkAllAllocationFailures (fails at every allocation).
  Fixed with errdefer.

Concurrency

• 8-thread stress through the real shared library. In test builds Zig's
  builtin.is_test short-circuits compat.io() to std.testing.io, so the
  threadlocal var tls_io cache is never exercised by zig build test.
  A C test (tests/c_abi_threads.c) now drives it through libkern.so:
  8 threads × 500 kern_hash → 0 divergences; 8 threads × 20
  kern_smt_verify → 0 errors, 160/160 proved. The reference digest is a
  constant (cross-checked against an independent BLAKE3), otherwise a
  mutation inside the hash path would change both sides of the comparison.

Tooling honesty

• Mutator covered only the old core (#102). TARGETS was a hard-coded list
  of 6 files, so every module added in v2.2–v2.4 was never mutated and the
  previously reported score said nothing about them. Now 14 files / 427 sites
  (was 6 / 63).
• C-ABI was outside mutation coverage (#103). zig build test never runs the
  C tests, so mutations in src/capi.zig survived. The mutator now rebuilds
  libkern.so from mutated sources and runs both C tests.
• Attestation fixes (#87, #92). The SLSA attestation no longer hashes its own
  evidence logs (circular), and it now attests the reproducible release artifact
  kernc-hermetic instead of Debug binaries that any zig build overwrites.

Human-facing features

• # @kern:ensures now accepts if/elif/else and local assignments (translated
  to SMT ite); out-of-subset code is reported as SKIP with a reason.
• Z3 counterexamples are printed in the CLI: [КОНТРПРИМЕР] balance = 0, amount = -1, result = 1.
• kernc build --deflate — object compression (measured 3.16× smaller image).
• examples/kern_mcp_server.py — MCP server with 4 tools for Claude Code / Cursor.

Verification baseline

Check	Result
Core tests (Debug + ReleaseSafe)	251 / 251
KERN-Next (kernx)	37 / 37
Lean 4 proofs	7 files, 0 errors, 0 sorry
canfail non-vacuous checks	72 / 72 CHECK targets with a proven-can-fail case (85 cases)
Mutation score (Zig-native mutator)	77.5 % (31 / 40 killed) over 14 files / 427 sites (was 6 / 63 before this release)
Defect registry	#1–#103, numbers unique
Evidence gate	all logs RC=0
SLSA attestation	VALID (unsigned — no cosign; recorded in kern:notes)