Unverified smart contracts may contain errors, with catastrophic consequences, such as data leaks, loss of assets, hacks, among other problems.

According to Immunefi, there are losses at DeFi for about USD 10 billion, which is about 10% of TVL (Total Value Locked) at this moment (DeFi Pulse).

Smart contracts have much stricter security requirements than many other programs, real money is at stake, and the immutable nature of the blockchain can make it difficult to update code after implementation. This means that more effort, time and money must be invested to ensure correct contracts upfront, and this has inhibited the popularity of smart contracts in many industries.

MuKn’s solution to this problem was to build Glow is a Domain Specific Language (DSL) for developing secure decentralized applications (DApps) on the blockchain. 

Glow’s logic is designed to deal with the inherently adversarial aspect of DApps that existing formal tools overlook, self-verification in the code structure. Behind Glow is an architecture that in the future will allow the correctness of Glow itself to be demonstrated, and may later become a full DApp operating system.

The initial version of Glow was released on Cardano KEVM in February 2021, with first-class abstractions for accounts, participants in an interaction, and crypto operations. 

You can read my article about another proposal for Glow, in this FUND7: Glow Implementation to the Plutus Application Backend. 

The Proposal

Although Glow has many built-in security features, for example, accounts need to be balanced, escrow is automatically released in the waiting time, among other functionalities, its security can be substantially increased if the contract developer establishes propositions that should be true for the program as a whole (e.g. there must be a winner of a game, all participants must come up with some statement, etc.), encode them as statements in a metalanguage (a statement of statement), and prove or disprove them automatically. This process is known as formal verification.

To do this, it lets developers ask themselves: does the business logic of the contract really make sense? 

In particular it leads them to wonder:

• Am I really implementing what I intended?
• Can I guarantee that each participant will always be able to do what was specified?
• Am I sure that all participants will not be able to trigger some unwanted result?
• Am I sure we didn’t accidentally transfer funds to the wrong account?
• Am I sure the amounts transferred between accounts are correct?

They have launched development of the formal verification engine for Glow with the help of voters, in the Catalyst FUND5, and now there is a functional proof of concept. 

After testing several different versions of assertion syntax and semantics, and with the initial implementation in place, the team decided that it is time to begin the next stage of the project. This phase will expand the capabilities of the formal verification engine, introduce a new tool for Glow developers, and employ state-of-the-art formal verification techniques to ensure the accuracy of critical parts of the formal Glow verification engine.

This proposal will make formal verification tools more available for teams of all sizes, with a formal verification engine for the Glow language, which allows automatic verification of the claims provided by the programmer.

The Glow code and the formal verification engine code are licensed by Apache 2. 

Roadmap

The team plans to deliver the work that will take three months for this proposal.

Glow programmers will be able to express important properties of the contract within the source code of the Glow program.

They will be able to add special lines to their code, describing directly the desired and unwanted results of the contract, and the Glow compiler will make sure that the program always runs accordingly.

If the formal verification engine detects an inconsistency during compilation, the compilation process will be interrupted, preventing the developer from compiling and implementing a faulty contract. In that case, a human readable output will be produced to help the developer address the issue.

A functional proof of concept of this system, capable of automated assertion verifications, was implemented with the help of a grant from Catalyst Fund 5. With the funds from this grant from Catalyst Fund 7, production-ready deployments can be shipped and a formal verification of some of its key parts.

The system uses the Z3 Theorem Prover to produce tests on the statements generated by our compiler. Some models and metamodels will be written in the Agda test wizard dependent language. The use of these components allows integration with third-party development tools and even independent implementation of the Glow compiler.

The grant also applies to the formalization of the Glow Language specification. This will be an important step along the way to demonstrate the accuracy of the implementation in the future.

The Future

In the next steps, not funded by this current proposal, they estimate that after about six months, they will be able to deliver expanded scope of verifiable Glow programs and claims about them, by integrating additional external tools such as model verifiers. LTL and CTL and the Computer Algebra System.

Since the model is well suited to future modifications, one of the key goals will be to express claims about the randomness and basic properties of cryptographic functions.

In the long term, they plan to implement an automated economic analysis of the contracts.

The team has already started planning future steps: Applying Formal Methods to the Glow ecosystem

Budget

The development team budgets that this work requires the expertise of a Senior Architect, Senior Support Engineer, and Junior Support Engineer. whose combined cost is USD 25,333 per month, for a total of three months.

The requested funds total USD 76,000.

The Team

One day, three game-theory enthusiasts with very different backgrounds decided to found a company around one main topic: TRUST.

A seasoned developer, a lawyer and litigator, and a communications expert joined their effort to build the Internet of tomorrow by developing avant-garde tools, both philosophically and technically.

Mutual Knowledge Systems also has its advisors, junior developers and other team-members. You can meet the team.

Mutual Knowledge Systems, Inc. is a company whose mission is to evolve a new decentralized Internet, developing tools on programming languages, with formal methods and distributed systems. This gives a unique advantage to write, audit or rewrite applications, so that they remain intact under attack.

The company has built Glow on Cardano testnet’s KEVM, with a proof of concept for the PAB.

GitHub https://github.com/Glow-Lang/glow 
You can see the proposal in Ideascale.