Decentralized systems and blockchain solutions are the main points of our focus. We are the developers of program systems based on a blockchain platform and we provide the scientific expertise in verification, evaluation, cybersecurity analysis and testing of blockchain solutions including smart-contracts and token economy models. Here below our possibilities and examples of successful application. 

Analysis of consensus protocol.

We provide formalization and verification of consensus protocols. We use the symbolic modeling approach for investigating a protocol's behavior by checking the reachability of the specific states and properties. This approach allows the finding of weaknesses and thresholds, performing research and improvement of the consensus protocols behavior before going live.

Our success history is the Pandora, Oroborus consensus protocols, and also Proof Of Prestige approach. We did the algebraic models of protocols and detect the possibility of the protocol to attacks resistance with an evaluation of attack probability. We considered the possibility and probability of double-spending, Sybille, and many other types of attacks.

Here the example of Proof of Stake formalization and double-spending attack analysis.

Evaluation of Smart-Contract attack resistance.

We generate the algebraic model from Solidity (or other smart-contract languages) the algebraic model and analyze it for resistance to different attacks like re-entrancy and many others.

Token economy analysis

Decentralization and the token economy sound downright charming before you start thinking about their real application. Don't get all bent out of shape about it, we know about how to simulate and validate your vision.  Being an experienced cyber-economists, we ‘ve realized some projects with evaluation and prediction of token behavior.

Here the example of token economy formalization and analysis in the project “Skilonomy”.

Model-based testing of blockchain platforms is a challenge for testers of a decentralized system. We propose an algebraic approach in model-based testing with using of the algebra of behavior properties. Here is the presentation in UCAAT conference.