Numerical correctness before performance

A generated runtime is not correct merely because it loads the model, emits fluent text, or stays within a convenient tolerance. It must match a named reference at the correct semantic boundaries while running the provider, dtype, reduction schedule, phase, ISA, and thread plan it claims to run.

C-Kernel-Engine (CKE) turns model circuits and kernel maps into generated C for CPU inference and training research. That creates a difficult obligation: CKE must show that the generated program still computes the intended model. A runtime can call the correct mathematical operation and still execute the wrong numerical program. Two kernels may both be named “attention,” accept the same tensor shapes, and produce plausible output while disagreeing because one rounds K and V through FP16 and the other consumes raw FP32 values. A threaded route may split a reduction into worker-local ranges while a serial route processes one continuous range. The equations look equivalent on paper. Floating-point execution is not necessarily equivalent.

Numerical behavior is compiler input, not an implementation detail to recover after code generation.

This post documents a concrete CKE v8 hardening sequence across Qwen3-VL. The work began with explicit attention reductions, moved numerical semantics into versioned contracts, hardened production replay against llama.cpp, separated AVX2 from AVX-512 evidence, and then extended the same architecture to PyTorch-compatible BF16 providers. The result is not a claim that every CKE operator has a complete numerical specification. It is a record of how correctness moved from “the output looks close” toward a chain of attributable, executable evidence.

The architectural foundation is available in the C-Kernel-Engine repository through the commits explicit attention reductions, explicit numerical contracts, and authoritative kernel contracts. The live architecture reference is the v8 Numerical Contracts documentation.

A prompt running through a reference path and CKE path, followed by a difference report and first-divergence repair
End-to-end output tells us that two paths disagree. Numerical attribution asks where the first meaningful disagreement entered the computation.

Numerical Parity Is Not A BF16-Only Problem

BF16 is one of the parity lanes in this article, not the definition of numerical parity. Numerical parity means that two implementations agree under a declared comparison contract. That declaration must identify the reference backend, model artifact, prompt or tensor fixture, checkpoint boundary, dtype semantics, execution phase, provider, ISA, thread schedule, and tolerance. Without those fields, “matches the reference” is incomplete.

Parity laneReferenceWhat can differCKE evidence in this sequence
GGUF quantized inferencellama.cppQ4/Q6 weight unpacking, Q8 activation bytes, grouped quantization, dot-product order, repackingExact production Q4/Q6 and canonical Q8 boundaries
FP16 attention storagellama.cppK/V rounding, online-softmax updates, split-KV partials, denominator merge, compiler contractionZero-tolerance 34-row matrix at 1, 16, 20, and 24 threads
FP32 normalization arithmeticllama.cppsqrtf versus reciprocal approximations, vector width, reduction orderISA-independent RMSNorm graph oracle
BF16 safetensors executionPyTorchBF16 storage points, FP32 accumulators, output rounding, Welford/reduction order, prefill versus decode providerExact leaf contracts plus stitched X-Ray promotion gates
Model behaviorNamed backend and pinned artifactLogit ranking, token choice, persistent cache state, segmented multimodal prefillTeacher-forced and greedy token replay with provenance

The same word, “parity,” therefore covers several strengths of claim. Bit-exact equality at one leaf kernel is stronger than a small error at that leaf, but weaker than equality through a complete layer. A layer match is weaker than a full model replay. A full replay on AVX2 does not certify AVX-512. A five-image BF16 pass does not certify forty images. Every result needs an explicit boundary.

The Pull Requests Form A Debugging Ladder

These pull requests did not repeatedly fix one generic “precision bug.” Each one exposed a different place where plausible evidence could be misleading. Read together, they show why model-runtime parity takes weeks rather than one successful generation.

