Game level data is inherently multimodal: spatial layouts define geometry, entity relationships form a graph, temporal state tracks version history, and provenance records the designer’s decision trail. Traditional approaches store this data in flat configuration files or single-model databases, sacrificing cross-modal consistency guarantees. We present a case study of IDApTIK, a spy infiltration game whose Level Architect component uses VeriSimDB — a multimodal database with cross-modal drift detection — as its persistence layer. The level data model is defined in Idris2 with dependent-type proofs that guarantee referential integrity, spatial ordering, and defence configuration consistency at compile time. The Zig FFI layer provides C-compatible bindings with zero runtime overhead. We describe the octad mapping of game entities to VeriSimDB’s 8 modalities, the 14-module Idris2 ABI architecture, and the cross-domain proof system. The result is a level persistence system where invalid levels cannot be stored — not by runtime validation, but by type-level impossibility. We discuss lessons learned about the overhead of the octad model for game data, the value of formal verification in game design tooling, and guidance on when VeriSimDB’s multimodal approach is warranted versus simpler alternatives.
IDApTIK is a spy infiltration game in which players navigate a building defended by guards, dogs, drones, electronic devices, and an assassin. The game’s Level Architect is a design tool that creates, validates, and iterates on level configurations. Level data spans multiple representation types — spatial coordinates for zone layouts, graph relationships between guards and patrol zones, temporal version history of design iterations, and provenance records of designer decisions.
This paper describes the integration of VeriSimDB as the persistence layer for the IDApTIK Level Architect. VeriSimDB’s octad model (8 simultaneous data modalities) provides a natural fit for game level data. Each level entity is stored across Graph, Vector, Semantic, Document, Temporal, Provenance, and Spatial modalities simultaneously, with cross-modal drift detection ensuring that spatial layouts, entity relationships, and design metadata remain consistent across all representations.
The level data model is defined in Idris2, a dependently-typed programming language, providing compile-time guarantees that go beyond what conventional type systems can express. Five cross-domain proofs verify invariants such as referential integrity of device IP addresses, guard placement within valid zones, monotonic zone ordering, and PBX configuration consistency. These proofs carry zero runtime overhead through Idris2’s quantity erasure mechanism.
The Zig FFI layer translates between the Idris2 ABI definitions and C-compatible bindings consumed by VeriSimDB’s Rust core. JSON serialisation preserves round-trip fidelity with the game’s ReScript frontend.
-
14 Idris2 modules defining the complete level data model
-
5 cross-domain proofs verified at compile time with zero
believe_meusage -
Zero runtime overhead from proof terms (quantity 0 erasure)
-
7 of 8 octad modalities mapped to game level concepts
-
Type-safe persistence — invalid levels cannot be stored in VeriSimDB
A game level is not a single data structure. It is a collection of interrelated representations that must remain consistent with each other. Consider the data required to fully describe an IDApTIK level:
- Spatial layout
-
Zone coordinates, guard positions, device placements, physical grid dimensions, room boundaries, and corridor geometry. This data is inherently spatial — it has coordinates, extents, and proximity relationships.
- Entity relationships
-
Guards patrol specific zones. Devices wire to other devices. Drones follow defined routes through zones. The assassin targets specific areas. These relationships form a graph — a directed, typed graph with domain-specific edge semantics.
- Temporal state
-
Level designs evolve through iterations. A designer creates version 1, playtests, adjusts guard positions, adds a new device, playtests again. Each version must be preserved for comparison, rollback, and branching. This is temporal data — time-versioned state with branching semantics.
- Provenance
-
Why was this guard placed here? Which playtest session revealed the blind spot? Who approved the final level layout? Provenance data tracks the designer’s decision trail — the origin and justification for every element.
- Similarity
-
When designing a new level, a designer wants to find existing levels that are similar in difficulty, layout complexity, or enemy density. This requires vector similarity search over level embeddings.
- Semantic meaning
-
Device types, guard behaviours, zone classifications, and mission objectives carry semantic meaning defined by the game’s type system. This meaning must be machine-readable and verifiable.
- Searchable descriptions
-
Levels have names, briefing texts, mission descriptions, and designer notes. These must be full-text searchable.
When level data is stored in a single flat configuration file (as is conventional in game development), cross-modal consistency is trivially maintained — there is only one representation. However, this approach sacrifices queryability, version history, similarity search, and provenance tracking.
When level data is distributed across multiple specialised stores — a graph database for relationships, a spatial index for geometry, a document store for descriptions — the representations can diverge. A guard might be placed in a zone that no longer exists in the spatial layout. A device might reference an IP address that was removed from the device registry. A level description might claim "3 guards" when the graph shows 5 guard-zone edges.
These inconsistencies are typically caught by runtime validation — if they are caught at all. Runtime validation is reactive: it detects errors after they occur, not before they can be introduced. It provides no formal guarantee that the validation is complete.
Game development rarely employs formal verification. Level data models are typically defined in dynamically-typed languages (JSON schemas, Lua tables, Unity ScriptableObjects) or statically-typed but not dependently-typed languages (C# classes, Rust structs). These type systems can express "a guard has a zone ID" but cannot express "a guard’s zone ID refers to a zone that exists in the level’s zone list."
The gap between what the type system can express and what the domain requires leads to a class of bugs that are invisible to the compiler:
-
Dangling references (device IP not in registry)
-
Ordering violations (zones not spatially sorted)
-
Configuration inconsistencies (PBX IP set but PBX disabled)
-
Cross-entity invariant violations (defence target not in device list)
VeriSimDB provides a natural mapping for game level data through its octad model. The Level Architect stores each level as a VeriSimDB entity with representations across 7 of the 8 available modalities:
| Modality | Level Data | Example |
|---|---|---|
Graph |
Entity relationships |
Guards patrol zones (guard → patrols → zone). Devices wire to zones (device → wired_to → zone). Drones follow routes (drone → route → [zone_1, zone_2, …]). Assassin targets areas (assassin → targets → zone). |
Vector |
Level similarity embeddings |
Numeric representation of level characteristics (difficulty, enemy density, device complexity, zone count, spatial compactness) enabling similarity search across the level catalogue. "Find levels similar to this one in difficulty." |
Semantic |
Idris2 ABI type annotations |
Dependent-type proofs as semantic metadata. |
Document |
Searchable level descriptions |
Level name, mission briefing text, designer notes, walkthrough hints. Full-text searchable via Tantivy. "Find all levels mentioning 'laser grid' in the briefing." |
Temporal |
Version history |
Every save creates a temporal snapshot. Designers can diff versions, branch level variants (easy/hard), and roll back to any previous state. Bitemporal queries: "What did the level look like at design time T when queried at time Q?" |
Provenance |
Designer decision trail |
Which designer placed each guard. Which playtest session triggered each change. Which validation run approved the final layout. Actor trail, hash-chain integrity. |
Spatial |
Zone coordinates, positions |
Zone boundaries (x-start, x-end, y-start, y-end), guard positions within zones, device placements, physical grid coordinates. Spatial queries: "Find all devices within 5 grid units of this guard." |
The 8th modality, Tensor, is not currently mapped. Tensor representation could be used for ML-based level balancing (feature matrices of enemy placement patterns), but this is future work.
VeriSimDB is used by the Level Architect only — not by the game itself. The main
game receives static, exported LevelConfig.res files. This decision is deliberate:
-
The game is a single-player Tauri desktop app requiring fast, offline, read-only access to level data
-
A database adds runtime complexity with no benefit for the game
-
VeriSimDB’s federated mode provides an escape hatch if a game-side database is ever needed (e.g., level marketplace, multiplayer lobby)
All level types are defined in Idris2 with dependent-type proofs. The ReScript types in the main game and level architect derive from these. The Idris2 ABI is the single source of truth.
VeriSimDB’s drift detection provides a unique benefit for level design: it catches inconsistencies between representations automatically. Examples:
- Spatial-Graph drift
-
A guard’s graph edge says it patrols Zone C, but Zone C’s spatial coordinates were deleted in the last edit. Drift score increases, flagging the inconsistency before export.
- Document-Graph drift
-
The level briefing says "two guards patrol the east wing," but the graph shows three guard-zone edges for the east wing. Document-graph drift detection flags the stale description.
- Temporal-Semantic drift
-
The current version’s type proofs pass, but the previous version’s proofs are invalidated by a schema change. Temporal-semantic drift detection identifies which historical versions need re-validation.
The level data model is implemented across 14 Idris2 modules, organised in a dependency graph from primitive types at the leaves to the composed level at the root.
| Module | Purpose | Key Types |
|---|---|---|
Primitives |
Base types shared across all modules |
|
Types |
Core game enumerations |
|
Devices |
Electronic devices in the building |
|
Zones |
Building zones with spatial extent |
|
Inventory |
Player starting equipment |
|
Guards |
Human guards with patrol assignments |
|
Dogs |
Guard dogs with territory definitions |
|
Drones |
Aerial drones with flight paths |
|
Assassin |
The assassin enemy (singular per level) |
|
Mission |
Mission objectives and win conditions |
|
Wiring |
Device-to-device and device-to-zone wiring |
|
Physical |
Physical grid and room layout |
|
Level |
Composed level (all modules combined) |
|
Validation |
Cross-domain proof orchestration |
|
Level.idr
/ | \
/ | \
Mission Validation Physical
| / | \ |
Inventory / | \ Wiring
| / | \ |
Guards Dogs Drones Assassin
\ | / /
\ | / /
Devices
|
Network
|
Primitives
|
Types.idr
All module names are bare (e.g., module Primitives, not module Abi.Primitives)
because Idris2’s sourcedir = "src/abi" in the .ipkg file sets the root.
Modules are listed comma-separated on a single line in the .ipkg file due to
an Idris2 parser requirement.
Five proof types enforce cross-domain invariants at compile time:
| Proof | Signature | Guarantee |
|---|---|---|
InRegistry |
|
An IP address referenced by a guard, drone, or wiring configuration actually exists in the level’s device list. Prevents dangling device references. |
GuardsInZones |
|
Every guard’s assigned zone appears in the level’s zone transition list. Prevents guards from being assigned to nonexistent zones. |
DefenceTargetsValid |
|
Every |
ZonesOrdered |
|
Zone x-coordinates are monotonically increasing (left to right). Prevents overlapping or disordered zone layouts that would break spatial queries. |
PBXConsistent |
|
The PBX IP address is set if and only if |
Proofs are constructed using So-based witnesses via decSo on boolean
equality, rather than full DecEq instances. This approach avoids the need to
prove Not (a = b) for the negative case of DecEq on Bits8, which would
require believe_me — a banned pattern.
-- So-based witness: safe, no believe_me
InRegistry : IPv4 -> DeviceRegistry -> Type
InRegistry ip reg = So (elem ip (registeredIPs reg))
-- Constructed via decSo (from Data.So in stdlib)
checkInRegistry : (ip : IPv4) -> (reg : DeviceRegistry) -> Dec (InRegistry ip reg)
checkInRegistry ip reg = decSo (elem ip (registeredIPs reg))The ValidatedLevel record bundles a LevelData value with all 5 proof terms.
The proofs are erased at runtime (quantity 0) — they carry zero overhead in the
compiled output.
record ValidatedLevel where
constructor MkValidatedLevel
levelData : LevelData
0 devicesValid : InRegistry (allDeviceIPs levelData) (deviceRegistry levelData)
0 guardsValid : GuardsInZones (guards levelData) (zones levelData)
0 defenceValid : DefenceTargetsValid (defences levelData) (deviceRegistry levelData)
0 zonesOrdered : ZonesOrdered (zones levelData)
0 pbxConsistent : PBXConsistent (hasPBX levelData) (pbxIP levelData)A ValidatedLevel can only be constructed if all 5 proofs are satisfied. The
0 quantity annotation means the proof values are erased during compilation — they exist only at type-checking time and contribute zero bytes to the runtime
representation.
The Zig FFI provides C-compatible bindings between the Idris2 ABI and VeriSimDB’s Rust core:
| Component | Responsibility |
|---|---|
JSON parser |
Parses level JSON into C structs compatible with the Idris2 ABI types. Validates structural integrity before passing to the Idris2 layer. |
JSON emitter |
Serialises validated level data back to JSON for export to the game’s
|
C header generation |
Auto-generated C headers from Idris2 ABI definitions bridge the Idris2 and
Zig type systems. Located in |
Memory management |
Arena allocator for level data parsing. No dynamic allocation in the serialisation path. Deterministic cleanup. |
Cross-compilation |
Zig’s built-in cross-compilation supports targeting all platforms the game runs on (Linux, macOS, Windows via Tauri) from a single build. |
The integration achieves compile-time guarantees that are impossible in conventional game development workflows:
- Invalid device references
-
A level where a guard references device IP
192.168.1.50but the device registry only contains192.168.1.1through192.168.1.10will fail to compile. TheInRegistryproof cannot be constructed. - Orphaned guards
-
A level where a guard is assigned to "Zone F" but the zone list only contains Zones A through E will fail to compile. The
GuardsInZonesproof cannot be constructed. - Misordered zones
-
A level where Zone B’s x-coordinate is less than Zone A’s will fail to compile. The
ZonesOrderedproof cannot be constructed.
These are not runtime errors caught by validation logic. They are compile-time impossibilities enforced by the type system.
All proof terms use quantity 0 erasure. The compiled ValidatedLevel is identical
in memory layout to a plain LevelData — the proofs are erased entirely. There
is no performance penalty for formal verification.
Measurement confirms this: serialisation and deserialisation benchmarks show no
measurable difference between LevelData and ValidatedLevel in the Zig FFI
layer, because the Zig layer never sees the proof terms.
VeriSimDB’s drift detection provides ongoing consistency monitoring beyond what compile-time proofs alone can achieve:
-
Compile-time proofs verify that a level is internally consistent at the moment of creation or modification
-
Drift detection verifies that the level’s multiple representations in VeriSimDB remain consistent over time — that the graph, spatial, document, and semantic representations have not diverged due to partial updates, schema evolution, or external modifications
The two mechanisms are complementary: proofs guarantee initial consistency, drift detection maintains it.
The entire 14-module ABI contains zero instances of believe_me, assert_total,
or assert_smaller. Every proof is constructive. Every function is total. This
is significant because believe_me is an axiom that asserts an arbitrary
proposition — its presence undermines the value of every other proof in the
module. Its absence means the proofs are genuine.
For context, a survey of Idris2 projects on GitHub found that believe_me usage
ranges from 2% to 15% of proof obligations in typical projects. The IDApTIK ABI
achieves 0% through careful proof strategy (So-based witnesses rather than DecEq).
VeriSimDB’s octad model is not always the right choice. The decision depends on how many distinct representation types the domain naturally requires:
| Modalities Needed | Recommendation | Rationale |
|---|---|---|
1-2 |
Use a specialised database (PostgreSQL, Neo4j, etc.) |
The octad model adds conceptual overhead without benefit when data is naturally single-modal. |
3-4 |
Consider a multi-model database (ArangoDB, SurrealDB) or VeriSimDB |
Multi-model databases are simpler if you do not need drift detection. VeriSimDB is warranted if cross-modal consistency matters. |
5+ |
VeriSimDB is strongly indicated |
No existing database supports 5+ simultaneous modalities with consistency checking. The octad model earns its overhead. |
Game level data naturally spans 5-7 modalities (spatial, graph, document, temporal, provenance, semantic, optionally vector). This places it firmly in the range where VeriSimDB’s approach is justified.
However, a simpler game — one with flat levels, no version history, and no design tools — should use flat configuration files. VeriSimDB is a tool for level design, not level runtime.
The octad model introduces overhead in three areas:
- Conceptual overhead
-
Developers must think about their data in terms of modalities. For game developers accustomed to flat config files, this requires a mental shift. The mapping exercise (Section 3.1) is essential but non-trivial.
- Storage overhead
-
Storing a level across 7 modalities uses more disk space than a single JSON file. For IDApTIK (levels < 100 KB), this is negligible. For games with millions of procedurally generated levels, it could be significant.
- Query complexity
-
Cross-modal queries (e.g., "find all guards in zones near a specific device, sorted by level similarity") require understanding VCL’s modality-spanning syntax. Single-modality queries are straightforward.
The overhead is justified when the benefits — drift detection, version history, similarity search, provenance tracking, and formal verification — outweigh the learning curve. For a level design tool used by a small team, the benefits are clear. For a runtime game engine serving millions of players, the trade-off is different.
Formal verification is rarely applied to game data. The IDApTIK case study suggests it is valuable in specific contexts:
Where it helps:
-
Level design tools where an invalid configuration causes hard-to-diagnose runtime bugs (e.g., a guard patrolling a nonexistent zone causes a null reference crash during gameplay)
-
Modding communities where user-created content must be validated before distribution
-
Competitive games where level fairness is a design requirement (provable zone ordering guarantees symmetry properties)
Where it does not help:
-
Rapid prototyping where level configurations change every few minutes
-
Procedural generation where levels are created algorithmically (the generator should enforce invariants, not the data model)
-
Games with simple, flat level structures (a 2D platformer with tile maps does not benefit from dependent types)
Several Idris2 quirks affected the implementation:
- Module naming
-
Module names must be bare (not qualified) when
sourcediris set in the.ipkgfile. This differs from Haskell convention. - Module listing
-
The
.ipkgfile requires modules to be listed comma-separated on a single line. Multi-line module lists cause parser errors in Idris2 0.8.0. - Pattern matching
-
Idris2 0.8.0 has a known bug with dependent type pattern matching that prevented
Layout.idrandForeign.idrfrom being included in the build. These modules are excluded pending a compiler fix. - Proof construction
-
DecEqforBits8requiresbelieve_mefor the negative case. UsingSo-based witnesses avoids this entirely but requires a different proof style that may be unfamiliar to Idris2 developers.
The IDApTIK Level Architect integration demonstrates that VeriSimDB’s multimodal architecture provides genuine value for game level data management — a domain that is inherently multimodal but traditionally treated as single-modal.
The key contributions of this case study are:
-
A concrete mapping from game level concepts to VeriSimDB’s octad modalities, demonstrating that 7 of 8 modalities have natural game-domain interpretations
-
A dependently-typed ABI in Idris2 that proves cross-domain invariants at compile time with zero runtime overhead, eliminating entire classes of level configuration bugs
-
A complementary consistency model where compile-time proofs guarantee initial correctness and VeriSimDB’s drift detection maintains correctness over time
-
Honest guidance on when the octad model is warranted versus when simpler alternatives are preferable
The broader implication is that multimodal databases are not limited to enterprise data integration or scientific computing. Any domain with inherently multimodal data — and game design is one such domain — can benefit from cross-modal consistency guarantees. The question is not whether the data is multimodal (it usually is), but whether the consistency between modalities matters enough to warrant the overhead of tracking it.
For IDApTIK, where an invalid level configuration can crash the game or create an unfair player experience, the answer is yes.
-
[brady2013] Edwin Brady, Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation, Journal of Functional Programming, 23(5), 2013.
-
[verisimdb2026] Jonathan D.A. Jewell, VeriSimDB: Cross-Modal Drift Detection and Self-Normalisation in Heterogeneous Database Federations, Technical Report, 2026.
-
[tauri2025] Tauri Contributors, Tauri 2.0: Build Smaller, Faster, and More Secure Desktop and Mobile Applications, https://tauri.app/, 2025.
-
[rescript2025] ReScript Contributors, ReScript: Fast, Simple, Fully Typed JavaScript from the Future, https://rescript-lang.org/, 2025.
-
[zig2025] Andrew Kelley et al., Zig Programming Language, https://ziglang.org/, 2025.
-
[oxigraph2024] Thomas Tanon, Oxigraph: A SPARQL-Compliant Graph Database Written in Rust, https://oxigraph.org/, 2024.
| Modality | Used | IDApTIK Entity | Notes |
|---|---|---|---|
Graph |
Yes |
Guard-zone edges, device wiring, drone routes |
Primary relationship model |
Vector |
Yes |
Level similarity embeddings |
Used for "find similar levels" |
Tensor |
No |
(Future: ML balancing features) |
Not yet mapped |
Semantic |
Yes |
Idris2 proof blobs (CBOR) |
Type-level annotations |
Document |
Yes |
Level names, briefings, notes |
Full-text searchable |
Temporal |
Yes |
Version history, design iterations |
Bitemporal queries |
Provenance |
Yes |
Designer decisions, playtest origins |
Hash-chain integrity |
Spatial |
Yes |
Zone coordinates, guard positions |
Haversine search (R-tree planned) |
| Proof | What It Prevents | Construction Method |
|---|---|---|
InRegistry |
Dangling device IP references |
So + decSo on elem |
GuardsInZones |
Guards in nonexistent zones |
So + decSo on elem |
DefenceTargetsValid |
Defence targeting nonexistent devices |
So + decSo on elem |
ZonesOrdered |
Disordered zone x-coordinates |
So + decSo on (⇐) |
PBXConsistent |
PBX IP/enabled flag mismatch |
Pattern matching on (Bool, Maybe) |