A unit test asks whether code works for the examples we chose. Formal verification asks a different question: does a stated property hold for every input allowed by the program? ShoggothOx uses Verus to ask that second kind of question about selected pieces of its low-level pixel mathematics.
Verus is a verifier for a subset of Rust. It extends familiar Rust syntax
with specifications such as requires, ensures,
and mathematical integer types. Verus turns those specifications into
verification conditions and asks the
Z3 SMT solver whether the conditions always follow. A successful run
is a static result: it does not add a check to every rendered frame.
Consider an increment function over an 8-bit unsigned integer. Ordinary
Rust knows that u8 ranges from 0 to 255, but
value + 1 can overflow when value is 255. The
precondition excludes that input, and the postcondition states exactly
what the function returns:
use vstd::prelude::*;
verus! {
fn increment(value: u8) -> (next: u8)
requires
value < 255,
ensures
next as int == value as int + 1,
{
value + 1
}
fn main() {
let answer = increment(41);
assert(answer == 42);
}
} // verus!
Verus proves two things here. First, the addition cannot overflow for any
caller satisfying value < 255. Second, the returned value
is the mathematical integer value + 1. It also checks each
verified call site against the precondition. This is stronger than trying
a selection of values in a test, but only with respect to the contract we
wrote.
The distinction between kinds of code matters. Verus separates code into three modes:
execspecproofSpecification and proof code are ghost code: Verus uses them while checking the program, then erases them. The executable path does not become slower because a lemma was added.
Our article on cellular automata in ShoggothOx describes the standard flame update. Each output pixel gathers four neighboring 8-bit palette indices. If their sum is s, the decay lookup implements:
The implementation precomputes this function in a 1024-entry table. That
is fast, but it creates a concrete safety question: can four pixels ever
produce an index outside 0..1024? This proof answers it:
proof fn neighbor_sum_bounded(
a: u8, b: u8, c: u8, d: u8,
)
ensures
(a as int) + (b as int) + (c as int) + (d as int) < 1024
{
}
No explicit precondition is needed. The four u8 types already
tell Verus that each input lies between 0 and 255. Therefore:
The proof body is empty because linear integer arithmetic is enough for Z3
to discharge the obligation automatically. Casting to Verus's mathematical
int makes the statement about an unbounded integer sum rather
than an overflowing machine operation.
A second lemma checks the largest value stored in the table. For every valid table index, dividing by four gives at most 255; subtracting one gives at most 254:
proof fn divsub_val_fits_u8(ii: int)
requires
0 <= ii < 1024,
ensures
(if ii / 4 > 0 { ii / 4 - 1 } else { 0int }) <= 254,
{
}
ShoggothOx then composes the two lemmas: first establish that the neighbor sum is a valid index, then establish that the indexed decay result fits in one byte. The executable loop still uses a defensive clamp before table access; the proof shows that the ordinary four-neighbor path does not need it.
spec fn divsub_formula(sum: int) -> int {
let idx = if sum < 1024 { sum } else { 1023int };
if idx / 4 > 0 { idx / 4 - 1 } else { 0int }
}
proof fn flame_output_fits_u8(a: u8, b: u8, c: u8, d: u8)
ensures
divsub_formula(a as int + b as int + c as int + d as int) <= 255,
{
neighbor_sum_bounded(a, b, c, d);
let sum = a as int + b as int + c as int + d as int;
let idx = if sum < 1024 { sum } else { 1023int };
divsub_val_fits_u8(idx);
}
There is a similar small proof behind the
translation-table lookup: for a nonempty
buffer, source_index % length is always less than
length. These are modest properties, but they sit inside
loops executed once per pixel and are good candidates for exhaustive
reasoning.
ShoggothOx pins a Verus release in its Nix development environment so a
proof is checked with a reproducible toolchain. Proof modules are guarded
by cfg(verus_only): normal Rust builds omit Verus-specific
syntax, while the verification build includes it. The pre-commit workflow
runs:
cargo verus verify -p shoggothox-core
Verification complements, rather than replaces, the existing Rust unit tests and browser tests. Tests remain better for examples, integration, rendering behavior, and regressions that are awkward to specify as logic. Verus is strongest where we can state a compact invariant over a large input space.
It is important not to overstate what the green verification result means. Today, ShoggothOx uses Verus selectively for mathematical lemmas that mirror its flame and translation logic. It does not formally verify the entire application, its audio stack, platform integrations, WebGL or WebGPU drivers, or the visual quality of a rendered frame.
The current proofs also do not yet establish a full refinement theorem connecting every line of the executable lookup-table construction to its mathematical specification. They establish useful local facts: bounds, decay behavior, and safe index relationships. Expanding that connection is where formal verification becomes more ambitious — and more valuable.
Small proofs teach us where specifications clarify the design. A 1024-entry table is not arbitrary once its bound is written down: it is the smallest convenient power-of-two table covering every sum of four bytes. The output limit of 254 is not an observation from a test run: it follows from the decay equation for all valid inputs.
That is the practical role Verus plays in ShoggothOx today. Rust protects memory and ownership, tests exercise real behavior, and Verus checks a growing set of mathematical claims that neither can express as directly.