Pull requestFailure exposedWhat changedWhat it proved, and did not prove
PR #187 Production providers did not fully match llama.cpp arithmetic across vision, FP16 attention, normalization and quantized projections. Added explicit providers and contracts for FP16 attention, RMSNorm, Q/K normalization, SwiGLU, M-RoPE, Q4/Q6 and grouped Q8; routed prefill through those providers. Established an exact AVX2 production baseline. It did not certify native AVX-512 or eliminate the separate long-decode divergence.
PR #188 One split-KV FP32 ULP and thousands of grouped Q8 byte differences changed greedy tokens. Matched the fused denominator merge and routed grouped Q8 through the canonical byte-exact producer. Closed ten staged 128-token image prefixes and exact quantized boundaries. It did not claim the full forty-image corpus.
PR #189 The test harness forced arithmetic schedules that the one-worker production route could not select, creating false failures. Derived fixture schedules from runtime threads and added hash-locked private replay packets with strict schema and artifact provenance. Proved that the oracle harness itself must match production execution. Public CI validates the mechanism but skips private tensors when no manifest is configured.
PR #190 A hosted compiler differed by one FP32 ULP at the Q=63 short-prefill boundary. Made the intended fused multiply-add explicit with fmaf. Moved the maximum difference from 1.192093e-07 to zero without relaxing tolerance. It showed compiler contraction belongs to the contract.
PR #191 Forced AVX2 passed while native AVX-512 diverged because RMSNorm used a different reciprocal-square-root expression. Made llama-compatible RMSNorm arithmetic ISA-independent and added a real RMSNorm graph oracle with ISA provenance. Certified five native Xeon images and exact leaf matrices. It did not convert AVX2 evidence into a claim about every Xeon or every image.
PR #209 Building llama.cpp with -march=native enabled AVX512-FP16 and silently changed the oracle's attention accumulation path. Pinned oracle capabilities, preserved the declared LayerNorm reduction width, and rejected incompatible build provenance. Proved that the reference executable is part of the evidence. A faster or wider oracle is not automatically the same oracle.
PR #216 PyTorch-compatible BF16 normalization needed explicit storage boundaries, while AMX projection arithmetic was validated for prefill but not decode. Added exact BF16 normalization contracts and restricted AMX BF16 projections to prefill, retaining the generic BF16 decode path. Proved phase-safe provider selection and exact BF16 leaves. It did not claim complete Qwen3-VL BF16 corpus parity.
PR #223 An exact BF16 GEMM leaf provider made the stitched 27-layer vision encoder worse after layer 8. Added realistic-shape contracts, provider provenance and a monotonic X-Ray promotion gate. Correctly rejected the candidate. The leaf matrix passed 7/7, but the BF16 corpus baseline remained 18/40 and image 3 diverged at token 29.

What “One FP32 ULP At Q=63” Means

ULP means unit in the last place: the spacing between neighboring representable floating-point values at a particular magnitude. A one-ULP mismatch means two computations landed on adjacent FP32 values. It does not mean a universal decimal error; the spacing changes with exponent. In the PR #190 reproduction, the measured maximum difference was 1.192093e-07.

Q=63 means that the short-prefill attention case processed 63 query rows. Here Q is a shape dimension, not a quality score and not the complete query tensor. That boundary mattered because the selected tile and reduction path encountered a compiler-dependent multiply-add expression at that shape. Making fmaf explicit fixed the rounding graph without changing the provider, thread schedule or tolerance.

One ULP at one operation can be harmless, or it can be amplified. Q/K normalization, RoPE, softmax, projections, residual additions and later layers repeatedly transform the value. If two candidate output logits are close, accumulated drift can reverse their ranking and select a different token. That is why CKE traces the first divergence instead of judging importance only from the final decimal magnitude.

A rejected optimization is useful evidence: PR #223 demonstrates why exact leaf parity is necessary but insufficient. A provider is promotable only when the stitched model does not worsen at later checkpoints.

What BF16 Parity Specifically Requires

BF16 stores one sign bit, eight exponent bits and seven explicit fraction bits. It preserves roughly the dynamic range of FP32 but with much less mantissa precision. Many CPU kernels therefore load or store BF16 while converting values to FP32 for accumulation. That sentence still leaves critical questions unanswered: exactly where is a value rounded back to BF16, which reduction formula is used, in what order are values accumulated, and does the next operation consume the stored BF16 result or an unrounded FP32 temporary?

The Qwen3-VL BF16 path compares CKE against PyTorch safetensors execution. It is separate from the GGUF path compared against llama.cpp. The vision position interpolation, LayerNorm/RMSNorm, Q/K normalization, GEMM outputs, residuals, GELU, attention storage and projection boundaries can each introduce a rounding edge. AMX can accelerate a batched BF16 projection during prefill, but that does not authorize the same provider for one-row decode. Provider identity is phase-specific because shape and arithmetic can both change.

