zkvmBlast compares several zkVMs against a reference simulator, finding bugs single-VM fuzzers politely miss.

Formalizes a STARK in Isabelle/HOL, with executable prover/verifier models and staged soundness bounds, because math wasn't enough.