RVS — RISC-V Vector Kernel Verification
Automated formal verification of quantized ML kernels against the RISC-V Vector ISA specification.
Three-layer proof pipeline: MLIR spec ↔ LLVM IR ↔ Isla ISA traces, all checked by Z3.
FMCAD 2026
13 kernels proved
Formal Methods
RISC-V