Earlier technical work. This paper method can support a bounded compute test. It is not the current Ashiba offer. See current Ashiba work →
Method
How Ashiba attributes silent-correctness failures across silicon.
Two ML kernels can disagree numerically, pass functional tests, and remain correct under a given contract. No formal artifact grades that result today. That is the specification gap. Kernel Contracts defines a language for the gap.
The contract object
A kernel contract is an eight-part formal object:
- Identifier — fully-qualified name
- Scope — shapes, dtypes, devices, backends
- Precondition — constraints on inputs
- Postcondition — declarative clause over output and reference
- Tolerance — allowed deviation from reference, substrate-parameterized
- Reference oracle — implementation that defines the postcondition
- Measurement protocol — how to observe conformance
- Violation signature — measurable deviation that constitutes a violation
Three primitives, twelve classes
All twelve contract classes group under three physically-grounded failure primitives:
Path dependence. The result depends on an evaluation order the contract allows to vary. Root cause: IEEE 754 non-associativity combined with non-deterministic parallel scheduling.
Domain violation. The operator encounters inputs outside its valid domain — subnormals, NaN, overflow, out-of-range indices. Root cause: finite precision combined with unconstrained input distributions.
Resource contention. The result depends on concurrent access to shared silicon resources — atomics, memory-model reorderings, collective-operation arbitrations. Root cause: shared-memory concurrency combined with silicon-specific arbitration policies.
Three primitives, twelve manifestations, one framework.
What the method can produce
The paper draws on prior work in numerical analysis, statistical process control, fault tolerance, and probabilistic verification. A future implementation could produce:
- A contract suite that states the kernels, shapes, precision, devices, and tolerances in scope.
- A measurement protocol with executable checks and stated error bounds.
- A result record that separates supported results, failures, and unknowns.
- A decision input that a buyer can review with other deployment evidence.
Intellectual ancestry
Shewchuk 1997 on adaptive-precision geometric predicates. Demmel and Nguyen on ReproBLAS. Backward error analysis by Wilkinson. Bates on approximate-computing error debt. The silicon-test lineage: Shewhart SPC, ATPG, Huang-Abraham ABFT, Freivalds. Each contributes one component of the framework. The port from silicon test to ML kernel is the work.
See also
- Paper: Kernel Contracts
- Reference verifier: experimental source release under review
- Current work: Ashiba’s current work