Vosti: Specifying, Implementing, and Verifying Deterministic LLM Inference

1 Introduction

• For a fixed model, deployment configuration, prompt, and sampler state, deterministic inference requires bitwise-identical logits at every output position across executions.The specification constrains observable outputs without assuming batching, prompt chunking, or a KV-cache.Source: §1 · p. 1
• Production deterministic modes address batch-dependent kernels, but tested vLLM and SGLang modes still produce logit mismatches under execution variations.The paper notes that batch invariance alone does not establish determinism across chunking, prefill/decode transitions, or cache reuse.Source: §1 · p. 1
• A Verus proof maintains KV-cache and engine invariants so each engine step’s logits depend only on request token history, with induction establishing request determinism.Reusable KV entries must equal values obtained by recomputing their token prefixes.Source: §1 · pp. 1–2
• Vosti preserves continuous batching, chunked prefill, and KV-cache reuse while using fixed, runtime-independent kernel configurations.It rejects a missing configuration rather than autotuning; dispatch among bitwise-equivalent kernels is left for future work.Source: §1 · pp. 1–2
• Vosti achieves 1.36–3.19× the decode throughput of vLLM’s batch-invariant modes and completes synthetic agentic workload sessions 1.14–2.20× faster, while slower than default modes and SGLang’s deterministic modes.The evaluation reports these results on an H200 GPU.Source: §1 · p. 2

2.1 Why Deterministic Inference?

• Execution variation can change batching, prompt partitioning, speculative positions, or cached-prefix handling, although these choices should affect performance rather than model results.Continuous batching changes request companions; chunked prefill partitions prompts by token budget.Source: §2.1 · p. 2
• Determinism must hold across the whole system because kernels can change floating-point results while the scheduler and cache determine the inputs supplied to them.Different logits can affect speculative verification, reinforcement-learning log-probabilities, KV-state reuse, and reproducibility under changing load or cache history.Source: §2.1 · p. 2

2.2 Measuring Production Deterministic Modes

• Tests compare production modes across batching, chunked prefill, prefill–decode, and prefix reuse, using matching token histories or cache-hit checks where applicable.The evaluation includes vLLM and SGLang default and deterministic modes, with FA3 and Triton backends, on Llama3.1-8B and Gemma3-4B.Source: §2.2 · p. 2
• Production deterministic modes still show mismatches: SGLang Triton misses some Llama3.1-8B prefill–decode and prefix-reuse comparisons, and Gemma3-4B modes mismatch in every tested category.The modes usually reduce mismatches relative to defaults, but agreement varies by model, backend, and execution variation.Source: §2.2 · pp. 2–3

2.3 A System-Level Formulation

• Deterministic inference requires equal prompts and initial sampler states under the same configuration to produce output views that agree on their common prefix, including logit bit patterns.The shorter view must match the beginning of the longer one; equality of logit components is equality of bit patterns.Source: §2.3 · p. 3
• The definition constrains outputs when corresponding records are produced, but does not require scheduling progress or guarantee that outputs match intended model semantics.It is neither a liveness nor a functional-correctness specification.Source: §2.3 · p. 3

3 Overview

• Vosti pins kernels and launch configurations to the fixed model and environment, so runtime variation changes neither a position’s logical inputs nor its floating-point operation sequence.The runtime may vary token batching, state storage, and state access; dispatch among bitwise-equivalent alternatives is not proved.Source: §3 · p. 3
• Verus proves that engine steps preserve request and cache invariants and that emitted logits depend on request token history, assuming each GPU operation returns its contracted result.The proof reasons about request states, page tables, and cache sharing without modeling Triton or floating-point arithmetic.Source: §3 · p. 3
• The two proof layers meet at a shared kernel contract: Verus assumes its postconditions, while the kernel verifier proves them.Contract translation and tensor-representation correspondence remain trusted, and Verus does not recheck the kernel proofs.Source: Figure 1 · p. 4, §3 · p. 4
• The kernel verifier proves that batched or singleton invocations return the same selected output for the same logical input, despite layout, query-length, prefill–decode, or page-table differences.Configuration checks bind proved launch parameters to runtime invocations; the trusted Triton compiler produces the invoked GPU kernel.Source: §3 · p. 4

4 Engine Implementation and Verification

• Each engine step’s emitted logits equal a cold forward determined by the request’s pre-step history; equal initial sampler states then yield prefix-comparable output traces.Steps without an output do not advance a request’s per-request output sequence.Source: §4 · pp. 4–5

4.1 Engine Implementation

