This paper presents the development of Tula, a tool for video game balancing. The necessity for such a tool is substantiated by the growing requirements for quality and cost-effectiveness in the video game industry, particularly in managing in-game economy and game world logic. The study analyzes existing tools and approaches to game balancing, identifying their limitations, which informed the design of the new tool's functionality. The presented tool integrates features of contemporary solutions while providing enhanced capabilities for game parameter analysis and testing, including prototype generation via class descriptions and real-time simulation. The technological foundation and architecture of the tool are described in detail. Key implementation aspects are discussed: interface responsiveness, continuous data synchronization, and security. Comparative analysis with Machinations revealed advantages in data processing correctness, interface convenience, and prototype modification flexibility.

The paper addresses the problem of visual representation of temporal and probabilistic elements in formal modeling tools for game mechanics. An analysis of existing visual modeling systems – Machinations, Petri nets, UML state diagrams, and UPPAAL – reveals their key limitations in describing complex game scenarios. An approach to visualizing temporal operators and probabilistic constructs in the Tula tool developed by the authors is proposed. A set of visual primitives is described that ensures bidirectional correspondence between visual representation and formal specification in the gameplay specification language. Examples of visual modeling of typical game scenarios with time delays, conditional probabilities, and multiplayer interactions are given. The possibility of automatic transformation of visual models into formal specifications suitable for verification with PRISM and UPPAAL is demonstrated. A comparative analysis of the expressive capabilities of Tula and predecessor systems is conducted, showing that Tula is the only system among those considered that simultaneously provides formally verifiable semantics, built-in support for temporal operators (X, G, F, U), and arbitrary probability distributions, as well as a visual notation organized around resource flows and game events. The two-level specification principle with bidirectional transformation proposed in Tula closes the design–formalization–verification–correction loop, lowering the entry barrier to formal methods for practitioners without loss of verification completeness. This makes it possible to consider Tula as an intermediate layer between iterative game design and industrial verifiers.