Statebox is developing a technological stack based on a visual programming language. It is focused on modeling and executing processes. The Statebox language is built using a functional programming approach which utilizes, amongst other things, category theory, Petri nets and cryptography. You can learn more on the about page

Statebox is designed to be self-optimizing, open (technology agnostic), adaptive, terminating, error-cognizant, composable, and most distinctivelyâ€”visual.

Petri nets are the natural representation of decentralized computation and concurrency. By utilizing them as program models (models of computation), the entire language is diagrammatic, and this allows one to inspect the flow of the process executed by the program. The user immediately sees and understands the concrete realization of the abstract design by inspecting the visual representation in the form of Petri nets. Aside from Petri nets, most features in Statebox have a diagrammatic counterpart, so the code can be visually debugged at any level. The diagrammatics are guaranteed to be consistent with the underlying code they represent via mathematical results based on category theory.

Functional programming lends itself to preserving mathematical properties when implementing code, especially if described in terms of category theory.

Petri nets are used to glue "functions" together; Petri nets give "protocol" scaffolding; the transitions are then labeled by deterministic functions defining what computation runs as a consequence of firing transitions.

The system is structured as a P2P blockchain: asymmetric encryption is used to manage identity and sign transactions; the state of the system is computed from a transaction log. The entire system is deterministic.

We use state space analysis, type checking of logic programs, dependent typing:

- Proof of process correctness: no deadlock, liveness, etc.
- Proof of function correctness: typechecking, termination guarantee, etc.
- Global proofs: crypto economic equilibria,
- System proofs: compiler and evaluator work as advertised.

Watch Josh Harvey talk about some of these properties during his presentation at the Second Statebox Summit.

There is no real standard for Petri nets. Moreover, Petri nets are not done categorically which is precisely how Statebox is using them. Statebox also uses wiring diagrams of open Petri nets.

Petri nets are the natural generalization of state machines to a concurrent framework. This means that any state machine is also a Petri net, and that the Statebox formalism is at least as powerful as state machines are. Clearly, in addition to this, Statebox performs better in environments where concurrency is needed.

On the other hand, Petri nets share with state machines the property of not being Turing-complete, a fact that should be considered an advantage in environments where correctness is paramount: non-Turing completeness ensures program termination and makes possible to prove a series of desiderable properties for software to have. Check the monograph for more information about this.

No. Statebox nets can be compiled directly to Javascript or other frontend languages, and the language is hence very responsive. Moreover, Statebox allows for generating UI interfaces directly from backend content, ensuring correctness.

We are gradually opensourcing. A Statebox studio will be available soon. It allows one to click through a process, examine the types of transitions and places, automatically generate forms for different data types, inspect the history of fired transitions and more.

The most popular tool to draft business processes is BPMN (Business Process Model and Notation). There is a straightforward translation from BPMN processes to Petri nets, so everything that can be modeled using former can surely be modeled in our framework with the latter. Moreover, Petri nets offer several advantages over BPMN, the main one being that Petri nets are very well formally defined, while BPMN consists of different standards often incompatibile between each other.

Petri nets are an excellent tool to model complex processes, therefore they are not the best choice when applications are very simple process-wise. For example, a typical ERC20 token contract constitutes a very simple process, and albeit it can be formalized in Statebox, this would be overkill.