PyTorch BF16 reference
        |
        +-- checkpoint identity
        +-- tensor shape and layout
        +-- BF16 storage boundary
        +-- FP32 reduction formula and order
        +-- output rounding
        |
        v
CKE circuit requirement -> one compatible kernel provider
        |
        v
leaf parity -> layer checkpoints -> stitched encoder -> token replay

As of PR #223, CKE had exact BF16 leaf evidence, explicit prefill/decode ownership, and a monotonic stitched-comparison gate. It did not have complete Qwen3-VL BF16 model parity: the recorded corpus baseline was 18 passing images out of 40, with a known token divergence on image 3. This distinction is the point of the article. Numerical rigor means publishing the boundary of the evidence, not converting partial success into a model-wide claim.

How X-Ray Moves From A Wrong Token To A Wrong Operation

A final token mismatch does not identify a defective kernel. The token is downstream of image preprocessing, the vision encoder, projection into decoder space, segmented text/vision prefill, every decoder layer, the KV cache, final normalization, the language-model head, and sampling. Changing the last visibly different operation is therefore a poor debugging strategy.

CKE's X-Ray workflow narrows the failure while preserving semantic identity:

  1. Prove provenance first. Record the model and tokenizer hashes, CKE commit, reference commit, compiler, ISA, provider IDs, thread count, prompt, image grid, and execution mode.
  2. Reproduce the endpoint. Determine the first token or logit-ranking step where the two named paths disagree.
  3. Separate state from arithmetic. Compare persistent incremental decode with a full replay of the same prefix. If replay passes while persistent decode fails, inspect cache state and append semantics before leaf math.
  4. Compare sparse layer checkpoints. Capture a bounded set of semantically named outputs rather than dumping every temporary tensor.
  5. Bisect the failing interval. If layer 8 passes and layer 16 fails, request only layers 9 through 15.
  6. Expand the first failing block. Compare normalization, Q/K/V projections, RoPE or M-RoPE, attention, output projection, residual, activation and MLP boundaries.
  7. Replay the first divergent leaf. Feed the same input tensor and weights into the CKE production provider and the pinned backend oracle.
  8. Repair the owned contract. Fix the circuit requirement, numerical contract, kernel map or kernel. Do not add a model-name branch to the DSL.
  9. Promote the reproduction. Keep the leaf fixture, stitched checkpoint, token replay and provenance checks as regression gates.
wrong token
   |
   v
wrong persistent state or wrong replay arithmetic?
   |
   v
first failing layer interval
   |
   v
first failing operation boundary
   |
   v
production provider versus pinned oracle
   |
   v
contract repair + replay regression

X-Ray also needs permission to say “unknown.” PR #189 stopped assigning ownership to an ambiguous middle-Q checkpoint rather than inventing a comparison that looked useful. PR #223 stopped promotion when an exact leaf provider worsened later stitched checkpoints. These negative results protect the attribution chain.

The Failure Was Not A Loose Tolerance

The architecture changed because a real attention route exposed a mismatch. Three full-attention tests had persistent errors of approximately 5.68e-4 to 1.06e-3. It would have been easy to call that harmless floating-point noise and increase the tolerance. That would have hidden the actual problem.

The reference behavior for the relevant Qwen3-VL vision path used FP32 queries while K and V were rounded through FP16 before attention. The optimized AVX2 implementation consumed raw FP32 K and V. Both routes performed full bidirectional attention. Both had compatible shapes. Both could produce reasonable values. They did not implement the same numerical contract.

Pre-rounding only K and V through FP16 reduced the error to roughly 4.77e-7. That result localized the problem more convincingly than a generic end-to-end failure ever could. The leaf arithmetic was not merely “a little inaccurate.” The public route selected semantics different from the reference route.

BoundaryRequired behaviorFormer routeEvidence
Full-attention QFP32 computeFP32 computeQwen3-VL head dimension 72 test
Full-attention K/VRound through FP16Consume raw FP32Error fell to approximately 4.77e-7 after correct rounding
Decode KV below 512One FP16 online rangeImplicit route selectionKV=511 oracle
Decode KV at or above 512Worker chunks, FP16 partials, FP32 ordered mergeA different reduction route could be reached implicitlyKV=512 and KV=1058 oracle coverage

Wrong response: increase the tolerance until the test passes.

Correct response: identify the first semantic mismatch, define it explicitly, bind the public route to that definition, and preserve the selected provider through lowering.

