AI undergraduate @ Zhejiang University  ·  Hangzhou, China

Visual analytics · computer graphics · data-driven systems · automated theorem proving

I'm Jiarui Zhao, an undergraduate student at Zhejiang University and a Morningside Cultural China Scholar.

Passionate about navigating the intersection of AI, computer science, and global cultures, I consider myself a digital flâneur of sorts. Learn more about my journey here.

Languages
Web & Visualization
Data & ML
Graphics & Game
Systems & Hardware
Formal Methods

Isabelle Toolchain for OpenSourceVerif  ·  Isabelle/HOL · Poly/ML · Rust  ·  ongoing · repo private

Building an Isabelle toolchain that extracts trusted Rust code from formal specifications. Responsible for translator back-end development and the testing / verification of the extraction pipeline.

CastLock-Vis  ·  TypeScript Python  ·  in development

A visual-analytics system for actor type-lockup and transformation windows. Four linked D3 views over a macro→meso→micro pipeline (high-dim projection, Shannon-entropy career curves, Markov transition gates, T=0-aligned survival). Heavy stats run offline in Python (UMAP/MDS, KMeans, entropy, Markov); the SPA only renders & links. React 18 · D3.js · Zustand · Vite · pandas / numpy / scikit-learn

ComputerSystemIII  ·  C · SystemVerilog · Assembly  ·  contributor

Computer-systems course project: an operating-system kernel (C / Assembly) running on a SystemVerilog processor design, with a Makefile/linker-script build chain. Co-developed kernel-level systems code.

Dot-life  ·  C# · Unity  ·  game-jam, contributor

3D game built for a game jam. Owned Unity 3D architecture design, plus movement and UI development.

cg_project  ·  C++ · OpenGL · GLSL  ·  contributor

Real-time computer-graphics scene. Responsible for rendering & texturing, character animation, and camera control.

culture_china  ·  TypeScript  ·  contributor

Portal website for the Morningside Cultural China Scholarship. Contributed front-end content development for the site.