The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language. MVP has an expressive specification language, and is fast and reliable enough that it can be run routinely by developers and in integration testing in a few minutes. Besides the simplicity of smart contracts and the Move language, three transformations are responsible for the practicality of MVP: (1) an alias-free memory model, (2) fine-grained invariant checking, and (3) monomorphization. The entirety of the Move code for the Diem blockchain has been extensively specified and can be completely verified by MVP in a few minutes. Changes in the Diem framework must be successfully verified before being integrated into the open source repository on GitHub.
翻译：Move Prover (MVP) 是用 Move 编程语言写成的智能合同的正式验证器。 MVP 具有一种清晰的规格语言,并且足够快速和可靠,能够由开发者在几分钟内例行运行和在集成测试中运行。除了智能合同和移动语言的简单性外,三处转换对MVP的实用性负责:(1) 无别名内存模型,(2) 细微的细微差异检查,(3) 单形化。 Diem 块链的移动代码的全部内容已被广泛指定,可以在几分钟内由MVP完全验证。 Diem 框架的变化必须成功验证,然后才能并入 GitHub 的开放源库 。
相关内容
微信扫码咨询专知VIP会员