Same Shapes, Different Computation

Tensor shape is necessary information, but it is not a complete executable specification. Consider an attention kernel receiving Q, K, and V with identical dimensions in two implementations. Shape validation can prove that memory extents and matrix dimensions are compatible. It cannot answer these questions:

  • Was Q computed as FP32, BF16, FP16, or FP16-rounded FP32?
  • Were K and V stored in FP16 but accumulated in FP32?
  • Was each online-softmax update rounded before the next update?
  • Were maximum and sum statistics accumulated in FP32?
  • Was the KV range processed continuously or divided across workers?
  • Were worker partials stored in FP16, BF16, or FP32?
  • Were partials merged in worker order, tree order, or an implementation-defined order?

Those decisions can change the output while leaving every public tensor shape unchanged. This is why CKE now treats an attention reduction ID as a complete semantic identity rather than a vague label such as fp16, fast, or strict. Those short labels are explicitly rejected because they do not say enough.

Floating-Point Reductions Have History

Real-number addition is associative. Floating-point addition is not. If values vary in magnitude, the order in which partial sums are accumulated changes rounding. The simplified relationship is:

$$\operatorname{fl}(\operatorname{fl}(a+b)+c) \neq \operatorname{fl}(a+\operatorname{fl}(b+c))$$

Attention contains several reductions. Query-key scores are accumulated across the head dimension. Softmax tracks a maximum and a normalization sum. Value mixing accumulates weighted V vectors. An online-softmax implementation updates statistics as tokens arrive. A partitioned implementation computes worker-local partial states and merges them. These are not automatically interchangeable execution strategies.

Threading therefore becomes part of the mathematical contract whenever it changes partition or merge order. If every thread owns independent output rows and never contributes to a shared reduction, the numerical effect may be none. If workers split K, sequence positions, experts, or attention ranges and later merge partials, the execution plan changes arithmetic order. That order must be declared or the runtime cannot honestly claim deterministic parity with a specific reference.

Why The 511/512 Boundary Matters

Thresholds are common in optimized runtimes. A small sequence may run serially because thread dispatch costs more than the available parallel work. A larger sequence may be divided into worker chunks. The performance rationale is sensible, but the boundary can also change numerical behavior.

In the v8 attention contract, a decode route below 512 KV positions can use one online FP16 range. At 512 and above, workers can process KV chunks, store FP16 partials, and merge those partials in FP32 chunk order. If that threshold exists only inside a C wrapper, then the public model silently changes reduction structure when context length crosses 512. If the threshold is in the numerical contract, the behavior is visible, testable, and available to compiler resolution.

{
  "id": "f16_online_fp32_merge",
  "q_compute": "fp16_rounded",
  "k_compute": "fp16",
  "score_accumulator": "fp32",
  "softmax_statistics": "fp32",
  "value_accumulator": "fp16_rounded_each_update",
  "partial_storage": "fp16",
  "partial_merge": "fp32_chunk_order",
  "partition": {
    "kind": "kv_chunks_by_workers",
    "threshold": 512
  }
}

This JSON is not merely documentation beside the implementation. It is a registered semantic object used during resolution. A kernel map must advertise support for the complete reduction identity. A circuit must request that identity for a defined operation and phase.

Four Inputs Define The Executable Route

InputWhat it ownsWhat it must not decide
Weight manifestTensor names, shapes, physical dtypes, quantization formats, offsets, and dimensionsGraph order or numerical reduction policy
CircuitOperations, edges, branches, stitch points, phases, and required semantic capabilitiesA specific C function chosen only because it happens to work today
Contract registryComplete versioned meaning of a numerical identityModel-specific dispatch
Kernel mapABI, implementation function, layouts, provided capabilities, threading, and supported numerical contractsSilently reinterpret a circuit requirement

This separation is important. A circuit is the model-family topology and semantic request. It should not need to name attention_forward_decode_head_major_gqa_flash_f16cache forever. It should state what the operation requires. Kernel maps are executable providers. They state what concrete implementation exists and which complete contract it can satisfy.

The registry prevents two providers from using the same convenient label for different mathematics. The weight manifest prevents the compiler from pretending storage layout and quantization do not matter. The resolver joins these inputs without using a model-name conditional.

Resolution Must Happen Before GraphIR

