本文档描述了 Move 规范语言（MSL），它是 Move 语言的一个子集，用于指定 Move 程序的行为。MSL 与 Move Prover 一起使用，Move Prover 是一种静态验证工具，可以根据 Move 程序验证 MSL 规范的正确性。文章详细介绍了 MSL 的表达式、规范，以及表达能力。
