A clearer view of contract behaviour
From source code to formal confidence.
Solidity2CPN is a web application that automatically translates Solidity contracts into equivalent Coloured Petri Net models, then uses model checking to explore every reachable behaviour.
It helps teams find vulnerabilities such as reentrancy before deployment — without requiring prior knowledge of Petri nets or formal methods.
Formal depth,
practical interface.
Exhaustive model checking runs behind a web interface designed for developers, not formal-methods specialists.
Launch the verifierTrace every state
Explore contract behaviour beyond the paths reached by conventional tests.
Open by design
GPL-3 licensed and built from peer-reviewed research.
View sourceThe workflow
Three steps. One safer contract.
Submit
Paste or upload the Solidity source code you want to analyse.
Translate
The contract becomes a CPN model that captures its execution semantics.
Verify
Model checking explores reachable states and reports unsafe behaviour.
Grounded in research
Peer-reviewed methods.
Developer-ready tooling.
Developed at LIPN, Paris 13 University, Solidity2CPN builds on a series of publications covering smart-contract translation, business-process context, and vulnerability detection.
Browse the publications