Sky 合约形式化验证独立研究索引发布
热点事件持续更新
Sky 合约形式化验证独立研究索引发布
1 篇报道1 个报道来源2 小时前更新
先了解这件事
AI 综述
Bonapublica 在 Sky Forum 发布一项独立、非委托的 Sky 智能合约形式化验证研究索引，并公布首项 FA-1 结果。该研究使用 LLM 与 agentic 系统，以 Certora Prover、Halmos、Foundry、Lean 等工具开展；首个 BEAM 行动使用 Certora 及配套工具，并非基于 Lean 的证明行动。 作者明确，该研究不由 Sky 委托、不代表 Sky 进行，也不构成 Sky 认可的安全审计；它不替代认可安全公司的审计，不满足 Sky 的形式化审计覆盖要求，也不构成对任何合约或配置的官方治理批准。作者称形式化验证不是一次性认证，而是持续研究过程；可能可操作的漏洞将先通过私下安全报告与负责任披露渠道处理，再进行公开技术讨论。
AI 根据报道生成 · 2 小时前更新
最新进展11月11日 11:44
用 Agentic Intelligence 探索 Sky 智能合约的形式化保证报道时间线
沿着报道，了解事件的不同侧面。
11月11日
- Sky Forum用 Agentic Intelligence 探索 Sky 智能合约的形式化保证
一项独立、非委托研究尝试用 LLM 与 agentic 系统为 Sky 生态智能合约提供补充性形式化保证，明确不构成 Sky 认可的安全审计。研究以 Certora Prover、Halmos、Foundry、Lean 等工具开展，首个 BEAM 行动使用 Certora 及配套工具，并非基于 Lean 的证明行动。作者强调形式化验证不是一次性认证，而是持续研究过程。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。