香山缓存系统的形式化验证