Hard Fork Alonzo introduced the Plutus language for smart contract programming, and numerous DApps began to be developed in Cardano.
This is not surprising, given the rich features offered by the blockchain’s eUTxO ledger, and Ouroboros consensus mechanism, with atomic transactions, predictable fees, and the potential to mathematically verify a smart contract design in a deterministic way.
Cardano was designed to run secure smart contracts, with a functional programming architecture, based on Plutus. However, testing, auditing, and even designing DApps on Cardano comes with serious challenges.
Smart contracts within Cardano consist of scripts that control how transactions can consume eUTxOs, pieces of value associated with metadata.
Unlike the global nature of smart contracts on Ethereum (EVM), a Cardano script can only perform local inspection of the consuming transaction. This means that the implementation of a contract is often divorced from the desired semantics of its operation.
These characteristics of Cardano make it suitable for supporting mission-critical applications, such as DeFi DApps, that secure millions of dollars worth of value. However, this same unique design also presents key challenges for developers. Testing, auditing, and even designing Cardano smart contracts is still a complex task, and tools are needed to simplify the process.
The smart contract code can be public and so anyone can invoke endpoints, at any time, to irrevocably change the state of the ledger. This open nature, transparent to users and developers, inadvertently creates massive incentives to exploit poorly designed applications.
An important point of Cardano is that its core language, and its smart contract language, are amenable to formal verification. This means that smart contracts can be, more or less, mathematically proven to be safe.
It is also helpful to remember that Cardano’s multi-asset ledger lends itself to a wide range of use cases for tokens compared to single-asset ledgers like Ethereum. Developers will be able to use the specification to outline the properties and legal state transitions that govern their applications.
That specification can then be translated into program code that can be tested for behavior as expected on the encoded properties using the specification language. For properly designed smart contracts, users will have a high degree of assurance that the DApps, with which they interact, behave as intended.
Plutus and the Cardano blockchain obviously support a wide variety of use cases. This is easily seen in the current DApp ecosystem. Because of this, there are some difficulties in designing a Domain Specific Language (DSL) that sufficiently covers this wide range of use cases, and incorporates ‘end-case’ protocol designs.
Just as important, the proposal for a DSL will streamline DApp designs and generate tests to ensure the implementation works as intended. This will drastically reduce auditor and developer time, significantly reducing costs.
The Proposal
The proposal is the construction of a Domain Specific Language (DSL), to formally describe the behavior of the DApp, and generate tests to validate an implementation against its design.
The goal is to create an integrated DSL, in which the semantics of a DApp system as a whole can be described from an inter-transaction perspective rather than an intra-transaction perspective.
More specifically, the DSL is a way of specifying transactions (for example, changes in ledger status) and combinations of transactions, as well as the conditions under which they must be validated. In general, this involves delineating subsets of transaction types (transaction families), as well as defining how tokens can flow between eUTxO and the sequence of events on which their transfer is based.
Developers will be able to incorporate the DSL throughout the development process. More specifically, the DSL will provide DApp developers building on Cardano with an efficient, high-level way to ensure implementations match their designs.
Developers will be able to use the specification language to:
- reduce costs by reducing developer and auditor time
- build DApps that interact securely with others
- configure the types of value that their smart contracts can handle
- test assertions based on preconditions and postconditions
- employ automated, or human-driven, testing of the application function
- define the types of transactions (families of transactions) that a system can handle
- automate code generation in some cases
- design applications that cannot enter faulty states
- speed up the design of the architecture of a system
- have more confidence in testing
Milestones:
3 months: complete the initial exploratory phase of development and obtain a functional specification language that can be used by advanced users.
6 Months: compare production eUTxO scripts and expand the number of use cases covered by our DSL. They expect to have tested many working dApps throughout development and have several early stage dApps designed and incorporate the product throughout their development process.
12 Months: deliver a fully functional, audited and flexible DSL suitable for specifying any type of project. At the 12-month mark most of the focus will be on exploring “edge cases” and completing the scope of design types supported by the DSL.
The Budget
The total funds requested is USD 72,000, and will be applied to 900 hours of engineering.
- Initial Exploration, Notation, and Problem Domain Analysis: 60 hours
- Automated Classification and Delineation of Tx Families: 120 hours
- Design of Generalized Types and Syntax Systems: 120 hours
- Integration/Implementation into Current dApp Ecosystem: 80 hours
- Optimization (e.g. ., fine-tuning data structure traversals): 80 hours
- Documentation and Training Materials: 40 hours
- General Testing: 80 hours
- Audit Preparation: 80 hours
- Specifications: 80 hours
- Change Budget: 160 hours
The Team
MLabs has quickly become one of the leading companies in development in the Cardano ecosystem.
They have one of the largest groups of PureScript/Haskell/Plutus developers in the community. They are IOG Plutus partners and regularly work with IOG to develop the Cardano blockchain and ecosystem, employing more than 80 developers, the company tells us. You can see the core members of the full team here.
The development team advertises itself as follows:
Compilers and Formal Methods
Las Safin is a software engineer and formal methods specialist with experience in dependent scripting languages like Idris and Agda and is interested in Cedille. At MLabs, he helps manage Nix environments for use in development and writes compiler and application specifications.
He has also made significant contributions to Cardano tools. In particular, he is the creator of Plutarch. Plutarch is an eDSL written in Haskell for writing efficient Plutus Core validators. Plutarch significantly reduces the resource demands of validators written in eDSL while giving developers more granular control of the generated Plutus Core.
Plutarch: https://github.com/Plutonomicon/plutarch
GitHub: https://github.com/L-as
Ecosystem and Formal Methods
Maksymilian Brodowicz does a lot of research, both technical and product, financial, and related to user experience. Specifying and innovating protocols, his designs have been used in a variety of efforts.
Formal education in math and computer science, HoTT enthusiast and Haskell practitioner of five years.
Delivery Manager
George Flerovski manages a portfolio of projects at MLabs including decentralized exchanges, governance, auctions, performance optimization, and on-chain analytics. He completed his Master of Arts in Economics in 2017 and has five years of professional experience in data science and engineering. Prior to joining MLabs, George was involved in designing the streaming merge algorithm for concurrency on the Cardax decentralized exchange.
George has developed and loved Haskell since 2015, and has been involved with Cardano since 2018. He has carefully studied Cardano’s research papers and specifications, developing a deep understanding of the Cardano consensus protocol, smart contract framework, and network stack. He participated in the first cohort of the Plutus Pioneers Program in the summer of 2021 and was an active contributor to the Alonzo Blue, White and Purple testnets.
GitHub: https://github.com/GeorgeFlerovsky
Formal Methods
Maciej Bendkowski completed his Ph.D. in 2017 in the Theoretical Computer Science group at the Jagiellonian University in Krakow, Poland. His research interests include lambda calculus, formal verification, and random generation of large combinatorial structures. He is the author or co-author of 15 peer-reviewed research articles in theoretical and combinatorial computing. Throughout his career, Maciej has focused on finding practical applications for his theoretical findings. His recent projects include a Haskell-based combinatorial sample compiler that implements Boltzmann’s idea of multiparameter samples.
GitHub: https://github.com/maciej-bendkowski
Compilers and Formal Methods
Fraser Dunlop is a software engineer with experience developing Haskell and designing compilers for constraint modeling languages. At MLabs he has developed specification tools to generate property test suites from formal specifications.
Github: https://github.com/delicious-lemon
Formal Methods
Peter Dragos has a BA in Mathematics from the University of Rochester. His professional interests include applied category theory, fundamental mathematics, and the modeling of political and economic systems.
https://github.com/peter-mlabs
…
You can read the original proposal on IdeaScale: MLabs – Spec DSL for dApp Security
