DDR5内存标准引入了每行激活计数（PRAC）作为缓解Rowhammer攻击的机制，通过跟踪每行的激活次数并在超过阈值时触发缓解刷新。然而，当前PRAC设计的安全性评估依赖于人工构造的攻击模式，缺乏对安全属性的形式化验证或自动化漏洞发现技术。本文提出AutoPRAC，首个利用模型检查器自动化测试PRAC防御安全性的框架。AutoPRAC将PRAC实现建模为有界状态机，并针对最坏情况下的神谕攻击者检查安全关键属性。若属性被违反，框架会生成具体的反例轨迹，对应一次成功的攻击。使用AutoPRAC，作者在最新的PRAC防御方案MOAT中发现了一个此前未报告的缺陷：其计数器重置策略允许最多34次激活超过Rowhammer阈值而未被检测到。实验表明，AutoPRAC能够自动发现Rowhammer缓解措施中的细微安全缺陷，可作为PRAC设计的早期攻击发现辅助工具。该研究为硬件安全验证提供了新思路，尤其适用于新型内存防御机制的形式化分析。