一句话：FlowChecker 让工程师用 CTL 公式表达项目特定时序控制流规则，自动抽取有限控制流模型并用 Datalog 引擎求不动点完成模型检测。
工业界的正确性规则往往隐式存在，仅靠代码评审和团队约定维护。其中许多规则本质上是时序控制流义务，例如缓存加载路径不得污染缓存、错误不得在有效性判定之前抛出、失败必须跨组件边界保持可见。现有形式验证与静态分析虽可支持类似检查，但每条团队规则都需改写成定制遍历逻辑、测试驱动的执行探索或工具专属协议规约，难以日常使用。FlowChecker 面向开发者，将规则写成作用于熟悉程序事件的可评审 CTL 公式；系统抽取有限控制流模型，保留与规则相关的异常与框架中介路径，并在优化 Datalog 引擎 Soufflé 中通过求 CTL 不动点来检查公式，使检查可在本地与 CI 中重复执行，同时明确将结论限定于所抽取的模型。评估在 7 个公开 Java 项目上开展 42 项检查，覆盖可达性、异常传播、事件顺序及包装/捕获，公式从单一时序义务到嵌套组合；此外还研究了多达一千万状态的合成模型，以及来自阿里云的五个脱敏内部落地案例。
Industrial correctness rules often remain implicit, enforced only by review and team convention. Many such rules are temporal control-flow obligations: a cache-loading path must not pollute the cache, an error must not be raised before validity is decided, or a failure must remain visible across component boundaries. Existing formal verification and static analysis techniques can support related checks, but routine use remains hard when each team rule must be recast as custom traversal logic, harness-driven execution exploration, or a tool-specific protocol specification. We present FlowChecker, a developer-facing model-checking system for project-specific temporal control-flow rules. Engineers express rules as reviewable CTL formulas over familiar program events; FlowChecker extracts a finite control-flow model, preserves rule-relevant exception and framework-mediated paths, and checks the formula by evaluating CTL fixpoints in Soufflé, an optimized Datalog engine. This makes temporal control-flow checks repeatable locally and in CI, while keeping verdicts explicitly scoped to the extracted model. Across seven public Java projects, we evaluate 42 checks covering reachability, exception propagation, event ordering, and wrapping/capture, with formulas ranging from single temporal obligations to nested compositions. We additionally study synthetic models up to 10 million states and five sanitized internal adoption cases from Alibaba Cloud Computing.