Things I learned while programming as a Petri-net maximalist.

With the increasing popularity of blockchain technology and the adoption of smart contracts, ensuring the correctness and security of these contracts has become crucial. Traditional software development methodologies may not be sufficient to address the unique challenges posed by smart contracts. In this blog post, we will explore how a model-driven approach, combined with formal methods, can provide a powerful framework for validating Solidity smart contracts.

Model-Driven Development and Smart Contracts

Model-driven development (MDD) is an approach that emphasizes the use of models to drive the software development process. In MDD, a model serves as a high-level abstraction of the system being developed, capturing its structure, behavior, and constraints. These models are then transformed into executable code through automated processes.

When applied to smart contract development, MDD can help in creating correct-by-construction contract interfaces. By modeling the contract's behavior and properties using a formalism such as Petri nets, we can leverage formal methods to verify various properties of the contract and ensure its correctness.

Petri Nets and Formal Methods

Petri nets are a mathematical modeling technique used to describe and analyze systems with concurrent processes. They consist of places, transitions, and arcs that represent the flow of tokens between them. Petri nets provide a visual and formal representation of the system's behavior, making them well-suited for modeling smart contracts.

Formal methods, on the other hand, are mathematical techniques used to reason about the correctness and behavior of software systems. They involve formal specification, verification, and validation of properties using rigorous mathematical models. By applying formal methods to smart contracts modeled using Petri nets, we can formally verify various properties of the contract, such as safety, liveness, and absence of certain undesirable behaviors.

The Solidity Smart Contract Example

Let's take a look at a Solidity smart contract that demonstrates the application of a model-driven approach using Petri nets and formal methods for contract validation. The contract represents a Tic-Tac-Toe game and includes a metamodeling technique to create a correct-by-construction contract interface.

See the full solidity contract on Github.

In this example, the TicTacToeModel contract represents the Petri net model of the Tic-Tac-Toe game. It inherits from the MetamodelUint8 contract, which provides functions for building the Petri net model using the metamodeling technique. The TicTacToe contract is the actual implementation of the Tic-Tac-Toe game and includes functions for game moves and resetting the game.

Leveraging Formal Methods for Validation

To validate the Tic-Tac-Toe smart contract, we can use formal methods to verify properties such as:

  1. Safety: Ensuring that the game state remains within a set of desired states and that certain conditions are never violated.

  2. Liveness: Ensuring that the game progresses and eventually reaches a terminal state (win, draw, or loss).

  3. Role-based Access: Verifying that the players' moves are restricted to their respective turns and roles.

By formally specifying these properties and applying model-checking techniques, we can automatically analyze the Petri net model and verify whether the smart contract satisfies these properties. This provides a high level of confidence in the correctness and security of the contract, minimizing the risk of vulnerabilities and bugs.


In this blog post, we explored how a model-driven approach combined with formal methods can be used to validate Solidity smart contracts. By leveraging Petri nets as a modeling technique and applying formal methods for verification, we can ensure the correctness, safety, and liveness of smart contracts. This approach enhances the trustworthiness of smart contracts and reduces the risk of vulnerabilities and exploits.

As the blockchain ecosystem continues to evolve, adopting rigorous validation techniques like model-driven development and formal methods becomes increasingly important. By embracing these practices, developers can build more reliable and secure smart contracts, driving the widespread adoption of blockchain technology.

Note: The code provided in this blog post is a simplified example for illustrative purposes. When applying a model-driven approach and formal methods to real-world smart contracts, additional considerations and complexities may arise.

Petri nets are a mathematical tool used to model and analyze systems that involve concurrency, synchronization, and resource sharing. They are useful in a variety of fields, including computer science, engineering, and biology.

One way to view Petri nets is to think of them as a way of accounting for the number of possible ways a user can interact with a system over time. Recall that a Petri net consists of a set of places and a set of transitions. Each place represents a resource or state of the system, while each transition represents a change or event that can occur in the system. A Petri net describes the rules for how these changes can occur and how resources can be shared between transitions.

Consider this Petri-Net composed of actions only.

The gamepad model provides a ‘virtual gamepad’ with buttons. Just like a gamepad in the real world, this model doesn’t have a ‘state’ of it’s own, thus this Petri-net also has no places or connections between actions.

Consider a simple move from a Head-to-Head fighting game. When a player is mashing buttons randomly, sometimes you get lucky and construct a combination move. For example an Upper-Cut could be [ Down, Up, A ]

By adding some state to the model, (and transitions and guards) we can refine the Petri-Net to detect our combo move.

In the above diagram, we have declared ‘noop’ i.e. ‘no-operations’ state, and rules to disallow any other buttons that we do not use in this sequence.

Additionally, we add two interstitial states that enforce that we perform the moves in the proper order.

When we use Petri nets for programming, a programmer can represent the program's states in an explicit manner. This allows the developer and users alike to visualize the flow of the program and the dependencies between different parts of the program. By breaking down the program into smaller components, the programmer can better understand the behavior of the system and how different parts of the program interact with each other.

Now let’s consider a more elaborate move sequence: The Konami Code

(NOTE: when playing with two players, we have added […‘select’, ‘start’]

Petri nets provides a way for programmers to decompose the state of a program and reason about its behavior in a structured and systematic way.

For example, we can think about the overall complexity of these two models, by comparing the code used to generate them.

First let’s see our general solution for any string of non-repeating moves:

Now compare with this code written specifically to model the konami code:

The first sequence is much easier to compose, since we need only to string the required moves together. The Konami code essentially has to be composed directly as a ‘program’ itself. The simpler model is easer to compose, and to generalize for all non-repeating sequences.

There is also a trade-off at play: We could compose the Konami code in a similar manner, but we would have to expand the model to have a state for every move in the sequence.


Petri nets can be thought of as a form of programming synthesis because they provide a way to describe a program's behavior without specifying its implementation. Instead of directly writing code, a programmer can use Petri nets to model the system's state and transitions. This can be useful in situations where the programmer needs to quickly prototype or explore different design choices.

By comparing these examples, we have demonstrated that Petri-nets can model deterministic and non-deterministic automata depending on how state is used. Furthermore, we have seen that the more a programmer can refine and constrain models, the less complex, and more general our code can become. Ultimately, there is always a trade-off cost between interoperability, code size, and memory usage. Explicitly modeling these properties gives the programmer a very sharp tool for reasoning about them up front.

See a live-demo of these models, or view the source models on github.