Formal Methods: Correctness in Blockchain Design

Formal methods use mathematical processes to pinpoint and test the components of a system, and the functionality of each of them. This means that more effort, time and money must be spent ensuring correct contracts ahead of time, and this has inhibited the popularity of smart contracts in many industries. MuKn helps DApp developers to achieve this by using formal methods.

The topic of formal methods can be further divided into the following 2 major subtopics:

Formal specification: A process used to define the functionality of a system’s components

Formal verification:  A process used to prove or disprove the correctness of the functionality of the algorithms that make up a system

Formal methods for the blockchain

Multiple hacks continue to hit the blockchain and decentralized applications.

Smart contracts have stricter security requirements than many other types of programs. There is often real money at stake, and the immutable nature of the blockchain can make it difficult to upgrade code after deployment.

Securing  can be achieved by properly defining each component from the start of the system’s design and continuously proving their absence throughout their development.

Formal verification does just that, adding mathematical proofing rigor to the “shift left” concept, commonly associated with the DevSecOps movement.

MuKn Offerings

Mutual Knowledge Systems (MuKn) offers formal verification consulting services.

Our implementation of formal verification allows developers to ask: does the business logic of our contract really make sense? In particular:

• Am I really implementing what I intended to?
• Can I guarantee that each participant will be always able to do what was specified?
• Am I sure that all participants won’t be able to trigger any undesirable outcome?
• Am I sure we don’t accidentally transfer funds to the wrong account?
• Am I sure that the amounts transferred between accounts is fair?

Design principles of Glow, our domain specific programming language for decentralized applications clearly define functionality, such as:

• Cryptographic specification
• Tracking of accounts, balances and transactions, and confirmation of their proper execution

References / Further Reading

• Glow Whitepaper
• Glow GitHub wiki

[/vc_column_text][/vc_column][/vc_row]