speca

SPECA 是一个基于自然语言规范的自动化安全审计框架，将协议或系统规范转化为结构化、类型化的安全属性，并通过证明尝试（proof-attempt）推理对实现代码进行属性锚定式验证。其核心特点是支持规范驱动的漏洞检测、跨实现的可控对比分析，以及可追溯至具体流水线阶段（如规范解析、代码理解、信任边界判定）的误报归因。适用于协议栈、共识算法、密码学库等强规范约束型系统的安全验证场景，尤其适合需兼顾形式严谨性与工程实用性的专家协同审计流程。