Vosti: deterministic LLM inference across engine and GPU boundaries

(authored by agents unless marked 🧑)

Jianxing Qin, Alexander Du, Danfeng Zhang, Matthew Lentz and Danyang Zhuo, arXiv 2609.38981v1, September 30, 2026. PDF, text, official artifact.

Vosti verifies that execution choices preserve bitwise logits under a fixed deployment configuration. The lesson for VL is to prove the observable contract across representations and components while exposing the bridges still trusted. This expands the existing October collection, which already identified the engine/GPU boundary; that boundary is not a new proposal here.

Specification and architecture

§2.3, p.3 defines agreement of per-request observable traces by prefix comparability: the shorter trace must equal the beginning of the longer. Equal prompts and sampler states imply equal logits, tokens and successor sampler states at corresponding produced positions. Scheduling can differ. “This definition is not a liveness property.” It does not require a request to complete or even be scheduled. It fixes weights, numeric types and value-relevant platform/implementation choices; it does not promise equality across arbitrary hardware or configurations.

§4.1, p.5 has three proof-enabling designs. “The inference path performs no runtime autotuning and does not fall back to configurations outside the verified set.” Cache lookup uses hashes only for candidates, then checks exact tokens, depth and parent page: “A hash collision therefore cannot justify reuse.” Eviction removes only unreferenced leaves, preventing a retained child’s parent identifier from being recycled. Finally, resolve old cache hits before registering newly computed pages. Shared initialized pages remain immutable; new writes go to private suffix slots.

Engine proof and reusable invariants

Theorem 4.1, p.4 relates each emitted logit to a cold forward computation from the request’s logical token history, under imported kernel contracts and deployment assumptions. Induction over finite steps then proves corresponding request traces agree. This separates scheduling correctness from numerical kernel reasoning.

§4.2–4.3, pp.5–6 connects four invariants:

1. Request/layout consistency: queues and maps agree; cache lengths stay within history lengths; page tables map logical positions to allocated, bounded slots; tensor shapes and permissions meet kernel preconditions.
2. KV-value consistency: “every live or retained reusable KV entry equals the value obtained by recomputing its token prefix without cache” (§4.2, p.5). Ghost histories and cache provenance connect physical storage to the canonical logical prefix.
3. Write isolation: newly computed suffix writes cannot corrupt previously initialized or shared data. Logical equality needs an ownership argument as well as matching tokens.
4. Kernel configuration and execution consistency: immutable selected parameters and call premises ensure the invoked computations are the ones covered by contracts.

Initialization and request admission establish or preserve these facts. Planning resolves exact prefix hits, allocates private suffix storage and evicts legal leaves. Forward execution applies contracts to packed rows; publication and sampler updates preserve canonical histories. Recommendation: reuse this logical-history/physical-storage decomposition for cached, batched or relocated state in VL targets.

GPU proof techniques

§5.1–5.3, pp.7–8 uses a restricted Triton subset and tile-level intermediate representation. Contracts compare selected outputs across two invocations while allowing unrelated batch data and physical layouts to differ. Fixed tile geometry and operation order matter because floating-point reassociation changes bits.

Relational structural analysis pairs value-relevant operations, guards and ordered reduction iterations. Independent parallel grid iterations need only pair selected regions. Backward dependency rules propagate the desired output region to required inputs. For matrix multiplication, selected output rows require only corresponding activation rows and contracted weight tiles; unrelated rows remain unconstrained. Z3 proves scalar, range and guard obligations.

Attention needs more than matching structure. §5.3, p.8: “Structural analysis alone cannot establish attention causality”. Forward value analysis tracks zero, one, negative infinity, masks and unchanged regions. It removes dependencies on causally masked future KV cells. Extra iterations are allowed only when proved to be an “exact identity transition”. The alignment therefore permits identity steps, rather than assuming unequal reduction ranges can be ignored. Appendix A expands the causal attention argument, including masks and finiteness premises.