• Kernel choices depend on the fixed model and deployment configuration, while exact prefix matching and private suffix writes constrain cache reuse.The cache verifies candidate pages against exact tokens, depth, and physical parent; pages produced during a step become reusable only later.Source: §4.1 · p. 5

4.2 Engine Invariants

• The KV-cache invariant ties every initialized live or retained entry to the canonical value from a cold forward on its causal prefix.Retained prefix obligations can survive request completion, while uninitialized slots are not readable and carry no KV-value obligation.Source: §4.2 · pp. 5–6

4.3 Invariant Preservation

• Induction preserves the invariant through admission, planning, forward execution, and state updates, so scheduled outputs match cold-forward logits.The proof connects logical prefix values to physical cache slots; write isolation and leaf-only eviction preserve obligations for other requests and retained pages.Source: §4.3 · pp. 6–7

5 Kernel Implementation and Verification

• Contracts require corresponding computations to use equal logical inputs and matching value-relevant operations in the same order, since equal inputs alone do not ensure bitwise equality.They compare selected tensor regions; other inputs need not agree.Source: §5 · p. 7, §5.1 · p. 7

5.1 Relational Kernel Contracts

• A relational contract compares a selected packed-token row with its singleton run, while the engine proof imports kernel contracts as trusted assumptions.Contract translation and tensor-representation correspondence also remain trusted.Source: §5.1 · p. 7

5.2 Relational Structural Analysis

• Structural analysis aligns relevant operations and traces selected outputs backward to required input regions; Z3 checks dependencies, masks, and store coverage.The verifier translates supported Triton constructs into tile IR and rejects unsupported constructs or unresolved shapes.Source: §5.2 · pp. 7–8

5.3 Value-Aware Regional Analysis

• Value analysis identifies masked attention regions and proves extra all-false-mask iterations preserve state, allowing differing query indices and physical pages to yield equal outputs.The contract requires equal selected queries and logical KV values through the selected position, while future KV positions are causally masked.Source: §5.3 · p. 8, Figure 4 · p. 8
• Attention assumes input-dependent finiteness without runtime checks, and full numerical correctness against a reference semantics is outside scope.The translator, solver encoding, engine/kernel interface, and compiler/GPU execution also remain trusted.Source: §5.3 · pp. 8–9

6.1 Determinism and Numerical Variation

• 5,488 bitwise comparisons across seven Llama and Gemma models passed for Vosti.The tests cover batching, chunked prefill, prefill–decode equivalence, and prefix reuse.Source: §6.1 · p. 9
• Batch-wide K-length bounds and KV page-table metadata affect specialization, accounting for selected Gemma3-4B batch and prefill–decode differences.The page-table effect occurs even when valid keys are unchanged.Source: §6.1 · p. 9
• Numerical variation also arises within attention implementations: SGLang uses different prefill and decode algorithms, while vLLM’s invariant path varies with query partitioning and masked softmax tiles.In vLLM, processing a fully masked tile can replace a running maximum of −∞ with zero, affecting subsequent rounding.Source: §6.1 · p. 9
• The tested explanations cover some Table 1 mismatches; observed numerical differences need not indicate engine bugs.These conclusions concern tested execution variations.Source: §6.1 · p. 9

6.2 Performance

• 1.36–3.19× the decode throughput of vLLM’s invariant configurations was achieved by Vosti, while its prefill throughput remained lower than both engines.The comparison varied cached context length on one H200 GPU with batch size 4.Source: §6.2 · p. 9
• 1.14–2.20× faster session completion than vLLM’s invariant modes was measured for Vosti in a synthetic decode-heavy workload.Vosti remained slower than default modes and SGLang’s deterministic modes; decode accounts for 91–93% of its session time.Source: §6.2 · p. 10

6.3 Implementation and Verification Effort

• Table 2 reports implementation and verification effort, including 168 LoC for the abstract specification and 708 LoC for runtime contracts.The table also reports wall-clock verification time, with kernel times given per configuration.Source: §6.3 · p. 10, Table 2 · p. 10

• Determinism does not establish functional correctness, and Vosti does not establish bitwise agreement across numerical dtypes, kernel configurations, compiler versions, or hardware platforms.The guarantee fixes the model and value-relevant deployment configuration.Source: §7 · pp. 10–11
• Verifying bitwise equivalence across distinct kernels could enable workload-dependent dispatch, whereas Vosti fixes kernel and launch choices.DeepSeek-V4’s two decoding-attention kernels preserve the same accumulation order for bitwise identity [11].Source: §7 · p. 11
• Linear-attention and MoE support would require extending cache or routing invariants and establishing further bitwise and relational contracts.MoE extensions would address batch-independent routing, token identity through regrouping, and expert computation and output accumulation.Source: §7 · p. 11
• Vosti currently supports single-GPU execution; multi-GPU determinism would require preserving value-relevant accumulation order and tracking request and token provenance across devices.Agreement across GPU counts or partitionings requires additional constraints [35].Source: §7 · p. 11

