Gus Henry Smith
gushenrysmith@gmail.com – justg.us – GitHub – LinkedIn
Researcher using formal methods and compiler techniques to build environments and verifiers for post-training LLMs on hardware design tasks.
Current Employment
Since May 2026
Research Scientist
- Building novel compute substrates and AI techniques for hardware design.
- Post-training: Building verifiers for RL post-training. Scaling RL by replacing license-limited and low-throughput commercial EDA tools with free and fast open-source alternatives.
- Agentic EDA: Applying techniques from formal methods and compilers to implement agents for hardware design and verification. Exploring large-scale Lean-based hardware verification.
- ML compilation and novel hardware: Leading the design and implementation of the production compiler for a novel compute platform. Interfacing with hardware designers to define the hardware/software interface.
Past Employment
Fall 2025–Spring 2026
Software Engineer, Formal Verification Tools
- Improved synthesis and formal verification capabilities of Yosys, a leading open-source suite for hardware design and verification.
- Formal verification internals: Developed and documented the officially sanctioned process for concolic (alternating concrete/symbolic) bounded model checking with Yosys and SBY (docs page, repo, #360). In the process, found and fixed sharp edges around BMC ( #5701, #5592).
- RISC-V: Enabled support for the formal verification of hardware performance counters and cryptography primitives in the riscv-formal verification suite (to be open sourced eventually).
- Synthesis: Improved usability of Rosette backend (#5128).
Spring 2025–Fall 2025
ChipStack (acquired by Cadence)
Research Scientist
- Developed agentic EDA tooling for hardware design and verification.
- Agentic EDA: Developed agentic tools for understanding large, complex hardware designs.
- Knowledge graphs: Generated knowledge graphs from large designs using Yosys and graph databases.
- Published DUET: Agentic Design Understanding via Experimentation and Testing. Arxiv link.
Fall 2021–Summer 2022
PhD Student Researcher (part-time)
- Trained models for ML-guided optimization of MLIR sparse tensor kernels.
- Dataset generation: Generated a large dataset of CPU runtime measurements. Built clean, noise-free profiling environments. Postprocessed and analyzed data to ensure accuracy.
- ML model design: Trained a model on the generated data. Successfully demonstrated accurate prediction of ML kernel runtime.
- See this presentation.
See Internships as well.
Education
2018–2024
Ph.D. in Computer Science and Engineering
Dissertation: Generation of Compiler Backends from Formal Models of Hardware. Coadvised by Luis Ceze and Zach Tatlock. Focus: using tools from Programming Languages to automatically generate compilers for custom hardware. Led multiple research groups ranging from 2-10 people, each concluding in successful publications. Mentored a number of BS and MS students into top-tier graduate schools and industry positions. Built proficiency in a number of topics: paper writing, evaluation building for tools-based papers, mathematical formalization of novel programming language and compilers concepts, compiler engineering, program synthesis/equality saturation/other automated reasoning techniques, ML compilers, ML-assisted compiler optimization, EDA tooling, logic synthesis, technology mapping, FPGA and ASIC hardware design.
2013–2018
Penn State Schreyer Honors College
B.S. and M.S. in Computer Science and Engineering
Advised by Vijay Narayanan and John Sampson.
Publications
Improving Equality Saturation for EDA via Semantic E-Graphs. PLDI 2026. Sijie Kong, Jingtao Xia, Daniel Ruelas-Petrisko, Zachary D. Sisco, Jonathan Balkind, Gus Henry Smith. ACM DL link.
Fungible Memories for Automated Technology Mapping and Retargeting. PLDI 2026. Zachary D. Sisco, Sijie Kong, Daniel Ruelas-Petrisko, Jingtao Xia, Julian Springer, Varun Rao, Spencer Wang, Gus Henry Smith, Ben Hardekopf, Jonathan Balkind. ACM DL link.
Implementing Cache Coherence with Coroutines: A Case Study. LATTE 2026. PDF link. Andrew David Alex, Jingtao Xia, Gus Henry Smith, Rachit Nigam, Jonathan Balkind, and Gilbert Bernstein.
DUET: Agentic Design Understanding via Experimentation and Testing. Arxiv link. DVCon 2026. Gus Henry Smith, Sandesh Adhikary, Vineet Thumuluri, Vivek Pandit, Kartik Hegde, Hamid Shojaei, Chandra Bhagavatula.
Scaling Program Synthesis Based Technology Mapping with Equality Saturation. WOSET 2024. Arxiv link. Presentation video. Gus Henry Smith, Colin Knizek, Daniel Petrisko, Zachary Tatlock, Jonathan Balkind, Gilbert Louis Bernstein, Haobin Ni, and Chandrakana Nandi. (The Churchroad workshop paper.)
Generation of Compiler Backends from Formal Models of Hardware. Dissertation, University of Washington, 2024. Arxiv link.
FPGA Technology Mapping Using Sketch-Guided Program Synthesis. ASPLOS 2024. Arxiv link. Gus Henry Smith, Ben Kushigian, Vishal Canumalla, Andrew Cheung, Steven Lyubomirsky, Sorawee Porncharoenwase, René Just, and Zachary Tatlock. (The Lakeroad paper.)
Application-Level Validation of Accelerator Designs Using a Formal Software/Hardware Interface. TODAES 2023. Arxiv link. Bo-Yuan Huang, Steven Lyubomirsky, Yi Li, Mike He, Gus Henry Smith, Thierry Tambe, Akash Gaonkar, Vishal Canumalla, Gu-Yeon Wei, Aarti Gupta, Zachary Tatlock, Sharad Malik. (The 3LA paper.)
Fridge Compiler: Optimal Circuits from Molecular Inventories. International Conference on Computational Methods in Systems Biology. Lancelot Wathieu, Gus Smith, Luis Ceze, and Chris Thachuk.
Generate Compilers from Hardware Models! PLARCH@PLDI23. Arxiv link. Gus Henry Smith, Ben Kushigian, Vishal Canumalla, Andrew Cheung, René Just, and Zachary Tatlock.
Pure Tensor Program Rewriting via Access Patterns (Representation Pearl). MAPS 2021. Arxiv link. Gus Henry Smith, Andrew Liu, Steven Lyubomirsky, Scott Davidson, Joseph McMahan, Michael Taylor, Luis Ceze, Zachary Tatlock. (The Glenside paper.)
From DSLs to Accelerator-Rich Platform Implementations: Addressing the Mapping Gap. LATTE 2021. Bo-Yuan Huang, Steven Lyubomirsky, Thierry Tambe, Yi Li, Mike He, Gus Smith, Gu-Yeon Wei, Aarti Gupta, Sharad Malik, Zachary Tatlock.
Enumerating Hardware-Software Splits with Program Rewriting. YArch 2020. Gus Smith, Zachary Tatlock, Luis Ceze.
A FerroFET-Based In-Memory Processor for Solving Distributed and Iterative Optimizations via Least-Squares Method. IEEE Journal on Exploratory Solid-State Computational Devices and Circuits, 2019. Insik Yoon, Muya Chang, Kai Ni, Matthew Jerry, Samantak Gangopadhyay, Gus Henry Smith, Tomer Hamam, Justin Romberg, Vijaykrishnan Narayanan, Asif Khan, Suman Datta, Arijit Raychowdhury.
Designing Processing in Memory Architectures via Static Analysis of Real Programs. MS Thesis, 2018.
Computing With Networks of Oscillatory Dynamical Systems. Proceedings of the IEEE, 2018. Arijit Raychowdhury, Abhinav Parihar, Gus Henry Smith, Vijaykrishnan Narayanan, György Csaba, Matthew Jerry, Wolfgang Porod, Suman Datta.
A FeFET Based Processing-In-Memory Architecture for Solving Distributed Least-Square Optimizations. DRC 2018. Insik Yoon, Muya Chang, Kai Ni, Matthew Jerry, Samantak Gangopadhyay, Gus Smith, Tomer Hamam, Vijaykrishnan Narayanan, Justin Romberg, Shih-Lien Lu, Suman Datta, Arijit Raychowdhury.
Third Eye: A Shopping Assistant for the Visually Impaired. IEEE Computer, 2017. Peter A Zientara, Sooyeon Lee, Gus H Smith, Rorry Brenner, Laurent Itti, Mary B Rosson, John M Carroll, Kevin M Irick, Vijaykrishnan Narayanan.
Talks
- September 2025 @ ORConf, Valencia, Spain: Yosys + egglog: supercharge your passes with equality saturation
- May 2025 @ LatchUp, UCSB: Better FPGA Technology Mapping with Lakeroad
- September 2024–February 2025: Research talks while on Bonderman travel: Trevor Carlson’s group @ National University of Singapore; Microsoft Research Bangalore; LLVM Social Bangalore
- November 2024 @ WOSET, Virtual: Churchroad: Scaling Program Synthesis Based Technology Mapping with Equality Saturation
- May 2024 @ UW: Ph.D. defense
- April 2024 @ ASPLOS, San Diego: Lakeroad conference talk, FPGA Technology Mapping Using Sketch Guided Program Synthesis
Fellowships
Fall 2024–Spring 2025
Bonderman Fellowship for Independent Travel
University of Washington
Fellowship funding independent, solo travel around the world, focusing on long-term stays in unfamiliar countries. Spent six months traveling solo through Singapore, Thailand, Vietnam, India, Taiwan, and Japan. Developed my sense of self and deepened my understanding of what is truly important in my life. Tested my adaptability and flexibility in unfamiliar and uncomfortable situations. Connected with academic colleagues around the world; gave talks at MSR India, National University of Singapore, and NYCU in Taiwan.
Research Projects
Summer 2024–Summer 2025
Lead Researcher
Scaling program-synthesis-based FPGA technology mapping (Lakeroad) using equality saturation. Exploring how to make an SMT solver’s job easier by applying difficult equalities (e.g. equalities over multiplication) before sending queries to the solver.
Fall 2021–Summer 2024
Lead Researcher; UW SAMPL Lab/UW PLSE Lab/Real-time Machine Learning
Implementing more complete, more correct technology mapping for specialized FPGA primitives (e.g. DSPs) using program synthesis and formal semantics automatically extracted from hardware simulation models. Maintaining an automated Verilog to SMTLIB/Rosette converter, used to extract solver-readable expressions describing the semantics of FPGA blocks. Manually debugging the above SMTLIB expressions when synthesis of a hardware design to an FPGA block fails, which often results in finding bugs in the original Verilog.
2020–2024
3LA
Contributor; UW PLSE Lab, w/ colleagues at Princeton and Harvard
Designed a methodology
for verifiably mapping deep learning models to
custom accelerators.
Utilized Glenside
to expose mappings in workloads.
2020–2022
Lead Researcher; UW SAMPL Lab/Real-time Machine Learning
Designed a pure, binder-free intermediate language for optimizing low-level tensor programs via program rewriting. (See Pure Tensor Program Rewriting via Access Patterns.) Used the language to map computations to custom hardware. (See Specialized Accelerators and Compiler Flows: Replacing Accelerator APIs with a Formal Software/Hardware Interface.)
2018–2020
Lead Researcher; UW SAMPL Lab
Enabled the exploration of new, nontraditional datatypes (i.e., alternatives to IEEE 754 floating point) with an extension to TVM, a deep learning compiler. My qualifying exam project for my Ph.D.
2017–2018
Static Analysis for Processing in Memory Accelerator Design
Master’s Project; PSU Microsystems Design Lab
Given a model of accelerating computation using processing in memory, used LLVM to detect potentially offloadable code sections within workloads.
2014–2018
ThirdEye: Shopping Assistant for the Visually Impaired
Contributor, Lead Researcher; PSU Microsystems Design Lab
Built a wearable system to assist the visually impaired in shopping. My undergraduate research.
Internships
Fall 2023–Summer 2024
Sandia National Laboratories
Student Research Intern
Working on Lakeroad and related technologies.
Summers 2016, 2017, 2018, 2021
Software Engineering Intern
Contributed to Java-based Android profiling tools, Chrome Remote Desktop optimizations for embedded devices, the RFCOMM protocol in Fuchsia, and the MLIR sparse tensor dialect. Developed a learned cost model for configuring sparse tensor kernels.
Summer 2019
Microsoft
Research Intern, AI and Advanced Architectures
Statically analyzed deep learning workloads to inform architecture design.
Mentorship
- Sijie Kong, M.S. student at UCSB, since Winter 2025
- Hannah Leung, since 2021
- Colin Knizek, mentored summer 2024
- Thanawat Techaumnuaiwit, mentored spring 2024
- Andrew Cheung, mentored 2022–2024, now pursuing a Ph.D. at UCSD
- Vishal Canumalla, mentored 2021–2024, now pursuing an M.S. at Stanford
- Andrew Liu, mentored 2019–2021, now at Jane Street
Service
Committees
- 2026: Sijie Kong’s MS thesis committee at UC Santa Barbara
Conference Service
- IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems 2026 Reviewer
- ICFP 2025 External Reviewer (1 paper)
- PLDI 2025 External Reviewer (1 paper)
- LATTE 2025 Reviewer (3 papers)
- IEEE Transactions on Reliability 2024 Reviewer (1 paper, 3 rounds)
- ASPLOS 2024 Artifact Evaluator
- SCF22 External Reviewer (1 paper)
- LATTE 2022 Program Committee
- POPL 2021 Artifact Evaluator
- ASPLOS 2020 Artifact Evaluator
Other
- SIGPLAN-M Mentor (See People of PL: Special Mentoring Edition)
Other Stuff I’ve Written
- Verilog Programs have Stream Semantics for the UW PLSE blog
- Verilog Programs are Pure Expressions for the UW PLSE blog
In the News