创世的抵押品比率r为1.0。原则上，铸造一定数量的远期外汇包括将价值的n × r作为抵押品，并用外汇兑换券烧掉价值的 n ×（1−r）。当价格超过固定汇率时，该协议为投资者创造新的远期利率提供了动力。因此，预计FRAX供应的增加将逐步促使价格下降。在价格低于挂钩汇率的情况下，该协议允许投资者将价值1美元的抵押品和FXS的组合与价值低于1美元的单一远期外汇进行互换。这样的激励措施可能会产生远期外汇购买，并提高其价格。

3. 建模与验证

3.1 稳定币的建模

我们强调了稳定币的形式化建模框架M，M := < P，E，C，S，B，X >是一个由六种时间自动组成的网络[7]，每种时间自动机都是一个元组Q := < S，s0，X，a，T，I，Sn >。S是有限状态集。s0∈S是初始状态。X是一组非负实数作为时钟变量。Sn⊆S是一组接受状态。A是一组动作，I是一组分配给状态的不变量。假设Φ是约束函数，T⊆S×Φ（X）×2X×A×S是状态转换< s、A、g、R、s0>的集合，其中S和s0是源状态和目标状态，A是动作，g是启动转换的条件，R是要重置的时钟集。

此外，M通过四类同步信道Ω提供通信：={ωe，ωc，ωx，ωu}。特别地，ωe和ωc被设计来触发扩张和收缩过程。ωx模拟市场交易活动，生成新的稳定成本价格。ωu在E、C和X之间同步更新。特别是，我们在图1中给出了Basis Cash的正式模型。该框架适用于其他类型的稳定币。由于页面限制，我们选择了Basis Cash，因为它体现了一种典型的模式，是在撰写本文时最受欢迎的市场之一。

–P 将主协议建模为五种状态，即初始状态、扩张前状态和扩张后状态（当价格高于挂钩时）、收缩前状态和收缩后状态（当价格低于挂钩时）。在两个跃迁上，扩张（ωe）和收缩（ωc）通道被激活，从而实现扩张和收缩过程。

–E 自动机定义了一个具有时钟 t 和三种状态的进程。E响应P的扩张请求。执行扩张转换以增加稳定币的供应（即全局变量N bac）。如果 t 在扩张点（例如24:00 UTC），则允许转换。对于Basis Cash，E创建两个扩张转换，并通过更新通道（ωu）与X同步。

–C 自动机抽象了收缩过程。与E类似，提供了一个转换，通过更新一个全局变量来细化供应量的减少，另一个转换的目的是模拟供应量保持不变（投资者可以选择不将BAB换成BAC）。

– S和B是用来模拟交易中买卖双方的行为的。它们通过ωx通道生成随机交易请求。

–X 引入了一个带有自动做市（AMM）的去中心化交易所（DEX）抽象模型，例如Uniswap[6]。X定义了“卖出”和“买入”状态，以表明它是买方市场（即卖方多于买方）还是卖方市场（反之亦然）。新的价格是根据AMM和它的稳定币库计算的。 (责任编辑：admin)