FormalZ is a browser-based education game that teachers can use to break the typical monotony in a class on formal method by allowing students to have some fun playing the game, while also learning the basic of writing formal specifications. Unlike existing software engineering themed education games, FormalZ takes a deeper gamification approach, where ’playing’ is given a more central role. After all, what makes games so engaging is not merely the awarded scores and badges, but primarily the experience of playing them. The ultimate research question that intrigues us is whether such an approach will actually make a difference towards the game’s ultimate learning goal. This is still on-going work. Currently, we have a fully functional implementation of FormalZ, but polishing the user interface is still future work. 

Papers and publication

  • Paper: Having Fun in Learning Formal Specifications, by I.S.W.B. Prasetya , Craig Q.H.D. Leek , Orestis Melkonian , Joris ten Tusscher , Jan van Bergen , J.M. Everink, Thomas van der Klis , Rick Meijerink , Roan Oosenbrug , Jelle J. Oostveen , Tijmen van den Pol , Wink M. van Zon. Presented at the 41st International Conference on Software Engineering (ICSE): Software Engineering Education and Training (SEET), 2019.

    Abstract: There are many benefits in providing formal specifications for our software. However, teaching students to do this is not always easy as courses on formal methods are often experienced as dry by students. This paper presents a game called FormalZ that teachers can use to introduce some variation in their class. Students can have some fun in playing the game and, while doing so, also learn the basics of writing formal specifications in the form of pre- and post-conditions. Unlike existing software engineering themed education games such as Pex and Code Defenders, FormalZ takes the deep gamification approach where playing gets a more central role in order to generate more engagement. This short paper presents our work in progress: the first implementation of FormalZ along with the result of a preliminary users’ evaluation. This implementation is functionally complete and tested, but the polishing of its user interface is still future work.

  • FormalZ backend analytics is presented in: IMPRESS: Improving Engagement in Software Engineering Courses Through Gamification, by Tanja EJ Vos, I.S.W.B. Prasetya, Gordon Fraser, Ivan Martinez-Ortiz, Ivan Perez-Colado, Rui Prada, José Rocha, António Rito Silva. Presented at the International Conference on Product-Focused Software Process Improvement (PROFES) 2019.

    Abstract: Software Engineering courses play an important role for preparing students with the right knowledge and attitude for software development in practice. The implication is far reaching, as the quality of the software that we use ultimately depends on the quality of the people that make them. Educating Software Engineering, however, is quite challenging, as the subject is not considered as most exciting by students, while teachers often have to deal with exploding number of students. The EU project IMPRESS seeks to explore the use of gamification in educating software engineering at the university level to improve students’ engagement and hence their appreciation for the taught subjects. This paper presents the project, its objectives, and its current progress.

Teaching how to write formal specifications with FormalZ.


FormalZ is a browser-based game written in JavaScript. However, to be able to be used as a teaching tool it needs to be supported by some backend services, e.g. to allow users to register, to allow teachers to upload “problems”, and to organize users in “class-rooms”. The picture above shows the top-level architecture of FormalZ. The Haskell backend is used to check whether formulas built by users are semantically equivalent to the ones expected by the teacher. In turn, this backend uses the theorem prover Z3 to do the checking.

More on the architecture and various design decisions behind FormalZ can be found in its Design Document , 2018.

Getting it

FormalZ is Free and Open Source. Installer and dockers:

Source code:

  • You can get it from its Github.This will show two repositories: one for the FormalZ game itself, and the other is for its formula checker backend (the Haskell backend in the above picture).
  • UCM’s fork, adapted to ease analytics, integration, and deployment.


First FormalZ, with comentary
Latest FormalZ, no commentary