Hi, I'm N0zoM1z0 👋

🔬 Senior Incident Resolver @ Touhou-Lab · ⛩ Founding President of @Touhou-University · 🌏 Outside-World Student @ Tsinghua University

Reverse engineering · game systems · music tooling · formal methods · zero-knowledge systems

My GitHub is what happens when a Touhou fan treats curiosity as incident response. This has caused several incidents.

The name N0zoM1z0 is Nozomi + Mizore, from Liz and the Blue Bird, with just enough leetspeak to survive as an internet handle. That probably also explains why music keeps finding its way into repositories that were supposed to be about something else.

I reverse engineer old games, build agents that have to survive the games they claim to understand, and use formal methods whenever “looks right” stops being a useful standard. Sometimes I also ask coding agents to make IA sing.

If a postmortem grows too large for a README, it usually escapes to my personal site.

What I'm working on right now, translated into the University's preferred reporting format.

Most of my office hours are still spent investigating incidents in Gensokyo.

The lab rule is simple: simulation may suggest; the shipped game gets the final say.

• Reconstruction with receipts — TH07, TH08, and TH10.5 are source-reconstruction projects tied back to their original Japanese executables. Touhou Reverse Engineering holds the address maps, runtime experiments, patches, and other evidence gathered along the way. “Looks equivalent” is not a matching criterion.

• Getting old games to run somewhere they were never invited — the reconstructed TH08 code now has a playable modern Linux path, while TH08 Web compiles the game logic to WebAssembly and runs entirely in the browser with locally supplied retail DAT files. One endless night, now also a browser problem.

• Agents that answer to the game — the TH06, TH08, and TH10.5 solvers each use a different mix of state extraction, planning, experiments, and learning, but they share one contract: observe the real game, act through controlled input, and do not award shrine credit for a route that only works in a convenient model. The newer TH06 RL, TH08 RL, and PC-98 RL experiments keep learning behind explicit safety and evidence boundaries.

• Fuzzing the spell machinery — DanmakuFuzz treats ECL timelines, replay payloads, ANM resources, and game file formats as structured mutation targets. Headless execution is the fast scout; reduction makes the result understandable; Wine and the retail game decide whether a finding gets promoted.

• Faster Gensokyo, with disclaimers — th06-headless strips TH06 down to a deterministic accelerated Linux logic runtime for solver, replay, and RL research. It is useful for generating evidence quickly. It is deliberately not allowed to appoint itself the oracle.

• Proof-carrying spell cards — zkTH06 starts from differential traces against the shipped game, rebuilds gameplay semantics a boundary at a time, and feeds private replay input into OpenVM proofs. Apparently “did this run really happen?” is now a zero-knowledge question.

• The university itself — the joke got out of hand, so 幻想鄉立東方大學 now has seven schools, admissions, course registration, exams, thesis defences, research ethics, fieldwork, housing, healthcare, incident dossiers, careers, alumni, and a suspicious amount of lunar paperwork. There is also a hidden PHANTASM curriculum, because apparently ordinary higher education was not complicated enough.

• VOCALOID MCP — an MCP server that lets coding agents compose, tune, render, mix, and audit native VOCALOID3/4 projects. It can validate the project and its native rendering path. It cannot prove that the song is good; human listening retains jurisdiction.
• osu! Reverse Engineering — native parsers, planners, and in-process timing experiments for mania, taiko, and catch, plus a static analysis of the client's integrity mechanisms.

Catch autoplay field report: 99.93%, 2,806pp on Flowering Night Fever. osu! later banned the account—fair enough, honestly XD. The experiment is over; the screenshot survives.

• oszillator — drop an .osz into the browser and play. Web Audio owns the clock; Pixi owns the playfield; your beatmap never leaves your machine. Try the live demo →

I spend a lot of time on programs that are supposed to justify themselves.

The recurring question is not just “did the checker accept it?” but what exactly did we model, and is that actually the thing we meant to claim?

• VeriMorph — low-level program transformations with explicit semantics, checked side conditions, synthesis where search is actually useful, and translation validation before transformed bytes are allowed out. The x86-64 path stays narrow on purpose: unsupported cases are much better than quietly invented guarantees.

• Sphinx Interrogator — a deliberately leaky microcoded VM and a black-box interrogator trying to recover its hidden state. Instead of brute-forcing one noisy signal, it designs relational experiments, learns the hidden machine, and uses SMT/CEGIS to decide what question is worth asking next.

• zkTH06 — the inevitable Touhou crossover episode. Start with frame-by-frame evidence from the retail game, make the executable semantics precise enough to reproduce, then ask a private replay to carry the witness through OpenVM. The proof is only as interesting as the boundary it actually covers.

• ProofMark — a privacy-preserving assessment workflow built around anonymous eligibility, blind marking, tamper-evident records, and Noir proofs. The point is not to put a gradebook on-chain; it is to prove the useful facts without exposing everything else.

TouHou University approved my outside-world paperwork. Somehow.

Current postings include:

• Tsinghua University — my current outside-world posting. I study how to find holes in the Great Hakurei Barrier, how to tell when something crossed it that should not have, and how to keep Gensokyo on the correct side of the boundary. Sometimes the incident report gets reformatted and submitted in the local academic format known as a paper.

• Preference Labs — with morluto, I work on Jacobian, LeanToken, and Preference: exact mathematics, finding the code that matters, and getting agents to look at the evidence before they commit to a story.

• Bera Buddies — I'm a research intern working on zero knowledge, formal methods, and agent security. Most of the interesting work is still private; the Barrier is functioning as designed :3

When the work stops, the methodology becomes considerably less rigorous.

• 🌿 Visual novel: Key's Rewrite. Favorite means favorite. I am not accepting review comments on this one.

• 🕊️ Liz: I keep the complete 47-track Liz and the Blue Bird soundtrack in DSF. Is that necessary? No. Is it staying that way? Absolutely.

• 🌕 Lunar allegiance: TH08 → Eientei → Kaguya → “竹取飛翔 ～ Lunatic Princess.” Eirin still handles incident response: (ﾟ∀ﾟ)o彡゜えーりん！えーりん！ My music folder contains roughly thirty related files, which is probably enough evidence to stop calling this a casual preference. The arrangement I keep coming back to is nmk's “sola” from 千紫万紅 (MMO-12, Reitaisai 9, 2012-05-27).

• 🎤 VOCALOID: IA is my favorite voicebank; Natsume Chiaki's Miku track “花色日和” from 天響ノ和樂2 is my favorite song. Favorite voice and favorite song are separate variables. Q.E.D. ...probably.