协议状态机不再靠检索拼上下文：State-inferer按依赖切片喂给大模型，严格F值达95.2
State-inferer把协议实现的状态机提取改成按程序依赖切片：从状态变量赋值出发，在系统依赖图上做有深度上限的前向与后向搜索，为每条状态转移切出一段紧凑代码交给大模型，再把RFC安全属性特化成该模型上的线性时序逻辑公式，用nuXmv模型检验。在TLS、IKEv2、SSH的七个开源实现上，其宏平均严格转移级F值为95.2，最强基线Codex为78.9；并发现四个此前未知漏洞，均已获得CVE或CNVD编号。