M. Zhang
MemorandumRevised 1 August 2026

Michael Zhang

Michael Zhang
Subject
Formal verification, programming languages, and computer architecture
At
Cornell University · B.A. Computer Science, 2028
Contact
mxz6@cornell.edumichael-zhang-lambdacurriculum vitae

I’m an undergraduate at Cornell broadly interested in formal verification, programming languages, computer architecture, and their intersection. Right now I’m at the Capra lab, implementing model-checking algorithms in Rust — most recently Property-Directed Reachability for the Patronus hardware verification toolkit. I like problems where a machine can tell you whether you’re right.

Outside of work, I enjoy running, hiking, and reading.

§1

Experience

  1. 2026 —

    Research Assistant

    Capra, Cornell University

    Implementing the Property-Directed Reachability model-checking algorithm in Rust for the Patronus hardware verification toolkit, advised by Kevin Laeufer and Adrian Sampson. Also designed the counterexample extraction mechanism that emits concrete traces for property violations.

    Generalizing blocked counterexamples-to-induction with UNSAT cores made it ~13.5× faster than vanilla PDR and took HWMCC ’25 benchmarks solved from 2 to 20. Validated against Stanford’s Pono IC3Bits engine with no disagreements.

  2. 2025 — 2026

    Teaching Assistant, CS 3410

    Cornell University

    Led a lab section for Computer System Organization and Programming, covering both lectures and programming activities.

    5.0 / 5.0 overall rating on student-submitted teaching evaluations.

  3. 2025

    Intern

    ZBeats Inc.

    Infrastructure and integration work across a medical-device pipeline: a three-node Proxmox VE high-availability cluster, reverse-engineered ECG conversion logic folded into the production AWS pipeline, and a shipping API in Java and Spring Boot.

    Cut monthly compute cost by more than $2k, accelerated ML training 30%, and reduced conversion errors 20%.

§2

Selected work

  1. 2025

    OJeopardy!

    Lead

    Architected multiplayer command-line Jeopardy! game built on a server-client concurrency model that keeps the game engine loosely coupled from the interface while holding clients in sync, realized with a GraphQL server written in OCaml.

    Ran project planning, delegated tasks, and reviewed pull requests for style and correctness.

  2. 2025

    Quad-core fully pipelined RISC-V processor

    Contributor

    Developed control logic for the pipelined cores and the cache in SystemVerilog RTL, benchmarked with hand-written C programs, and verified with PyMTL unit tests and GTKWave.

§3

Writing

All posts

Nothing published yet. The first post is being written.

§4

News

Nothing to file yet. Talks, papers, and other news will appear here.