Market
Cardano dApp developers building mission-critical applications such as DeFi protocols.
Problem Space
Numerous dApps began building on Cardano following the introduction of the Plutus smart contract programming language. This is hardly surprising given the rich features offered by the blockchain’s EUTXO ledger and Ouroboros consensus mechanism: atomic transactions, predictable fees, and the potential to mathematically verify a smart contract's design.
These aspects are a natural extension of Cardano’s design which borrows heavily from formal methods. This architecture lends itself to functional programming, which can be noted in Plutus, a smart contract DSL built on Haskell.
These features of Cardano make it suitable for supporting mission-critical applications, such as DeFi dApps securing millions of dollars of value. Yet, this same unique design also presents key challenges to developers. Testing, auditing, and even designing Cardano smart contracts remains challenging, and tools are needed to simplify the process.
A specification language for sound dApp design
Smart contracts within Cardano consist of scripts that control how UTXOs, pieces of value with an associated piece of data (the datum), can be consumed by transactions. Unlike the global nature of smart contracts on Ethereum, a Cardano script can only perform a local inspection of the consuming transaction. This means that the implementation of a contract (i.e., the script) is often divorced from the desired semantics of its operation.
Moreover, it is generally non-trivial to decipher the intention of a smart contract from its raw implementation. This has reaching consequences for a smart contract blockchain like Cardano. Here, all smart contract code is public and endpoints can be evoked by anyone, at any time, to irrevocably change the state of the ledger. This open nature inadvertently creates massive incentives to exploit poorly designed applications.
Our goal is to create a specification language, an embedded DSL, in which we can describe the semantics of a dApp system in its entirety, from an inter-transaction perspective rather than an intra-transaction perspective. More concretely, our specification language consists of a way of specifying transactions (e.g., changes to the state of the ledger) and combinations of transactions as well as the conditions under which they should validate. In general, this involves delineating subsets of transaction types (transaction families) as well as defining the way tokens can flow between UTXOs and the sequence of events upon which their transfer is predicated.
How does formal specification help Cardano?
A major selling point of Cardano is that its core language and smart contract language are amenable to formal verification. This means smart contracts can be, more or less, mathematically proven to be secure. As noted in the Cardano documentation, “specification derived from white papers looks a lot like Haskell code, and connecting the two is considerably easier than doing so with an imperative language.”
It is also useful to recall Cardano's multi-asset ledger lends itself to a wide range of use cases for tokens in comparison to single-asset ledgers such as Ethereum. Developers will be able to use our specification to delineate the properties and legal state transitions that govern their applications.
Such a specification can then be translated to program code which can be tested to behave as intended per the properties encoded using our specification language. For properly designed smart contracts, users will have a high degree of assurance that the dApps they interact with behave as intended and are unable to enter undesirable states where value may be inadvertently lost.
Just as important, however, our DSL will streamline dApp designs and generate tests to ensure an implementation functions as intended. This will dramatically reduce auditor and developer time while significantly reducing costs.
Plutus and the Cardano blockchain obviously support a wide variety of use cases. This is readily seen in the current dApp ecosystem. Because of this, we expect some difficulties designing a DSL that sufficiently covers this wide scope of use cases and incorporates 'edge-case' protocol designs. We expect that improvements will be ongoing.