We study finite Kripke semantics as an explicit search and certification problem for modal formulas. Sets of worlds are encoded as integer bitmasks, so Boolean connectives, $\Box$, and $\Diamond$ reduce to word-level containment and intersection tests. This gives a deterministic evaluator with an independent certificate checker, then scales it through a fused CUDA kernel for exhaustive small-frame scans. Over $K,T,S4,S5$, a corpus of 5,624 formulas is evaluated on all frames through five worlds, performing $1.63\times 10^{14}$ formula evaluations in 45 minutes on one H100. All 20,990 emitted countermodel certificates verify. In this bounded corpus, every $K$-refutable formula has a countermodel on at most two worlds, far below the standard filtration bound $2^{|\mathrm{Sub}(\varphi)|}$. We then turn pairwise formula equivalence into a minimal-countermodel problem for biconditionals and synthesize semantic mirages: formulas that agree on every model up to a finite size and split only later. In particular, $α_2=(\Box\Diamond)^2\top$ and $α_3=(\Box\Diamond)^3\top$ agree on all frames of at most five worlds but are separated by a checked six-world path. Finally, we build a density-aggregated semantic atlas for representation-guided candidate retrieval and compare raw features, PCA, UMAP, spectral layouts, and random layouts under a common million-pair verifier budget. The result is a reproducible bridge between modal finite-model theory, GPU enumeration, certificate checking, and graphics-supported semantic exploration.

翻译：我们将有限克里普克语义研究为模态公式的显式搜索与验证问题。世界集合被编码为整数位掩码，从而布尔联结词、$\Box$和$\Diamond$退化为字级包含与交集测试。该方法提供了一个确定性求值器与独立的证书验证器，并通过融合CUDA内核实现可扩展的穷举小框架扫描。针对$K,T,S4,S5$逻辑系统，在包含5个世界的所有框架上对5624个公式组成的语料库进行评估，在单块H100平台上于45分钟内完成$1.63\times 10^{14}$次公式求值。所有20990个生成的反模型证书均通过验证。在该有界语料库中，每个$K$可驳斥公式均存在至多两个世界的反模型，远低于标准过滤界限$2^{|\mathrm{Sub}(\varphi)|}$。随后我们将成对公式等价问题转化为双条件式的最小反模型问题，并合成了语义幻影：在有限规模的每个模型上一致、仅在后继更大框架中产生差异的公式。特别地，$α_2=(\Box\Diamond)^2\top$与$α_3=(\Box\Diamond)^3\top$在所有不超过5个世界的框架上保持一致，但被一个经过验证的六世界路径分离。最后，我们构建了密度聚合的语义图谱，用于基于表征引导的候选检索，并在统一的百万对验证器预算下比较原始特征、PCA、UMAP、谱布局和随机布局。该成果为模态有限模型论、GPU枚举、证书验证与图形支持的语义探索之间建立了可复现的桥梁。