用途：对 DEX 的 Plutus V3 Aiken 合约（验证器与铸造策略）做对抗性安全审计，产出含威胁模型、不变量、漏洞发现和可复现利用交易形态的严谨报告。
主要能力：提供完整审计工作流——构建系统模型（状态 UTxO、资产、脚本地址、状态转移）；提取可测试的显式不变量（价值守恒、LP 供应规则、费用边界与舍入、授权规则、唯一状态 UTxO、datum/价值增长有界）；建立威胁模型与攻击面；手工链上审查各验证器/策略分支，重点排查双重满足、伪造状态 UTxO、资产类别不匹配、可选 datum 陷阱、无界增长、时间范围漏洞、除法/舍入/负数问题及“恰好一个”执行缺陷；链下审查交易构建器；用 Aiken 单元测试与属性测试为每个不变量和漏洞回归提供证据；做预算与 DoS 分析。报告使用既定模板。
使用方式与所需输入：需要脚本清单与用途、datum/redeemer 模式、参数配置（策略 ID、脚本哈希、升级/管理控制、预言机依赖）、范围内链下交易构建器、网络假设与约束。缺失项需明确索取。相关文件：references/audit-framework.md、templates/audit-report.md、templates/invariants-checklist.md、templates/tx-shapes.md。
限制与规则：不得臆造，不在仓库或输入中的内容须标注未知并列出缺失项；假设攻击者可构造任意交易；绝不索取或处理助记词/私钥；以证据优先（最小交易形态+失败测试+修复+通过测试）。