The first numerical-contract integration validated that legacy lowering had emitted the selected kernel. That preserved behavior during migration, but it still left room for a later stage to be the practical selector. The authoritative follow-up moved selection before GraphIR construction.

  1. Load and schema-validate the circuit requirements.
  2. Load and validate the canonical reduction registry.
  3. Load versioned executable kernel maps.
  4. Match operation, phase, Q dtype, KV dtype, layout, and complete reduction identity.
  5. Fail if no provider matches.
  6. Fail if more than one provider matches.
  7. Record the one resolved provider in GraphIR.
  8. Carry that identity into LoweredIR and call-ready IR.
  9. Hard-fail if a later stage changes the kernel identity.

Zero matches means the requested model semantics are unsupported. Multiple matches means the capability model is ambiguous. Picking the first JSON file, the first registry entry, or a model-specific preferred implementation would make the compiler nondeterministic or policy-driven in the wrong layer.

circuit requirement
        +
contract definition
        +
kernel capabilities
        |
        v
exactly one provider
        |
        v
GraphIR -> LoweredIR -> call-ready IR -> generated C
             no reselection allowed

GraphIR Now Carries The Decision

A contract-bearing operation records both sides of the decision. required_contract preserves what the circuit requested. resolved_contract records the selected provider and reduction identity. Versioned kernel maps also contribute resolved_execution, which records implementation characteristics such as ISA dispatch and threading policy.

Lowering may add memory offsets, pointer expressions, buffer assignments, and call arguments. It may not reinterpret the selected kernel. If LoweredIR receives a kernel ID different from the GraphIR contract identity, the build raises a hard contract fault. Call-ready IR performs the same identity check. This creates a visible chain from semantic request to executable call.

The distinction between numerical and execution metadata should remain clear. Attention currently has the deepest versioned numerical contracts. Generic execution capabilities cover ISA dispatch, threading runtime, work partition, dispatch mechanism, and reduction-order effect for a growing set of kernels. That metadata is valuable, but it does not yet mean every GEMM, normalization, RoPE, SwiGLU, vision, and backward operation has an equally complete numerical registry. The migration should proceed one operator family at a time.

Bring-Up And Production Are Different States

New architecture support needs room to exist before every route is fully validated. CKE therefore distinguishes bring-up resolution from production resolution. A bring-up route can expose blockers. A production route must satisfy all required validation states.

Production gateQuestion
Circuit request validatedIs this the intended model-family behavior for this phase?
Contract definition validatedIs the complete numerical meaning recorded and tested?
Kernel implementation validatedDoes the concrete function implement that meaning?
Explicit selectorCan the implementation route be selected without hidden legacy behavior?
Public-route parityDoes generated execution reach the tested leaf?
Stitched and E2E evidenceDoes the complete model retain expected behavior?

This prevents “the unit test passed” from becoming “the model path is validated.” A correct leaf kernel can be hidden behind the wrong wrapper. A correct function can receive data in the wrong precision. A correct reduction can be bypassed by an older dispatch branch. Validation must cover the public generated route.

The Hard-Fail Policy Is An Agent Policy

AI agents can produce large patches quickly. That speed makes architectural boundaries more important, not less important. When an agent encounters an unsupported contract, the tempting fixes are precisely the dangerous ones: add a fallback, insert a default kernel, loosen a tolerance, restore a model-specific conditional, or hide the problem behind an environment variable.

v8 now records a contract policy that forbids those responses. A contract failure should be repaired in one of three places: the circuit semantics, the canonical contract, or the executable kernel map. The repair must then add leaf, public-route, stitched, and end-to-end evidence appropriate to the change.

Forbidden: fallback providers, silent defaults, ignored schema fields, relaxed tolerances, warning-only contract failures, bypass flags, and model-specific attention selection in code generation.

This is not bureaucratic purity. It is how the repository prevents the same semantic decision from leaking into several Python scripts, generated wrappers, runtime flags, and C kernels. The compiler should have one visible explanation for why a provider was selected.

What The Committed Tests Actually Prove

The contract test suite checks more than the happy path. It verifies complete registry semantics, kernel-map agreement, function-drift rejection, separate prefill and decode resolution, production rejection of unvalidated routes, rejection of ambiguous short IDs, deterministic failure for unsupported or multiple providers, rejection of unknown schema fields, and resolution of supported v8 circuits without legacy attention selection.