• Vosti combines engine invariants with relational kernel contracts for per-request determinism across batching, chunking, prefill–decode transitions, and cache reuse.The claim is under Vosti’s stated assumptions.Source: §8 · p. 11
• LLM-42 uses fixed-shape verification and rollback, while MarginGate selectively verifies low-margin steps and repairs the current KV column [7] [15].Vosti verifies the implementation ahead of execution, avoiding per-request replay.Source: §8 · p. 11
• Bitwise-reproducible reductions independent of data partitioning or summation order have been developed in HPC; Vosti instead preserves logical inputs and value-relevant operation sequences for a fixed deployment.Source: §8 · p. 11
• Prior KV-cache security work describes attacker-controlled context reuse [34] and prompt reconstruction through serving-order side channels; Vosti’s guarantee does not cover timing or serving-order confidentiality.Source: §8 · p. 11
• GPU verification work includes race-freedom and barrier-safety proofs, PTX checks using real-number arithmetic [13], and functional kernel verification [5]; Vosti relates invocations of the same Triton kernel.Its tile-level analysis aligns selected computations and establishes equal dependencies.Source: §8 · p. 11

• Engine invariants and relational Triton kernel contracts establish per-request bitwise determinism under the stated assumptions and trusted computing base.The engine preserves logical inputs across scheduling and KV-cache reuse, while the kernel verifier aligns value-relevant operations and dependencies.Source: §9 · p. 11
• 1.14–2.20× faster session completion than vLLM’s batch-invariant modes was measured on the evaluated decode-heavy workload; Vosti remained slower than default configurations and SGLang’s deterministic modes.Vosti also passed all 5,488 bitwise comparisons across seven Llama and Gemma models.Source: §9 · p. 12

• §5.3 is expanded with a mathematical presentation of the attention tile IR.Source: A Verifying Paged Attention · p. 13

• The setup fixes element types, head geometry, scale, page and tile sizes, and describes query rows by their logical token positions.Source: §A.1 · p. 13
• Logical key and value caches use a page table, while the engine supplies valid lengths and layouts and physical addresses may differ.Source: §A.1 · p. 13
• Batch invariance requires a packed request and its singleton run to have equal queries and logical cache.Source: §A.1 · p. 13
• A second property requires equal output rows at the same logical token position across singleton runs with different query or key lengths and row indices.Source: §A.1 · p. 13
• Together, the properties relate packed prefill to decode, under assumptions whose concrete annotations conservatively require equality of whole pages intersecting the prefix.Source: §A.1 · p. 13

A.2 A Simplified Tile IR

• The tile IR uses an online-softmax state initialized to (−∞, 0, 0), with fixed floating-point types, parameters, and value-relevant operation order.Weights are cast to the cache element type for the second dot, while the normalization sum uses uncast weights; the auxiliary log-sum-exp output is omitted.Source: §A.2 · pp. 13–14

A.3 Forward Value Analysis

• Forward value analysis tracks known constants and unchanged incoming state; a false mask arm gives zero weights, and a false selection preserves incoming state bitwise, even with exceptional candidate intermediates.Source: §A.3 · p. 14

A.4 Backward Regional Dependencies

• Backward analysis restricts query-key and value dependencies to visible lanes, assuming finite loaded values and a trusted masked-dot rule; finiteness is not checked at runtime.The verifier checks the query-key product and state update separately, and Z3 checks region and scalar obligations before equal inputs yield equal selected next state.Source: §A.4 · p. 14

A.5 Relational Alignment and Composition

• The verifier aligns full-attention runs at a shared token position: common tiles and masks match, while extra all-false iterations preserve selected state and outputs.Sliding-window alignment uses the tiles intersecting the shared window, but retains full-prefix equality and supplies no cache-eviction guarantee.Source: §A.5 · p. 14
• The proof’s bitwise-value and iteration-composition steps rely on trusted verifier and operation rules plus compiler/GPU assumptions; input-dependent finiteness remains an explicit premise.Tests support those assumptions on the evaluated configurations.Source: §A.5 · p. 14