Platform for Modeling, Formal Verification and Testing of Distributed  Systems Behavior and Cybersecurity Research

Our consulting team has over a combined-20-years-of-experience in industrial formal verification, algebraic modeling, cybersecurity, and model-based testing


Web based Garuda AI Platform


Areas of Application

Cybersecurity Research

Live demo is coming soon...

The algebraic approach allows one to detect vulnerabilities in the code and recognize attacker behavior in suspicious processes more efficiently than traditional heuristic and searching methods. Symbolic modeling and a new method of algebraic matching increase the accuracy of detection, minimize false positives, and dramatically speed-up the security verification process.

Consensus Protocols Modeling

Live demo is coming soon...

Garuda AI provides the service of 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 for finding weaknesses and thresholds, performing research and improvement of the consensus protocols behavior before going live.

Crypto Economics Modeling

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, Garuda AI knows about how to simulate and validate your vision.

Smart Contracts Validation

Live demo is coming soon...

We know how hard it is to improve or fix bugs in Smart Contracts after already deploying them to the network. Many companies and their users have suffered immeasurable losses due to the poor quality and weak security of their Smart Contracts. Garuda AI knows how to formalize and validate your contract on different levels of abstraction. We can consider and verify its internal behavior, external interaction with the consensus environment, as well as check it for known security issues.

Model-based Testing

Live demo is coming soon...

Model-based testing implies usage of a model of requirements, or design, for testing of the developed product. The model can be the source of the test suit that can be executed in a testing environment. Symbolic technology allows for reaching the maximum demanded coverage of code lines and values of variables, by use of parallel execution of models and software products.

Cryptography consulting

Open publications and papers are coming soon...

We provide consulting on various cryptography methods and approaches, including multi-party computation, secret sharing, zero-knowledge proofs, homomorphic encryption, and more.


Garuda AI Platform

We have accumulated years of experience in the development of formal verification systems to build a unique platform for simulation and validation of system behavior. The Garuda AI Platform consists of the following components:

Algebraic Programming System (APS)

APS was developed by the Glushkov Institute of Cybernetics of the National Academy of Science of Ukraine. It was the first system of term rewriting which used the systems of rewriting rules and rewriting strategies separately. The main goal of APS is to create an algebraic program that solves mathematical problems. The algorithms are designed in APLAN language. This language allows for creating a system of rewriting rules that is the main technique of symbolic computations, especially formula transformations. APS supports powerful mechanisms of formula processing. The system of recursive data structure CLEW has a very powerful and flexible library. It is the basis of the APLAN language.
There are many algebraic solutions in the library of APS. Boolean logic calculus contains all axioms, operations, and relations. The rewriting system can simplify Boolean expressions and create Disjunctive (Conjunctive) Normal Form. A Proving System is also part of APS. It is possible to prove some trueness of a formula in a theory if the axioms and relation are given. A  Solving System can resolve the equations in some theories. These are the following theories that are implemented in APS: enumerated types theory, Boolean logic, linear arithmetic, float arithmetic, string solving, and more.


Clients and Partners


GEO Protocol

The GEO protocol for decentralized P2P network allows participants to exchange assets, connecting crypto and inherited wealth.


Pandora Boxchain

Pandora Boxchain aims to create a world of decentralized artificial intelligence in the same manner Bitcoin has created a world of decentralized payments and Ethereum — a world of decentralized computers.



Talent management and skill monetization platform

The Team

Our R&D Team has over 20-years experience in formal methods of verification, cybersecurity, model-based testing and, re-engineering. We have developed several industrial tools and approaches that have been successfully applied in the telecommunication, automotive, networking, microprocessing, military and biological domains for Motorola, Intel, and other world-renowned companies. We are developing the Garuda AI Platform, which will offer the possibility to developers and researchers to apply our methods and techniques to their own products.


Viktor Radchenko


Dr. Oleksandr Letychevskyi

Chief Research Officer

Dr. Volodymyr Peschanenko

Chief Software Architect

Sasha Borovik

Legal Сounsel | Business and Partnership Development

Alexey Hodkov


Ruslan Shevchenko

Lead Researcher

Victor Yakovlev

Lead Researcher

Andriy Donchenko

Lead Researcher

Maxim Poltoratskiy


Yuliia Tarasich


Yaroslav Hryniuk



Prof. Volodymyr G. Skobelev

Member of the National Academy of Sciences of Ukraine. Areas of expertise: algebraic theory of automata, applied theory of algorithms, mathematical foundations of cryptography and quantum computing.


Prof. Alexander Letichevsky 

1935 - 2019

Words cannot describe how blessed we are to be among those that were inspired during the time of scientists and teacher like you. Your boldness and selflessness will always guide us. Farewell!

Head of Department of Glushkov Institute of Cybernetics National Academy of Sciences of Ukraine, Member of the National Academy of Sciences of Ukraine. Under his leadership, the APS and IMS systems have been developed
Garuda AI Adviser and Friend.


Contact Us

Thanks for your interest in our research. Get in touch with us if you have any questions or comments regarding our work and verification services. We’d love to hear from you.

Het Poortgebouw, Beech Avenue 54-62, Schiphol, 1119 PW, Netherland

+38 068 991 09 25


©2019 by Garuda AI. Proudly created with