A raylib RPG game built on formally verified game logic. Every game rule is specified in Quint, tested via Model-Based Testing (MBT), and implemented in Odin.

Inspired by: Model-Based Testing for D&D

Quint Crawl is a turn-based RPG rendered with raylib. Explore a 9x9 world grid (81 zones across 5 difficulty levels), fight enemies, gather resources, craft gear, and level up to conquer the Castle.

just play             # build and run the game

The game logic in quint_crawl/ is the single source of truth — shared by both the raylib game and the MBT test harness. Every state transition is formally specified and verified.

See the HUD sidebar for zone-specific actions.

• World — 9x9 grid, 5 difficulty levels, biome tiling (3x3 pattern repeats across regions), fog of war, HUD minimap, mouse hover tooltips, per-zone weather (Clear/Rain/Fog/Storm) affecting combat/gathering/movement, village waypoints with fast travel, one-time treasure chests with tier-scaled gold rewards.
• Combat — turn-based, stamina-gated actions, 3-hit combo chain with damage multipliers, cooldown abilities (heavy strike, battle cry, fortify, counter-attack), status effects (poison, ATK/DEF buffs) with turn-based ticking, enemy respawn timer (5-turn cooldown after a kill), four weapon types (sword / dagger / battery pistol / staff; weapon_type gates combat actions — sword and dagger share blade-combat paths with per-weapon stamina + attack tuning).
• Bestiary — data-driven catalog of 200 named enemies across 20 archetypes (4 per tier, 5 tiers), 6 trait tags (Undead/Beast/Elemental/Construct/Humanoid/Aberration), trait-keyed secondary loot drops.
• Elemental system — 4-element cycle (Fire > Ice > Lightning > Earth > Fire) with 2x/1x/0.5x damage multipliers.
• Companions — data-driven species catalog (Wolf/Hawk/Turtle/Fox/Bear/Owl/Lynx/Sprite) with biome-gated adoption, trait affinities (Attacker/Defender/Scout/Support), rarity tiers (Common/Rare/Legendary), species-specific perks (HP regen / mana regen / stamina vigor / loyalty bond), loyalty-on-combat loop (inactive below LOW_LOYALTY until fed), in-combat command, village training to raise rarity, and a 3-stage companion quest chain. The spec verifies the abstract (trait × rarity) effect space; Odin grows the catalog freely without code changes.
• Progression — XP/level-up, skill tree with 3 branches (Offense/Defense/Utility), 1 point per level, respec at village, 3 prerequisite-gated quests (Slime Slayer → Venture Forth → Castle Conqueror) tracked in the HUD, Castle Boss encounter gates the final victory claim.
• Items & crafting — resource gathering (wood, iron), level-gated sword crafting (Lv2+, batch-of-3 option), sword durability with village repair, salvage system (upgradeable 1–3), 3-slot weapon enchantment (fire/ice/vampiric/lightning; fire/ice mutually exclusive), venom sac crafting, holy water crafting (holy_dust + wood → out-of-combat full heal), fire scrolls (bypass mana gate), loot drops with pity-counter guarantee, zone-tiered sword rarity drops (Common/Rare/Legendary with ATK scaling), per-tier unique archetype trophies (5 collectible drops that grant a permanent ATK bonus), village recycling (3-for-1 wood/iron/potion conversion), full-screen inventory overlay ([I] to open), inventory capacity (30 items) enforced across gathering/shopping/loot.
• Persistence & polish — save/load snapshot with full state round-trip; post-processing effects (zone tint, chromatic aberration, low-HP pulse, level-up bloom, poison overlay).

specs/*.qnt  ──[quint run --mbt]──▶  traces/*.itf.json  ──[odin test]──▶  pass/fail
                                          │
                 Odin implementation  ◀───┘
                 (*_mbt/*.odin)        replayed against spec expectations

1. Write a Quint spec — state variables, actions (state transitions), invariants (properties that must always hold)
2. Generate traces — Quint explores the state space nondeterministically and records execution traces in ITF (Intermediate Trace Format)
3. Write Odin glue — a step handler (dispatches action names to your code) and a state getter (reads your implementation's state back for comparison)
4. Replay — the MBT runner walks each trace step, mutates your implementation, and checks that every state variable matches the spec's expectation

quint_crawl/           Shared game logic (Game_State, all action procs, constants)
quint_crawl_game/      Raylib game executable (rendering, input, UI, shaders)
  assets/              GLSL shaders (effects.fs)
quint_mbt/             Shared Odin library: ITF parser + trace replayer
quint_crawl_mbt/       MBT harness for the integrated game spec
specs/                 Quint formal specifications
  core/                Character fundamentals (rpg, healing, leveling, stamina)
  combat/              Combat systems (combat, combat_full, status, cooldown, elemental)
  items/               Equipment & crafting (equip, durability, enchantment, crafting, salvage, ...)
  economy/             Trade & loot (shop, dynamic_shop, trade, loot)
  world/               Exploration (world_grid, trap, respawn, companion)
  social/              Progression & social (party, quest, skill_tree, reputation, summoning)
  quint_crawl.qnt      Integrated game spec
mbt/                   Per-module Odin MBT test harnesses (mirroring specs/ layout)
  core/                ...
  combat/              ...
  items/               ...
  economy/             ...
  world/               ...
  social/              ...
traces/                Generated ITF trace files (.itf.json)
docs/                  Design documents (asset specs, etc.)
justfile               Task runner for common workflows

The integrated game spec lives at specs/quint_crawl.qnt — 7 record-typed state vars, ~50 actions, ~46 invariants covering HP/gold/level/position/inventory bounds, level gates, skill prerequisites, quest counters, cooldowns, status effects, enchantment slots, companion loyalty, and victory conditions.

Alongside it, specs/{core,combat,items,economy,world,social}/ holds 38 standalone spec modules (rpg, combat, equip, healing, stacking, shop, status, crafting, party, leveling, cooldown, quest, durability, loot, respawn, dynamic_shop, combat_full, capacity_craft, gated_craft, stamina, skill_tree, reputation, summoning, world_grid, elemental, enchantment, trap, companion, salvage, auction, faction, fast_travel, dialogue, fog_of_war, permadeath, bounty, trade) that each verify one subsystem in isolation — useful as unit tests for the underlying mechanics before integration.

just play            # build and run the game
just build-game      # build without running

just check           # typecheck all specs
just traces          # generate MBT traces for all specs
just test            # run all Odin MBT tests
just all             # check + traces + test
just retest          # traces + test

just check-one rpg             # typecheck one spec
just test-one rpg              # test one module
just trace rpg rpg_run         # regenerate one trace
just trace-crawl               # regenerate quint_crawl traces (5x, 100k samples)
just test-crawl                # regen traces + run crawl MBT tests
just verify NAME MAIN INVARIANT # run invariant check (100k traces, 20 steps)

• Odin (with vendor:raylib)
• Quint (tested with 0.32.0)
• just (task runner)
• X server or WSLg (if running on WSL)

• Asset Design Guide — sprite specs for V2 visual upgrade (91 required assets)