3.2 形式化验证

我们进一步强调了重要的形式化规范，用时态逻辑定义稳定币的稳定性（或非挥发性）[21]。具体地说，稳定性（非挥发性）是通过以下两个属性（A和G是量词，即，对于状态空间中的所有路径和路径的所有状态[21]）来指定的。

稳定性规范（非挥发性）。在扩张有效性和收缩有效性中规定了两个属性，以形式化价格波动弹性（以Basis Cash为例）。根据扩张有效性的形式化，在P处于扩张状态而E处于验证状态的情况下（即，扩张已被强制执行），X不得停留在购买状态以使价格下跌，即买方市场。同样地，当P处于收缩状态，C处于有效状态时，X不能处于卖出状态，即卖方市场。

反例分析。我们使用时间自动机的Uppaal模型检查器[16]验证了Basis Cash模型。图2显示了稳定性属性的两个反例，即Basis Cash可能变得不稳定的条件。图2a描述了一个违反扩张有效性的交易场景。具体来说，BAC的需求增长发生在扩张过程开始铸造和分销新的稳定币时。结果，DEX变成了买入而不是卖出的状态，从而触发了一个反例。在收缩有效性方面，图2b显示了Basis Cash的另一个潜在波动性。当BAC的价格跌破联系汇率制度时，这种收缩使得投资者可以将BAB与BAC互换。然而，如果互换没有发生，因此BAC的供应量保持不变，则由于DEX进入卖出状态而不是预期的买入状态，因此违反了收缩有效性。

4 实证分析

在对Basis Cash进行正式建模和验证的基础上，我们现在用实际市场观察进行了实证分析。可以使用查询和数据(https://explore.danealytics.com/dashboard/winky)在Dune Analytics[3]平台上。

正常情况。图3a和3b显示了扩张和收缩效果良好的两种情况。如图3a所示，随着新BAC的铸造，其价格逐渐下降。类似地，在图3b中，许多BAC因收缩而被烧毁，其价格开始上涨。

扩张破裂。图3c和3e解释了2020年12月14日和15日§3.2中推断的扩张破裂。在图3c中，扩建于00:00开始，并收集了新铸造的BAC。然而，它的价格在7小时内从1.35美元上涨到1.56美元（12月14日），从1.62美元上涨到1.76美元（12月15日），增长了15.72%和8.40%。根据图3e，如图3e所示，需求的快速增长导致了扩张断裂式的破裂。由于BAC-DAI在早期非常流行，并导致了极高的产量率，因此即使在扩张点，BAC的需求也会迅速提升。2020年12月14日，新铸造的BAC有92%的资金在扩建后2小时内进入了流动性挖矿池，这也反映了BAC的受欢迎程度。

收缩中断。图3d和3f也证实了由于收缩破裂而导致的潜在波动性。从2021年1月11日到撰写本报告时，尽管收缩的条目不断打开，但根据图3d，BAC的价格一直保持在联系汇率制度之下。其背后的原因是参与收缩的比例较低，即许多投资者不愿意将BAC换成BAB，因为他们担心自己可能永远无法赎回。如图3f所示，这一时期燃烧的BAC（驼峰）数量比几天前小得多。 (责任编辑：admin)