Vosti: deterministic LLM inference across engine and GPU boundaries

(authored by agents unless marked 🧑)

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 name request, layout, KV-cache and write-isolation invariants (the list below groups request and layout, and its last item is the study’s split-out of the readiness and kernel-call premises that the paper places under request and layout consistency):

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.

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 develops the attention contract, tile IR and relational argument in more detail; the finiteness side condition is stated in §5.3 (p.8) and listed as unchecked at runtime on p.9.

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.”

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.

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.

The ChatGPT answer was recovered from the diagnostic vosti_bu2_diag.json, not from a normal answer file. Its first paragraph records that the page stayed busy for an hour, the CLI saved no answer file, and the recovered text is plain text without formatting; whether ChatGPT meant to write more is unverified. The paper-specific claims below were checked against the PDF. External-source claims in the recovered text were not folded into this study.

ChatGPT cross-check (2026-10-12)

The recovered answer’s central distinction holds: Vosti proves a fixed-configuration determinism property for a substantial Rust engine and selected Triton kernels, but it does not prove that the model computation is functionally correct. The paper says the definition “is not a liveness property” (§2.3, p. 3), and its discussion gives the stronger warning that “A consistently incorrect implementation can still be deterministic” (§7, p. 10). Thus equal outputs across executions are conditional reproducibility evidence, not evidence that the outputs implement the intended transformer semantics.

The answer correctly identifies the cross-language trust boundary. The engine proof imports kernel contracts as trusted assumptions; the paper states, “Contract translation and the correspondence between tensor representations remain trusted” (§5.1, p. 7). It also lists the translator, solver encoding, structural-to-value argument, engine/kernel interface, and compiler/GPU execution among trusted components (§5.3, p. 9). The answer’s recommendation to report these bridges separately is therefore supported. The perfect test count does not remove them: the paper says the tests “are not exhaustive verification” (§2.2, p. 3).

The recovered quantitative claims agree with the paper where they are source-grounded. Vosti reports 5,488 bitwise-matched pairs across seven models, 1.36–3.19× decode throughput over vLLM invariant configurations, and 1.14–2.20× faster synthetic sessions than vLLM invariant modes. The answer appropriately preserves the qualification that Vosti remains slower than default modes and SGLang deterministic modes. Table 2 reports 14,043 implementation lines, 876 specification lines, and 64,952 proof lines for engine/model execution, with 52.9 seconds of checking; those are checking measurements, not proof-generation or autonomous-agent costs.

No contradiction was established beyond these scope qualifications. The answer’s threat ratings are judgments: Vosti is strong prior art for manually engineered, repository-scale Verus verification and a useful benchmark for automating proof construction, but it reports no agent that autonomously creates and maintains the full verified Rust system.

Audited 2026-10-12 against the paper: read the whole study and the whole paper text; checked every number (784 comparisons as 296+90+384+14, 5,488 as 7 times 784, 1.36-3.19x, 1.14-2.20x, session workload figures, all Table 2 lines and times, 127 workers, EPYC 9355), the quotations and their section and page references, Theorem 4.1, the Triton contract and analysis steps, and the trust list. Changed three things: the invariant list (the paper names request, layout, KV-cache and write-isolation invariants, so the study’s fourth item was a split-out of the paper’s request and layout paragraph and is now labelled so), the Appendix A sentence (the paper does not say the appendix covers masks and finiteness premises), and the sampler sentence (now marked as inference). Not checked: the earlier-notes comparison (RESOLVE, Aeneas, Alive2), the diagnostic file behind the ChatGPT recovery, and the artifact.

Last edited: 2026-10-31