修改xv6的内核接口，构建状态机规范和声明式规范以支持SMT（Satisfiability Modulo Theories）求解器来进行验证。通过有限化内核接口，使用硬件虚拟化简化虚拟内存推理，并在LLVM IR级别工作，以避免对C语义进行建模，从而实现了"一键验证"。
诚
