**研究对象：**Move Prover
产出要求：
直播分享会（$200 奖金）：
- 结合参考资料，具体解释以下内容： (1) 和单元测试相比的区别和优势 (2) 无别名内存模型(alias-free memory model)、不变量检查(invariant checking)、单态化(monomorphization)的理论和应用 (3) 验证器架构和Boogie IVL (4) 形式化验证的限制和未来
- 讲解时请注意考虑听众的理解程度
讲解时请注意考虑听众的理解程度
参考资料：
- Fast and Reliable Formal Verification of Smart Contracts with the Move Prover：https://arxiv.org/pdf/2110.08362.pdf
- The Move Prover： https://www-cs.stanford.edu/~yoniz/cav20.pdf
欢迎你通过自行检索查找相关资料；如果在研究结果中使用了其他资料来源，请注明。
语言要求：研究成果产出要求中文，但是需要你有英文文献阅读能力
报名流程：
请在本页面左侧点击Participate进行初步报名； 研究开始前，我们需要简单的资质审核。请联系官方 Telegrams support账号：@HackerDojo0或者添加微信@HackerDojo0。 最先通过审核的申请者即获得Bounty认领权，可以开始研究； 确认你的研究进度后，Dōjo团队将为你安排直播分享会，展示你的研究成果； 完成直播分享会与文稿后，请在本页面进行奖金认领。（hunter奖励认领指南：https://dorahacks.io/blog/guides/bounty-hunter/）
关于Hacker Dōjo
Hacker Dōjo是由hacker共建的加密、Web3前沿技术开源知识社区。Dōjo会以直播/音频/文字等形式定期组织分享session，内容包括Web3领域前沿技术论文解读、技术研讨、工作坊、技术领袖研讨会等。
加入Dōjo的Hacker可以提出自己的学习期望，主动提案自己擅长的技术话题，由Dōjo组织分享。同时，Hacker Dōjo推出Web3前沿课题研究计划，定期选题，由hacker进行研究和讲解，并以bounty形式奖励研究贡献者。
联系我们: Telegram: @HackerDojo0 WeChat: @HackerDojo0 E-mail: hackerdojo0@gmail.com