论文导读系统形式化验证Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent SystemsSharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems