Before You Code: DeFi Applications of TLA+

Written by Mark Ettinger – Lead Data Scientist

This is part one of a series of articles on the benefits of using lighweight formal methods in the design process of DeFi Protocols.

Decentralized finance (DeFi) has tremendous promise but anyone following current progress is all too aware of the potential financial dangers of interacting with DeFi protocols. Hacks occur on a regular basis which result in loss of crypto-assets. The value of these hacks often exceeds tens of millions of dollars and sometimes exceeds hundreds of millions of dollars. Auditing is the gold standard for reducing vulnerabilities specific to languages used for programming smart contracts. However many times these hacks are executed through attacking vulnerabilities within the logic of the system. Logical flaws can be extremely difficult to find during design because often the tool used to exploit the logic may not yet exist (e.g. the rise of flash loans and their use to exploit protocols).

This highlights a fundamental difficulty in protocol design. How can you mitigate attacks when you might not be able to conceive of the method of attack? At Volatility Group we believe that many logical insecurities can be prevented through the efficient use of lightweight formal methods. Using a language like TLA+ and a model checker allows you to build the system’s logic and verify the reachable states do not exhibit unexpected behavior.

Besides discovering logical insecurities, using a lightweight formal method language like TLA+ prior to coding improves the design process in three ways:

  1. The act of formalizing clarifies the thinking process. Specifically, in our experience the design and development team moved from thinking procedurally (i.e. how do we design for implementation) to logically (i.e. what are the states of this system).
  2. Writing a specification in a mathematical language rather than natural language removes all ambiguities.
  3. With ambiguities removed, the specification serves as a blueprint against which any implementation can be compared and judged to be correct or incorrect.

This series of posts will summarize our recent explorations using TLA+, a formal specification language. We began this exercise when one of us (Ettinger) became uncomfortable trying to understand the very complex and ambiguous “big picture” of how the DAOracle protocol worked. It was only through mathematics that the ambiguity was eliminated and the complexity wrangled. We should note that while this post emphasizes the importance of using TLA+ before writing code, that is not the process that was used for Version 1 of the DAOracle. We designed the protocol iteratively and wrote the code without a lightweight formal specification. Retrospectively using TLA+ uncovered various problematic issues with Version 1 and has helped to improve our process immensely. We plan on using TLA+ prior to writing code for future versions of the protocol.

A simple example of TLA+ from wikipedia showing every state of a one-bit clock ticking endlessly from 0 to 1. You can find more examples of TLA+ here.

What Are Formal Methods?

The subfield of computer science called formal methods has been around for decades but is rarely used in software engineering practice due to the requirements of specialized knowledge, extensive training with novel computational tools, and significant amounts of human effort that is difficult to automate. However, the basic idea of formal methods is quite simple and elegant. The basic idea is to treat algorithms as mathematical objects with which we can rigorously reason and mathematically prove that various expected properties hold. This is not unlike when you took your first geometry class in high school and learned to prove properties of triangles, circles, and other geometric objects. However in formal methods, a notion of proof is introduced which goes beyond the proofs typically expressed with a combination of mathematical symbolism and natural language. Proofs in formal methods are called formal proofs because they are expressed in a formal mathematical language and can be checked for correctness by a computer unlike traditional proofs which you would find in a journal. Formal methods have the advantage of bringing the power of mathematics to bear on software engineering but also carry the disadvantages mentioned above. Perhaps we can have the best of both worlds by using so-called lightweight formal methods.

Lightweight formal methods retain the use of a formal mathematical description language for algorithms and protocols but dispense with formal proofs. This significantly reduces the time and resources necessary for creating a specification. You might now be wondering, “If we drop proofs, what remains?” In lightweight formal methods we retain two crucial elements to aid us in our goal of creating secure software:

  1. A formal language which enables us to specify and model protocols with mathematical precision.
  2. Tools for exploring the state space of our models called model checkers.

These two affordances of lightweight formal methods are briefly described below and we intend to expound on both topics at length in future entries in this series of articles. But first let us give an overview of the technical aspects of TLA+

The Mathematics of TLA+

The most difficult aspect of learning to use TLA+ is not mathematics or anything technical but rather learning to think logically rather than procedurally. This is especially true for programmers who are accustomed to describing what the computer should do next. In contrast, TLA+ is built on logic and specifies which state transitions are permitted. (Note: There is also a pseudocode-like language, PlusCal, which mimics procedural thinking and compiles to TLA+. We prefer to use TLA+ directly and do not use PlusCal though some of the references below favor it).

The way one uses TLA+ to write a specification is actually straightforward in theory as TLA+ uses state machines as the models for discrete dynamical systems. A state is an assignment of values to temporal variables. These variables are called temporal because the values assigned to them change over time. Using the linguistic elements described below, one first specifies all the valid initialization states. Then one specifies the valid transitions from one state to the next. That’s it! These two declarations serve to define all valid behaviors of the system.

The initial state and potential next states for UMA’s Optimistic Oracle. The left image shows TLA+ syntax while the right image shows the mathematical specification produced from TLA+.

The syntax of TLA+ can be described as combining three components which we express heuristically as:

TLA+ = First Order Logic + (Linear) Temporal Logic + (Naive) Set Theory

The first component means TLA+ uses all the standard logical connectives and quantifiers, e.g. “and”, “or”, “not”, “implies”, “for all”, and “there exists”. The second component means TLA+ has temporal “modal” operators intuitively expressing the temporal concepts of “always” and “eventually.” Finally, the third component means that everything expressed in TLA+ is a set, though the set theory involved in TLA+ is very basic, including notions like “subset” and “element of” and contains none of the sophisticated mathematics that set theorists study.

In traditional formal methods, after writing a specification we would then prove theorems which hold for all behaviors. Indeed, TLA+ has a tool called the TLA Proof System (TLAPS) which facilitates the construction of proofs but since we are currently only describing lightweight applications we will not discuss this aspect further. (See Specifying Systems for further details on TLAPS.) Rather than proving theorems, which is difficult, time consuming, and costly, we are interested in the easy, fast, and inexpensive benefits which come from the clarity that formal specifications provide and finding unexpected behaviors through model checking.

The Benefits of Formal Specification

There are several benefits to composing a formal specification even without the intention to do any theorem proving or model checking down the road. We regard these benefits as the dramatic low-hanging fruits of lightweight formal methods. These low-hanging fruits are why we are so passionate about our use of TLA+ internally at Volatility Group and also about communicating these advantages to the wider DeFi community. There are three benefits to writing a specification of a protocol in a formal language:

  1. The specification serves as a blueprint against which any implementation can be compared and judged to be correct or incorrect.
  2. Writing a specification in a mathematical language rather than natural language removes all ambiguities.
  3. The act of formalizing clarifies the thinking process.

Regarding the first point, it is important to notice that a formal blueprint is a necessary and sufficient condition for evaluating a piece of software for correctness. Without a specification, the code itself serves as it’s own trivial blueprint in the sense that any and all behavior permitted by the implementation is “correct” by definition. Unintended behaviors, especially logical hacks of protocols, reveal this state of affairs to be unacceptable. A formal mathematical specification fixes this issue.

The third point is a bit more subtle than the first two and requires actual experimentation with formal specification to really “get it.” Writing a specification reveals errors in thinking which are extremely difficult to discover. Turing award winner Leslie Lamport, the creator of TLA+, summarized this by saying “Writing is nature’s way of telling us how lousy our thinking is.”

This is perhaps a good time to address the proper place of a formal specification in the software development workflow. Formal specification should ideally be completed before any implementation is begun. At Volatility Group we became involved with TLA+ only after the initial design and implementation of the DAOracle protocol in Solidity. Nonetheless, writing our TLA+ DAOracle specification ex post facto served to clarify ambiguities and shortcomings in the initial implementation and to serve as a blueprint for the next iteration of the protocol. Going forward, Volatility Group intends to implement the proper workflow of writing a specification before any coding for all future protocols.

The Benefits of Model Checking

A model checker is a computational tool that exhaustively searches the state space of a finite state machine for counterexamples of an expected property. If the state machine is not finite, i.e. the number of possible states is infinite, then a model checker may be used to search a finite subset of the infinite state space. If no counterexample is found in the finite case then the model checker has verified the property holds for all behaviors of the system. In the infinite case the model checker can only explore a finite subset X and therefore may have missed a counterexample to the property that falls outside X. In spite of this limitation, there is empirical folk wisdom that small counterexamples often exist for real-world system models and can be discovered with a reasonable amount of computation using model checkers. Modern model checking algorithms are highly optimized to avoid redundant calculations. Very large state space may be exhaustively explored by exploiting symmetries. Furthermore, many model checkers translate the problem into a statement of propositional logic, thus leveraging recent dramatic advances in SAT-solver algorithms. TLA+ has a model checker, TLC, which can be used to perform model checking for models corresponding to a large subset of the TLA+ language. Model checking will be discussed at length in a future entries in this series.

Next Up

In the next entry in this series on applications of lightweight formal methods to decentralized finance, we explore our specification of the UMA Optimistic Oracle in detail. In particular, we illustrate how sitting down to translate documentation written in natural language into TLA+ revealed to us some issues that we didn’t even realize we didn’t understand thoroughly! Furthermore the resolution of these issues cannot be found in UMA’s user documentation but only by a close examination of the Solidity source code implementing the Optimistic Oracle. This process sheds light on three important principles which we hope to convince you are reasonable.

  1. A completely unambiguous, mathematically precise description of any decentralized protocol should be made available by the creators.
  2. Examining source code in order to understand an algorithm is an inherently insecure methodology.
  3. A formal specification should be developed before any implementation work begins.

We hope you are intrigued by TLA+ and look forward to feedback that will help shape future articles. Meanwhile see below for references to further information on TLA+.

References:

Lamport, Leslie. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. This is the definitive reference for TLA+, written by the inventor.

Wayne, Hillel. Practical TLA+: Planning Driven Development. This is an excellent introduction to TLA+, though it emphasizes PlusCal, a pseudocode-like language that compiles to TLA+. Also see Wayne’s online tutorial at learntla.com.

Price Discovery and Correlation for ETH/USD & BTC/USD on Three Leading Exchanges

Written by Bryan Williams – Guest Author

This article is a part of a series where we explore recent research by Volatility Group (“Periodicity in Cryptocurrency Volatility and Liquidity”). In this article we look at price discovery and correlation on CEXs vs. DEXs. In future articles we’ll explore patterns of volume and volatility across exchanges.

If I were to ask you for the price of your favorite crypto asset, how would you answer?

You’d probably look up the asset on CoinGecko (CG), CoinMarketCap (CMC), or the exchange you use most often. However, if you were to look at the spot price across many different exchanges you’d most likely find a discrepancy in pricing. This occurs because the “true” or “efficient” price of any asset, crypto or otherwise, isn’t necessarily what is currently being displayed on a single exchange or even the most commonly used sites like CG and CMC.

Now, before you storm off in a huff to loudly type your ire in 280-character segments, give me a chance to explain. Let’s use gas stations as an example.

On your way to work you drive by Gas Station A and see the price of gas at $4.40/gal, but you are running late and decide not to stop. After a long day, you leave to go home and forget to stop and get gas. Your gas light comes on but luckily there is Gas Station B near your house. Your tank is nearly empty, so you pull in and fill up your vehicle at a price of $4.50/gal.

The next day you’re driving by Gas Station B and become crestfallen when you notice that the price of gas is now $4.45/gal! Did the universe itself conspire against you to cheat you out of those five cents per gallon? Well, not really. Chances are the true price of gas was lower than the $4.50 you paid, but since the gas station updates their prices at discrete points in time, there is a separation between the posted price and the true price that occurs between updates at the station. This phenomenon also occurs between any sort of public and private marketplaces. Equity pricing for privately-owned companies only occurs at discrete points in time during valuations when the curtain is pulled back for just a moment, while public company pricing during market hours looks continuous in comparison.

Even so, there are various micro-effects that can prevent a public market from showing “true” pricing for an asset. Impediments such as transaction costs, lack of trading volume, or a lack of demand on one side of a trade can lead to a schism between a listed price on one exchange matching “The Truth” being shown across the others. This aberrant price won’t fall back into place until these and other micro-effects are favorable to do so (i.e. the reward for taking on an incorrect price outweighs the risk). This is typically referred to as an “arbitrage opportunity” in traditional financial parlance. If one is quick enough, you could buy an asset “stuck” at a lower price on one exchange and sell it at the correct price on another, both pocketing the difference between the two as well as allowing the exchange to bump up to the true price.

This idea of arbitrage and price discrepancies are integral to Section 4 of the recent paper “Periodicity in Cryptocurrency Volatility and Liquidity” by Hansen, Kim, and Kimbrough. Specifically, is there any sort of lag in price discovery in crypto assets across popular centralized and decentralized exchanges?

In order to determine this, five combinations of currency pairs and exchanges were examined by the researchers to see if there was any lag in prices across their relationship over time. The five combinations used were:

  • BTC-USDT on Binance
  • ETH-USDT on Binance
  • BTC-USD on Coinbase Pro
  • ETH-USD on Coinbase Pro
  • WETH-USDC on Uniswap V2 — Note: Uniswap V3 launched at the end of the sample period for this research and did not yet have the volume or liquidity to be included.

In order to measure any lag effect on pricing between exchanges, the researchers used a combination of autocorrelation and cross-correlations.

What exactly are autocorrelation and cross-correlation?