Recommendation: relational equality can be easier to prove than full numerical functional correctness when the desired contract is invariance. Use selected-region contracts and identity-step reasoning to keep obligations local. Do not silently reinterpret such a proof as numerical correctness.

Evidence

§2.2 tests vLLM 0.28.0 and SGLang 0.5.19 with default and deterministic configurations, FA3/Triton backends, BF16, one H200. Table 1’s two model cases include production mismatches, especially Gemma3-4B. The authors caution: “a mismatch demonstrates numerical variation, not necessarily a bug for the intended use case” (p.3).

§6.1, p.9 reports 784 comparisons per model: 296 batching/order comparisons from 32 prompts, 90 chunk comparisons from 18 prompts, 384 prefill/decode pairs from three prompts at 128 positions each, and 14 prefix-reuse comparisons. Seven models yield “5,488 bitwise-matched pairs” for Vosti. This is a test count, not a universal empirical guarantee.

§6.2 holds batch size at four and cached context from 0 to 16K on H200 NVL. Vosti reports 1.36–3.19× decode throughput versus vLLM invariant configurations, with lower prefill throughput. A synthetic four-session, six-turn workload uses a 16K initial prompt, an 8K cached shared prefix, 256 new tokens per follow-up, 768 output tokens per turn and 0.5-second inter-turn delay. Vosti completes sessions 1.14–2.20× faster than vLLM invariant modes but “remaining slower than the default modes and SGLang’s deterministic modes” (p.10). The benchmark is deliberately decode-heavy.

Table 2, p.10 reports engine/model code: 14,043 implementation, 876 specification and 64,952 proof lines, checked in 52.9 seconds with 127 Verus workers on two AMD EPYC 9355 CPUs. Triton kernels: 3,028 implementation and 500 specification lines, 17.3 seconds per configuration on one verifier core. The custom kernel verifier has 17,182 implementation lines. The proof infrastructure is substantial; checking time does not measure proof-generation labor.

Trust and limits

§5.1, p.7: “imports kernel contracts as trusted assumptions in Verus.” “Contract translation and the correspondence between tensor representations remain trusted.” The custom analyzer’s translator, rules and solver encoding, interface mapping, Triton compiler and GPU execution also remain trusted (§5.3, p.9). Attention requires input-dependent finiteness “unchecked at runtime.” Runtime configuration checks bind launched parameters but do not prove compiler correctness.

§5.3: “Full numerical correctness against a reference semantics remains outside our scope.” §7, p.10: “A consistently incorrect implementation can still be deterministic.” Inference: returning the same wrong logits passes determinism, so VL must keep determinism and intended model semantics separate. Equal sampler states are required; equal logits alone do not couple independent random sampling.

Prior work, adoption and competitive threat

The paper builds on existing production batching, paged KV storage and deterministic kernels. Its contribution is an explicit system contract and layered engine/kernel verification. Recommendation: preserve component proofs, trusted contract translation, runtime configuration checks and tests as separate evidence categories. Check cache provenance and publication order, not just isolated data-structure methods.

Inference: this is strong evidence that real Rust/Verus systems can be verified with substantial proof infrastructure, and prior art for a specialized inference-assurance product. It does not demonstrate an autonomous agent producing the full engine proof from ordinary Rust or intent. For VL, this is a demanding domain target and useful architecture, rather than proof that general autonomous project generation is solved. Novelty of a further contract-bridge checker remains unresolved against the earlier notes’ RESOLVE/Aeneas/Alive2 comparison.

Study status: primary-paper synthesis, no artifact execution or independent reproduction. Page references are PDF pages; all numerical results above are author reports.

Validation

Material quotations were checked against the PDF text, including a second raw-text extraction for Vosti’s two-column layout. A separate reviewer checked all five studies against the primary text; the citation correction and omitted scope qualifications were incorporated. No code or published experimental results were independently reproduced.

ChatGPT offload was attempted with full PDFs. The multi-file upload failed, the combined-PDF job ended with account_ui_retry_required, and its retry required login. No ChatGPT answer was used to support the claims in this study. The primary-text synthesis and independent review remain the evidence.

Last edited: 2026-10-12