# A Reasoning Engine for the Gamification of Loop-Invariant Discovery

arXiv: https://arxiv.org/abs/2109.01121 · HTML: https://mlsanity.com/paper/2109.01121/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 25 references that are in the map.
- First posted on arXiv 2 Sep 2021.

## Builds on (most cited first, 2 of 2)

- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Data Definitions in the ACL2 Sedan](https://mlsanity.com/paper/1406.1557/) (2014)

## Abstract (arXiv)

We describe the design and implementation of a reasoning engine that facilitates the gamification of loop-invariant discovery. Our reasoning engine enables students, computational agents and regular software engineers with no formal methods expertise to collaboratively prove interesting theorems about simple programs using browser-based, online games. Within an hour, players are able to specify and verify properties of programs that are beyond the capabilities of fully-automated tools. The hour limit includes the time for setting up the system, completing a short tutorial explaining game play and reasoning about simple imperative programs. Players are never required to understand formal proofs; they only provide insights by proposing invariants. The reasoning engine is responsible for managing and evaluating the proposed invariants, as well as generating actionable feedback.