Let’s return to the example of the gas stations. Why did Gas Station B lower its prices the next day? There are two obvious reasons why this could have happened. First, the price of gas at Station A could have had an effect on Station B. If more people were going to Station A because it was $0.10 cheaper, Station B would need to update their price to attract customers. When one exchange affects the price of another exchange this is called cross-correlation. Second, the price of gas at Station B influenced the future price at Station B. Pretend that Station A had no effect on Station B (e.g. customers were not willing to drive across town because it was too far). If Station B was still losing business wouldn’t they lower prices? Because of this, Station B’s current price affects its future price. When the price of a time series affects the future price of the same time series it is called autocorrelation. In reality both autocorrelation and cross-correlation probably had an effect on the gas price at Station B.

Continuing with this analogy, suppose the price of gas just increased by 0.05 at your local gas station. The autocorrelations will tell you what price changes you can expect to see on the same gas station in the future. Perhaps, you would expect the price to bounce back shortly after, perhaps you would expect price changes in the same direction for a longer period. The cross correlation tells you what price changes you would expect to see at other gas stations. If your local gas station is simply a “price follower,” then the cross correlations could be zero. On the other hand, if it is a “price leader” it would induce price changes at other gas stations. The cross-correlations tell us how large the price impact will be at other gas stations, and how long it will have an impact. The effect could be nearly instantaneous, or could be long lasting if other gas stations were sluggish at adjusting their prices. Combined, the autocorrelations and the crosscorrelations tell you which gas station best reflects the “fair” price of gas, the price that prices elsewhere have a tendency to converge to.

Here is another example that may help to clarify. Imagine you are on the edge of a perfectly still lake. Next to you is a respectable pile of rocks of various shapes and sizes that roughly averages out to rocks the size and weight of a particularly dense russet potato. You heave one of these rocks into the air and watch it break the surface of the lake with a satisfying SPLOOSH. This rock-tossing has resulted in a ripple effect on the surface of the lake. You wait exactly one minute and repeat the process with another rock. SPLOOSH. There are now two sets of ripples on the surface, one larger than the other. You do this again, and again, and again. By rock N you have a lake surface that is roiling and splashing each which way. How much of that surface activity is due to that first rock? The second one? Rock N?

Autocorrelation and cross-correlation functions are the mathematical equivalent to answering this. In essence, if we recorded the pertinent data from our ripple effect generation experiment, we could run an autocorrelation to let us know how long the lag effect of each rock persists in this environment. In terms of the paper, these ACF/CCF functions tell us how long the price on one exchange exhibits an effect on the price of another exchange. If a significant effect persists for an extended period of time between two exchanges, then it would indicate that the lagging exchange is seeing a slower update of pricing which could be potentially exploited as an arbitrage opportunity.

Autocorrelations and cross-correlations of one-minute returns for the five currency pairs during the sample period of October 1, 2020 at 00:00 UTC to June 1, 2021 at 00:00 UTC. Charts on the diagonal positions of (1,1), (2,2), (3,3), (4,4), (5,5) are autocorrelations. The Y-axis represents the correlation coefficient, which is always bound from (-1,1). If the Y-axis is above 0 there is positive correlation, below 0 there is negative correlation, and at 0 no correlation. The shaded area represents the 95% confidence band (i.e. outside of this band we know with 95% certainty the value is not 0). The X-axis represents delay in minutes. The far right column illustrates that price changes on Uniswap V2 tend to lag price changes on centralized exchanges by as much as 12 minutes.

Take a look at the Figure above. Mathiness aside, what immediately jumps out to your eyes as not being the same as the rest of the figure? The right-most column? The other four columns have pretty much the same shape in their charts minus some minor flux. Both the shape and the y-axis scale for the right-most column diverge dramatically from the rest. This column shows cross-correlations and autocorrelations for WETH-USDC on Uniswap V2. Look at where the line hits the shaded area on the X-axis. This shows that it takes roughly 12 minutes (12 on the X-axis) for prices on Uniswap V2 to no longer be correlated to prices on other exchanges. What does this mean? It indicates that price discovery is primarily taking place on centralized exchanges (Binance, Coinbase Pro) instead of the decentralized exchange (Uniswap V2).

We attribute the staleness in prices on Uniswap V2 to the cost of transacting. The amount that arbitrage must overcome covers both the cost of gas and the 0.3% fee. Furthermore, the liquidity depth of the pool is integral to the amount of slippage which determines if there is enough depth for the arbitrage to overcome the cost of transacting. As DEXs move to Layer 2 we expect the cost of transacting to reduce significantly, vastly improving the price staleness on DEXs.