Kernel Contracts: A Specification Language for ML Kernel Correctness Across Heterogeneous Silicon

• URL: http://arxiv.org/abs/2604.22032v1
• Date: Thu, 23 Apr 2026 19:46:52 GMT
• Title: Kernel Contracts: A Specification Language for ML Kernel Correctness Across Heterogeneous Silicon
• Abstract summary: ML kernels ship with an implicit contract about what it computes.<n>Recent empirical work has measured the gap across silicon platforms, but none of it specifies the contract being violated.<n>We present a specification language for kernel contracts.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Every ML kernel ships with an implicit contract about what it computes. People rarely write the contract down. When two kernels disagree -- when a matmul on AMD produces a different gradient than the same matmul on NVIDIA, when a fused attention kernel silently downcasts an accumulator, when an out-of-bounds access returns zero on one stack and garbage on another -- there is no formal artifact to arbitrate the dispute. Recent empirical work has measured the gap across silicon platforms, but none of it specifies the contract being violated. We present a specification language for kernel contracts. A contract has eight parts: identifier, scope, precondition, postcondition, tolerance, reference oracle, measurement protocol, and violation signature. We use it to state twelve contract classes covering precision, ordering, compiler-induced, and exceptional-value failure modes, each grounded in published empirical evidence. We require a three-state calibration: every contract must admit at least one reference-conforming implementation and at least one contract-violating implementation that passes basic functional tests. We apply the framework to three documented incidents -- Huawei Ascend silent precision coercion, Sakana AI CUDA Engineer reward hacking, AMD out-of-bounds silent acceptance -- and show that each informal diagnosis maps to a specific contract violation with a measurable signature. A kernel contract suite is a normative reference against which conformance can be graded, in the way that ISASecure grades industrial control systems against IEC 62443.

Related papers

• A Contract-Grade Verifier for LLM-Generated GPU Kernels, and a Native Blackwell Backward for the Gated-Linear-Recurrence Family [0.9740025522928777]
  Systems that generate GPU kernels with language models report high correctness rates.<n>Those rates come from a single loose test: run the kernel on a few random inputs at one fixed shape and accept it if the output is close to a reference.<n>We build a contract-grade verifier of twelve adversarial gates, each a property a correct kernel must satisfy, several of them tolerance-free.
  arXiv  Detail & Related papers  (2026-08-13T01:25:56Z)
• One Recipe, Many Harnesses: What Self-Evolution Encodes Across Languages and Models [46.83445434865936]
  Self-evolving harnesses are closed-loop systems in which an agent inspects its own rollouts and edits its prompts, tools, and memory.<n>It remains unclear whether they encode benchmark-specific adaptations, language-specific engineering knowledge, or compensation for limitations of the underlying model.
  arXiv  Detail & Related papers  (2026-08-10T19:45:45Z)
• Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification [7.004725450780227]
  We present the first contract-based regression verification tool.<n>Contract soundness is ensured by proving all function versions match the behavior.<n>We ask whether a partial, caller-sufficient contract, rather than a full behavioral specification, is enough.
  arXiv  Detail & Related papers  (2026-07-11T12:40:22Z)
• Can Code Specify a System Precisely Enough to Formally Verify It? [0.0]
  This paper evaluates both on production software: the payment workflow of an operational restaurant point-of-sale system.<n>The core protocol is correct relative to a hand-built, line-cited model under a precisely stated failure model.<n>A single probe of the production payment sandbox exposed a response-shape divergence that makes an entire recovery ladder unreachable.
  arXiv  Detail & Related papers  (2026-07-06T13:39:00Z)
• Gaming the Metric, Not the Harm: Certifying Safety Audits against Strategic Platform Manipulation [1.253312107729806]
  We ask when an audit metric can still certify a genuine reduction in harm.<n>The protocol is modeled as a published transformation graph whose connected components form semantic classes.<n>We check the claims at three levels: exhaustive enumeration on a finite-state grid of mixed strategies, an SMT encoding in Z3 cross-replayed in cvc5, and a bounded single-player MDP encoded in PRISM-games.
  arXiv  Detail & Related papers  (2026-05-07T14:22:21Z)
• Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
  We propose a paired-outcome measurement interface for auditing a single protocol step on exact-match tasks.<n>For each instance, the interface records a baseline correctness bit and a post-step correctness bit.<n>These rates predict accuracy changes and define a reusable empirical interface testable across seeds, mixtures, and pipelines.
  arXiv  Detail & Related papers  (2026-04-20T13:25:40Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  Existing benchmarks test only individual languages/tools, so the performance numbers are not directly comparable.<n>We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean.
  arXiv  Detail & Related papers  (2026-02-10T06:58:26Z)
• Outrunning LLM Cutoffs: A Live Kernel Crash Resolution Benchmark for All [57.23434868678603]
  Live-kBench is an evaluation framework for self-evolving benchmarks that scrapes and evaluates agents on freshly discovered kernel bugs.<n> kEnv is an agent-agnostic crash-resolution environment for kernel compilation, execution, and feedback.<n>Using kEnv, we benchmark three state-of-the-art agents, showing that they resolve 74% of crashes on the first attempt.
  arXiv  Detail & Related papers  (2026-02-02T19:06:15Z)
• Do Large Language Models Respect Contracts? Evaluating and Enforcing Contract-Adherence in Code Generation [11.445615378917578]
  PACT is a program assessment and contract-adherence evaluation framework.<n>It provides a comprehensive test-suite corpus focused on contract violations.<n>It enables a systematic analysis of code generation under varied prompting conditions.
  arXiv  Detail & Related papers  (2025-10-14T01:12:37Z)
• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  We introduce SolBench, a benchmark for evaluating the functional correctness of Solidity smart contracts generated by code completion models.<n>We propose a Retrieval-Augmented Code Repair framework to verify functional correctness of smart contracts.<n>Results show that code repair and retrieval techniques effectively enhance the correctness of smart contract completion while reducing computational costs.
  arXiv  Detail & Related papers  (2025-03-03T01:55:20Z)
• Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety [8.906268052552582]
  1.45-million contracts form a single "gigantic program"<n>Can programmers be assured that this gigantic program conforms to high-level safety specifications?<n> Static code verification cannot be faithful to this gigantic program due to its scale and high polymorphism.<n>Our technology, called Theorem-Carrying Transactions (TCT), combines the benefits of concrete execution and symbolic proofs.
  arXiv  Detail & Related papers  (2024-08-12T20:27:41Z)
• JailbreakBench: An Open Robustness Benchmark for Jailbreaking Large Language Models [123.66104233291065]
  Jailbreak attacks cause large language models (LLMs) to generate harmful, unethical, or otherwise objectionable content. evaluating these attacks presents a number of challenges, which the current collection of benchmarks and evaluation techniques do not adequately address. JailbreakBench is an open-sourced benchmark with the following components.
  arXiv  Detail & Related papers  (2024-03-28T02:44:02Z)
• Contract Usage and Evolution in Android Mobile Applications [45.44831696628473]
  We present the first large-scale empirical study on the presence and use of contracts in Android applications, written in Java or Kotlin. We analyzed 2,390 Android applications from the F-Droid repository and processed more than 51,749 KLOC. Our findings show that it would be desirable to have libraries that standardize contract specifications in Java and Kotlin.
  arXiv  Detail & Related papers  (2024-01-25T15:36:49Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.