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.
Introduction
Context
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:

1. System invariants: The DApp always keeps all inputs and outputs balanced at all times, never involving negative amounts, and never leaving assets unaccounted for.
2. Adversarial Safety: It is an optimal strategy for each participant to follow the protocol. No participant may gain an advantage by straying, defecting, or trying to cheat—they may only timeout and lose their collateral. Meanwhile, no matter how badly the other participants behave or fail to behave, participants who do follow the protocol may collect that forfeited collateral, and are otherwise guaranteed not to lose anything beyond the bounded transaction fees.. These properties establish the safety of the interaction, on the assumption that each participant has a suitable initial valuation of each asset, and that volatility remains within their predicted range.
3. User-defined: Any DApp-dependent user-defined invariant is specified in a suitable modal logic that covers the relevant aspects of concurrent temporal logic, epistemic logic, linear logic, game semantics, and game theory. For instance, a zero-sum gamble may include an invariant according to which neither participant has a winning strategy, and that given suitable convex respective utility functions, both participants may a priori gain in participating. A derivatives product might include an invariant according to which, within some suitable economic and technical hypotheses, the strike price enforced by the contract will remain close enough to some formula valid outside the contract.
   MuKn broadly understands how to implement this formal verification: we first wrote the theory of it, and our previous prototype automatically verified some of these properties. Unhappily, that codebase has grown stale and no longer matches the current version of Glow.
   The goal of this project would be to implement a new formal verification tool that closely matches the current version of Glow and can be easily amended as Glow itself is extended. Emphasis will be given to the adversarial safety properties, since they are what guarantee the safety of a DApp in an adversarial environment, and are not studied by any of our competitors.
   We believe that it is important that our tool can automatically prove that various "obvious" implementations of a protocol are wrong: for instance, that publishing bets or bids without a commit-reveal protocol in some interactions allows the last person who publishes their data to game the results. Or that omitting some verifications allow some users to cheat. It is not enough to say "yes" to a complete program, the tool must say "no" to most incomplete or incorrect programs.
   No amount of language safety can remove the necessity of having DApp audited by proficient experts. But careful language design and tool automation can greatly improve both the cost and quality of these audits, by making subtle bugs and underhanded code very hard to write, so that auditors can focus on the intent of the DApp and its higher-level, more obvious, issues.
   Budget and Deliverables
   Updating Glow to reimplement these formal verification methods will require funding a full-time research engineer, and enough management overhead to oversee their work. We believe a qualified hire will cost approximately $15k per month, plus another $7.5k per month for two months to create the necessary management overhead and support, including having the compiler team refactor their code to accommodate the needs of formal verification.
   **With a funding of $60,000, we believe we can deliver a minimal proof of concept, limited to handling demo cases, within 3 months. Assuming continued funding, we believe we could have functional formal verification of Glow within 6 months, and complete, externally audited formal verification of the Glow stack within 12 months to verify that no invalid operation is possible, and no valid operation is rendered impossible.

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.
The above features eliminate a large class of issues, and an order of magnitude in the effort required to build a DApp, but also to audit it, compared to developing in Solidity and JavaScript. Developing in Glow is still a factor two times simpler than developing in Plutus and Haskell. And unlike either of the above approaches, it is potentially portable to all blockchains with smart contracts. Glow thus offers the promise of a blockchain ecosystem where DApp functionality is not tied to any single blockchain. In such an ecosystem, technically superior blockchains, like Cardano, will win.
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.
MuKn
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:
https://docs.google.com/document/d/1wBsE-kvWjhOzZOACPJEIO8Df0qLpDBbDXWPbhp0EdFQ/edit?usp=sharing
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.