The authoritative propagation tests verify that selected Qwen3-VL contracts reach call-ready IR while preserving executable behavior. Additional scaffold and code-generation tests guard circuit isolation, runtime-policy extraction, local kernel-registry use, bridge generation, generated C, provider provenance and phase ownership. Counts evolve as the contract surface grows, so the useful evidence is attached to each change rather than presented as one permanent project-wide number:

Evidence laneRecorded resultBoundary
FP16 attention production matrix34/34 exact at each of 1, 16, 20, and 24 threadsllama.cpp-compatible attention leaves and reduction schedules
Private replay mechanism10/10 manifest and adapter testsSchema, hashes, providers, commands, shapes and stale-environment rejection
Native AVX-512 Qwen3-VL sample5/5 images with 128/128 exact pre-EOS tokensPR #191 supplied Xeon evidence, not a forty-image certification
BF16 GEMM storage oracle7/7 exactLeaf output storage, not stitched model correctness
BF16 provider contract suites43/43 focused contract testsResolution, realistic shapes, provenance and phase ownership
BF16 stitched corpus baseline18/40Incomplete model-level certification; candidate promotion rejected
make test-numerical-contracts

PYTHONPATH=unittest .venv/bin/python -m unittest -v \
  tests.test_build_ir_v8_scaffold \
  tests.test_v8_qwen3vl_template \
  tests.test_v8_codegen_bridge

PYTHONPATH=unittest .venv/bin/python unittest/test_attention_full.py -v
make test-v8-qwen3vl
make v8-regression-fast

Passing tests do not prove that every sequence length, ISA, thread count, model, dtype or numerical edge case has been exhausted. They prove only their declared boundaries. The incomplete BF16 corpus is therefore not in conflict with exact BF16 leaf tests: it demonstrates that additional divergent boundaries remain in the stitched path.

How To Extend The Contract System

The migration policy should remain deliberately incremental. For each new operator family:

  1. Record the behavior of the current public route.
  2. Identify which precision, layout, partition, and merge choices affect semantics.
  3. Add a canonical versioned contract schema.
  4. Add a scalar or trusted reference and leaf tests.
  5. Add public-wrapper and generated-route tests.
  6. Declare circuit requirements without naming an implementation.
  7. Enrich real kernel maps with capabilities and evidence states.
  8. Resolve before GraphIR and preserve identity through lowering.
  9. Prove artifact equivalence when the migration is intended to preserve behavior.
  10. Run stitched parity and model-family E2E gates before production promotion.

Likely future families include normalization reduction order, quantized GEMM/GEMV accumulation and activation contracts, SwiGLU intermediate precision, RoPE and MRoPE coordinate semantics, vision preprocessing and projection boundaries, recurrent-state updates, optimizer reductions, and backward gradient accumulation. Not every operation needs an enormous contract. The contract should encode only the choices that distinguish valid executable meanings.

Performance Planning Comes After Semantic Resolution

Once several kernels satisfy the same complete contract, a performance planner can rank them using ISA availability, tensor dimensions, cache behavior, thread count, and measured profiles. The order matters. Performance ranking should choose among semantically valid providers; it should not decide what mathematics the model meant.

This separation is especially important for CKE because the project targets many CPU classes. AVX2, AVX-VNNI, AVX-512, AMX, NEON, SME, scalar fallbacks, different thread pools, and different memory systems may all need distinct implementations. The compiler needs freedom to select a physical kernel without allowing that choice to silently alter the model contract.

The Larger Architectural Lesson

Model architecture is often described as a graph of named operations: attention, normalization, MLP, residual connection. Runtime architecture adds physical detail: dtypes, layouts, buffers, strides, vector instructions, thread partitions, and cache policy. Numerical contracts connect those views. They state which physical differences remain implementation choices and which differences change the model being executed.

The Qwen3-VL bug was useful because it made the missing boundary measurable. The same shapes reached two attention implementations. The output drift looked small enough to dismiss. A targeted precision experiment reduced that drift by orders of magnitude and showed that the route was semantically wrong. CKE then moved the missing information out of implicit dispatch and into compiler-visible contracts.

That is the standard CKE should continue to follow: do not claim correctness because C code compiles, a kernel unit test passes, or generated text looks plausible. State the intended semantics, resolve an executable provider, carry that decision through the IR, compare against a named reference, and fail loudly when the system cannot prove what it is running.

Related Reading