Catastrophic bugs keep developers from wanting to build DApps, because the risk of losing all the assets in the DApp is terrifying.
MuKn's Glow language will overcome this problem by automatically proving the mathematical correctness of every interaction of a program.
This is the total amount allocated to Glow Formal verification
Abstract: We propose to develop Formal Methods to prove or disprove certain important properties of common classes of Decentralized Apps (DApps) that run on top of the Cardano ecosystem: these properties may establish that it is safe to participate in some interactions, but unsafe to participate in other interactions, because adversaries may follow some strategy that enable them to cheat and win in those latter interactions. So far as we know, no one even attempts to automatically verify these particular important properties, because they fail to consider the adversarial relationship between participants as a fundamental feature of their formal models, often because their formal models are too low-level. This will be a premier feat, that will confirm Cardano as funding the bleeding edge of blockchain technology.
MuKn launched our Glow DSL for DApp development on Cardano's Mantis-EVM side-chain. This project was funded by IOHK and will benefit Cardano in the long run by bringing DApp users and developers to it. IOHK continues to fund front- and back-end development of Glow, but in order for Glow to maximally benefit Cardano, lots of work remains to be done.
One problem that keeps developers from building DApps is the risk of catastrophic bugs. MuKn's Glow language was designed to help overcome this problem by automatically proving the mathematical correctness of every interaction of a program (both user-to-user and user-to-blockchain).
MuKn now has the manpower to implement this formal verification architecture, and can begin building out these features as soon as they are funded.
Thus, with the generous assistance of the Catalyst Fund, MuKn would like to build formal verification into our Glow DSL. With this technology, users will be able to verify that DApps built with Glow are indeed safe before they start using those DApps. Importantly, developers will also be able to detect that some of their DApps are currently incorrect and must be fixed, before those DApps are launched and lose their users' assets.
Formal verification for Glow DApps
We designed Glow so that DApps written in it can automatically prove their correctness with respect to three classes of properties:
We believe we can launch functional formal verification of Glow by December 2021.**
The Glow Language
Glow is a Domain Specific Language (DSL) for Decentralized Applications (DApps). It is developed as an Open Source product by Mutual Knowledge Systems, aka MuKn (pronounced "Moon"). Compared to competing DApp languages, Glow provides much higher-level abstractions that make DApp development drastically simpler and faster, but also portable and amenable to formal verification. With Glow, DApps will be much cheaper and faster to develop and to use, but also, importantly, to audit and to trust.
In Glow, a DApp is an interaction between two or more participants who do not trust each other, exchanging digital assets on decentralized ledgers, using a "smart contract" to automatically enforce the rules of the interaction.
Importantly, a Glow program includes simple annotations about which participant may or must take what actions at each step of the interaction. These restrictions are enforced by the language itself, and it isn't possible for developers to unwittingly omit or reverse a permission check, which already eliminates a vast class of problems with DApps written in Solidity.
While a DApp interaction involves a smart contract, it also importantly involves code that runs "off-chain" on each of the mutually distrusting participants' machines. The more work is off-loaded off-chain, the cheaper the DApp can be, but the harder it is to assess that the contract still holds the participants mutually accountable. Glow generates not just a "smart contract", but also client code that will run on the local machines of participants for each role involved in the interaction. This ensures that there is never a discrepancy between the contract and the client code.
Finally, Glow is designed around a logical model that abstracts at a much higher level than other DApp languages, which enables it to automatically handle the chaining of sequences of transactions by alternative users, with timeouts and loss of collateral for users who fail to act within contractually mandated time limits. In the near future, Glow will be able to automatically insert the escrow of sufficient collateral to align the interests of all parties toward cooperating to the completion of the interaction into any DApp. Glow currently emits code in "direct style" that closely matches the style in which humans write DApps today; but soon it will also be able to emit code in "generalized state channel style", that allows for scalable private contracts. The complexity of implementing this style correctly by hand makes it critical that the Glow compiler generates not just the "smart contract" for a DApp, but also matching client and server code.
Glow has already been launched on Cardano's Mantis EVM side-chain, and is currently funded by IOHK to develop a new UI, more supported smart contracts, and a compiler.
We at MuKn (or more formally, Mutual Knowledge Systems, Inc.) envision a world where everyone uses blockchains for commercial and financial transactions. In this world, simple auditable DApps maximize how much users can trust the system while minimizing how much they need to trust other users. And our Glow language helps make DApps orders of magnitude simpler and more auditable.
François-René Rideau: Co-Founder, has been making programming languages and distributed systems usable for 25 years. Alumnus of the École Normale Supérieure, Former Senior Engineer at ITA Software, he also worked at Google and Bridgewater Associates. While working in the industry, he notably maintained and rewrote ASDF, the build system at the heart of the Common Lisp open source community; he also kept publishing academic papers and speaking at programming language conferences. Early in his career, he even proved in Coq the correctness of a (centralized) payment protocol, which held up in court! Eventually, his interests in economics and software security converged with his experience in open source software and formal methods and he started working on Layer 2 solutions for the Blockchain. Since January 2018, he has made plenty of mistakes as co-founder of startups, and learned the hard way to become his own CEO. linkedin.com/in/fahree
Alexander Smart: Co-Founder, has always thought fast, but learned to think deep and sharp at UChicago. After studying law at Pepperdine, he spent nearly fifteen years guiding executives and decision makers through litigation, in matters ranging from shoplifting and speeding tickets to multi-forum international investment bank disputes. His practice honed his ability to quickly assimilate and master new information, and deliver that information clearly at any level of sophistication. Tiring of courthouses, he found his skills were readily applicable and desperately needed in the blockchain space. linkedin.com/in/alexandersmart
Gauthier Lamothe: Co-Founder, with an atypical background. Trained both as a psychotherapist and in the field of medias and marketing
Alexander Knauth: Junior developer, has already co-authored two notable papers, and contributed to the Racket ecosystem. His previous work on combining types and macros is directly relevant to building our compiler. github.com/AlexKnauth
Drew Crampsie: Drew Crampsie is an independent systems developer with over 20 years of experience in designing, implementing and maintaining Internet based applications and servers with a focus on "bleeding edge" Web Apps.
Drew is a seasoned user in non-mainstream languages and tech to bring useful IT Systems to his clients. https://github.com/drewc
Emeka Nwanko: After graduating in 2005 from Nnamdi Azikiwe University, Emeka Nwanko worked for several companies as a Field Engineer or Operations Manager, such as Schlumberger Nigeria or Northern Oilfield Services and Supplies.
He also worked for Satajanus Nigeria Limited as a software developer in the field of Blockchain industry, both in C# and F#, but also in Rust and Solidity. He also offers free programming classes as a teacher.
Appendix A: Verifying DApp Safety is here:
Keywords: Catalyst Fund, Cardano, DApps, Domain-Specific Language, smart contracts, client code, formal verification, theorem-proving, Z3, adversarial interactions, game theory, Plutus, Haskell, Glow, end-point projection, code extraction, portability.
MuKn built the Glow language, and our CEO was one of the first to formally verify the correctness of a payment system that held up in court.