NFT 自动做市商协议 Sudoswap 的联合创始人 Zefram Lou 最近宣布，即将推出全新去中心化交易所 TamaSwap，并称其是首个通过 Lean 形式化验证实现“可证明且不被黑客攻击”的 DEX。
TamaSwap 采用经典的 xy = k 恒定乘积模型，项目团队利用机器辅助的形式化证明，证实即便面对单一攻击者，无论其采用何种策略，都无法从系统中抽取价值。同时，协议保证流动性不会因攻击而缩水，且所有储备均由真实的 ERC‑20 代币提供支持。
在前端实现方面，TamaSwap 完全在链上部署，遵循 ERC‑4804 与 ERC‑5219 标准，实现了永久在线、无需运维、抗审查的特性。平台不收取任何协议费用，并提供“一键无代码”部署工具，任何人都可以将其快速部署到任意 EVM 兼容链上。
TamaSwap 基于 Tama + Verity 工具链构建，项目代码与形式化规范已在 GitHub 上以 AGPL 许可证开源，供社区审阅与贡献。
