Design Lessons From Binary Fission: A Crowd Sourced Game for Precondition Discovery

Binary Fission is a crowdsourced formal verification game developed at UC Santa Cruz to address a fundamental scalability problem: there are far too few human formal-methods experts to verify the millions of programs that could benefit from it. The game asks players to discover program preconditions by sorting "quarks," colored blue for good program states and orange for bad, using filters that act as logical predicates. The resulting decision trees yield candidate invariants, which are then checked by the CBMC model checker. The central thesis is that non-experts can meaningfully contribute to formal verification when the underlying reasoning is abstracted into accessible, point-and-click mechanics.

The evaluation provides the most substantive findings. Among 972 players who produced 2,963 solutions, 191 of 3,108 player-created clauses qualified as usable function preconditions. For seven TCAS functions, the player-discovered preconditions accepted between 0% and 53.7% of good test states, indicating considerable variation in how general the resulting conditions were. The authors interpret these results as evidence that the game's abstraction and scoring produced human-readable and reasonably general preconditions, while acknowledging that the outcomes were uneven across functions.

Design features such as the Iris View, which previews in real time how many filters split the quarks, and highlighting strategies based on purity, balance, and utility, were intended to speed decision-making. The work also identifies notable shortcomings. Community engagement remained weak, over-abstraction frustrated some players, and the absence of personal-best tracking limited motivation. Real-time chat failed to build community given the sparse player base, and players requested greater visibility into the underlying mechanics.

Looking forward, the authors propose a refined version with chat, alerts, and improved classification trees, an industrial-strength variant operating on client code, and a suite of linked games forming a closed loop to strengthen invariants over time. The overall conclusion is that the crowd produced novel, legible, and useful invariants, while the retention and engagement results point to design challenges that remain unresolved.