Research
Authorized access only
←
RVS — RISC-V Vector Kernel Verification
- Problem: Nobody formally verifies vector/SIMD kernel implementations against ISA specs
- Method: Three-layer pipeline — MLIR spec ↔ LLVM IR ↔ Isla ISA traces, all reduced to Z3 SMT
- Result: 13 llama.cpp quantized kernels proved equivalent, fully automated, <2s per kernel