Serval is a framework for developing automated verifiers for systems software. It is based on three key strategies: lifting interpreters into verifiers under symbolic evaluation, employing symbolic profiling to identify verification performance bottlenecks, and performing symbolic optimizations to produce solver-friendly constraints. Using Serval, we build automated verifiers for RISC-V, LLVM IR, BPF, and x86-32. Below are a few results of applying the Serval verifiers.