Formal Verification Reveals Optimal Strategy in Board Game Caverna

In an impressive demonstration of applying formal methods to game theory, a researcher has mathematically proven the optimal strategy for the popular board game Caverna. By formalizing the entire game in the Lean 4 proof assistant and constructing a labeled transition system (LTS) model, the author has demonstrated that a "furnishing rush" strategy is the unique weakly dominant pure strategy across all possible game configurations.

The Formalization Approach

The project represents a substantial technical achievement, comprising approximately 3,000 lines of Lean 4 code spread across 19 modules. Eleven definition files model the complete game mechanics—including all 24 action spaces, 48 unique furnishing tiles, the expedition loot system, board geometry, harvest schedule, and scoring formula—while eight theorem files contain 176 machine-checked proofs.

The model covers all 2,880 possible 2-player game setups (144 card orderings multiplied by 20 harvest marker placements), providing comprehensive coverage of the game state space. The formalization treats Caverna as a finite deterministic perfect-information system, which naturally lends itself to formal verification techniques.

Labeled Transition Systems and Game Rules

The core of the formalization models Caverna as a labeled transition system (LTS)—a mathematical structure consisting of states, actions, and transitions. In this formalization:

• States represent complete game configurations (round number, phase, both players' inventories, board layouts, etc.)
• Actions correspond to dwarf placements and harvest events
• The transition relation encodes the complete rulebook

This approach allows the researcher to prove properties hold on all reachable game states without enumerating them explicitly. The LTS formalization captures every legal move sequence across all possible setups, including sequences no human would ever play, providing stronger guarantees than testing alone.

Strategic Analysis and Dominance Proof

Through careful analysis of the formalized game, the researcher identified eight distinct strategy archetypes that represent coherent approaches to the game:

1. Furnishing Rush
2. Weapon Rush
3. Animal Husbandry
4. Mining Heavy
5. Balanced
6. Peaceful Farming
7. Ruby Economy
8. Peaceful Cave Engine

The payoff matrix, derived from the formalized game rules rather than simulation or guesswork, reveals that furnishing rush is weakly dominant. This means that for any opponent strategy and any alternative strategy, the furnishing rush payoff is greater than or equal to the alternative.

The formal proof of this dominance relation is remarkably straightforward—Lean's kernel checks all 64 cells of the payoff matrix, confirming that furnishing rush achieves the column maximum everywhere. This mathematical certainty eliminates any need to trust the researcher's arithmetic or strategic intuition.

The Prisoner's Dilemma Structure

The analysis reveals a fascinating game-theoretic structure: while furnishing rush is the optimal individual strategy, when both players adopt it, the outcome is suboptimal from a collective perspective. This creates a prisoner's dilemma:

• Both players score 85 points in the Nash equilibrium (both playing furnishing rush)
• If they could coordinate on different strategies, combined welfare would reach 210 points
• The price of anarchy is approximately 19% (210/170)

This means that while both players would prefer the other to play something different, neither can unilaterally deviate without making themselves worse off. The result is a situation where rational self-interest leads to a collectively inferior outcome.

Technical Innovations in Formalization

The formalization incorporates several elegant technical approaches:

1. Refinement Types: Making illegal states unrepresentable through dependent types. For example, the Weapon structure carries proof that its strength is between 1 and 14, eliminating the possibility of invalid weapon values.

2. Complete Rulebook Encoding: The entire Caverna rulebook is captured in approximately 250 lines of Lean, with a 160-line applyPlacement function handling all 24 action spaces.

3. Closed Transition Relations: The formalization explicitly defines all legal transitions, with any action not explicitly listed being illegal (represented by | _, _ => False).

Implications for Game Design

The analysis reveals an interesting insight about game design: Caverna's dominant strategy comes with a 19% welfare tax on mirror matchups, which paradoxically makes the game more interesting. When opponents deviate from the dominant strategy, the game becomes more engaging, explaining why players don't always follow the optimal strategy in practice.

This suggests that good game design can be robust to being solved—a game with a trivially dominant strategy would be boring, but Caverna's structure maintains interest despite having a provably optimal strategy.

Limitations and Future Work

The researcher acknowledges limitations in their approach:

• The payoff matrix entries are estimates derived from formalized game rules rather than exhaustive search
• The 3+ player variants remain unanalyzed and likely have different strategic structures
• The exact sequence of dwarf placements for each specific setup hasn't been computed

The formalization code, built on Lean 4 v4.28.0 with Mathlib, is available for further verification and extension. The analysis represents a compelling example of how formal methods can provide deep insights into game theory and strategy.

The study demonstrates that even seemingly complex games like Caverna can be subjected to rigorous mathematical analysis, revealing elegant structural properties that might not be apparent through casual play. The prisoner's dilemma structure that emerges from the optimal strategy analysis adds an intriguing meta-layer to the game's strategic depth.