Foresight News 消息，NFT 自动做市商协议 sudoswap 联合创始人 Zefram Lou 拟推出 TamaSwap，并表示 TamaSwap 为首个通过 Lean 形式化验证实现「可证明且不被黑客攻击」的 DEX。该项目基于经典 xy=k 模型，通过机器验证证明单一攻击者无论采取何种操作都无法从系统中提取价值，同时确保流动性不会减少且储备始终由真实 ERC-20 代币支持。

TamaSwap 前端完全部署在链上（遵循 ERC-4804/ERC-5219），实现永久在线、无需维护和抗审查。此外，项目无协议费用，且支持任何人一键无代码部署到任意 EVM 链。TamaSwap 由 Tama + Verity 工具链构建，代码与形式化规范已在 GitHub 开源（AGPL 许可）。