The name N0zoM1z0 comes from Nozomi and Mizore in Liz and the Blue Bird, which is my favorite film. Most days, I do security research at Tsinghua University's INSC, where I'm currently focused on formal verification and zero-knowledge systems. I also reconstruct Touhou games, and that work often turns into other experiments.

I write about some of these projects in more detail on my personal site.

• Formal verification. My research applies formal verification to the security of network protocols such as DNS and BGP.
• Zero knowledge and zkVMs. With Bera Buddies, I'm exploring domain-specific zkVMs and broader questions about how zkVMs are designed, including where compiler optimization fits in.
• Agents and AI for math. With morluto, I'm exploring AI for math and building Jacobian, a set of mathematical tools that agents can use and combine. We recently put forward a proposed complete solution to Erdős Problem 81.
• Touhou. I'm reconstructing, porting, and modding Touhou games, and trying out ideas from formal methods, zero knowledge, and fuzzing along the way.

Most of my research is still unpublished, so the related repositories are private for now. The latest work I can talk about is Principled Discovery of DNS Cache Poisoning Vulnerabilities in Bailiwick Enforcement, accepted at NDSS 2027. That's why the public side of my GitHub is mostly Touhou: I'm a fan who can't help bringing my security research habits to the games.

• Reconstruction, ports, and mods. I'm reconstructing TH04, TH08, TH09, TH09.5, TH10, and TH10.5. TH08 Web brings Imperishable Night to the browser with your own retail game files; TH08 Mods brings osu!-style modifiers like Hidden and Flashlight into the same game.

TH08 Mods in action: Hidden, Blind Spot, and Flashlight, all running in the browser port of Imperishable Night.

• Solvers and RL. The dream is to build a solver that clears a TH08 Lunatic route NMNB, with my hands nowhere near the keyboard. Along the way I've been working on TH06, TH06 RL, TH08, TH08 RL, TH10.5, and PC-98 RL.

• Fuzzing and formal methods. DanmakuFuzz mutates scripts, replays, and game files, then checks what actually happens in the shipped games. touhou-formal uses Lean and SMT to model the games' script VMs and find counterexamples to assumptions about them.

• Zero knowledge. zkTH06 is my attempt to prove a TH06 clear without publishing the replay that produced it. The current architecture uses OpenVM; I may try a domain-specific zkVM in a later version.

• TouHou University. 幻想鄉立東方大學 started as a joke about what a university in Gensokyo would look like. I kept building it out until it felt like a place someone might actually attend, with its own courses, campus life, and academic bureaucracy. I have the honor of serving as its founding president.

• I built VOCALOID MCP so coding agents can work on native VOCALOID3/4 projects all the way from composing and tuning to rendering and mixing. It can audit the project and check the native rendering path, though I still have to listen to decide whether the song is any good.

• I've also been taking osu! apart, especially mania, taiko, and catch. osu! Reverse Engineering grew out of writing native parsers and planners for those modes, then running timing experiments inside the client and looking into its 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.

• I made oszillator because I wanted to drop an .osz file into the browser and just play it. Web Audio handles the timing, Pixi draws the playfield, and the beatmap stays on your machine. Try the live demo →

• At Tsinghua University's INSC, I research the security of network protocols using formal verification. Some of that work eventually finds its way into papers.

• I also work with morluto at Preference Labs on Jacobian, LeanToken, and Preference. These projects bring together exact mathematics, finding the code that matters, and helping agents check the evidence before they settle on an answer.

• I'm a research intern at Bera Buddies, where I work on zero knowledge, formal methods, and agent security. Most of what I'm doing there is still private.

Outside work, I spend a lot of time with visual novels, Touhou, and music. These are a few favorites that have stuck with me:

• 🌿 Visual novel: Key's Rewrite is my favorite visual novel. I have my reasons, but I'm not taking review comments on this one.

• 🕊️ Liz: I keep the complete 47-track Liz and the Blue Bird soundtrack in DSF. There's no practical reason it has to be in that format; I just like it that way.

• 🌕 Lunar allegiance: In Touhou, I always find my way back to TH08, Eientei, Kaguya, and “竹取飛翔 ～ Lunatic Princess.” Eirin is still my emergency contact: (ﾟ∀ﾟ)o彡゜えーりん！えーりん！ I have roughly thirty related files in my music folder, so I probably can't call this a casual preference anymore. 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, but my favorite song is Natsume Chiaki's Miku track “花色日和” from 天響ノ和樂2. Apparently, favorite voice and favorite song are separate variables. Q.E.D. ...probably.

If you're interested in any of the things I work on or enjoy—Touhou, formal verification, zero-knowledge systems, music, VOCALOID, or AI agents—I'd love to hear from you. You can reach me on X.

Viel Spaß beim Entdecken – die besten Ideen fangen oft mit einer seltsamen Frage an.