Asher Feldman

Stealth startup — Automated reasoning at YC

What I'm working on now. More on this soon.

UToPiA Lab, UT Austin — Undergraduate Researcher

Extended TacMiner with Prof. Isil Dillig, Maxine Xin, and Prof. Elias Stengel-Eskin: a dynamic retrieval system that injects relevant custom proof tactics into LLM-based theorem provers at inference time.

Lean 4 Directed Reading Program — Member

Functional programming and formal verification in Lean 4. Proved the termination of quicksort by hand, which is what got me interested in formal reasoning.

Python interpreter and compiler

A Python-like language in C with a dynamic type system, first-class functions, lexical scoping, and both positional and keyword arguments. Compiled a subset of it to x86 assembly through an AST-based backend, with tail-call optimization.

Pipelined CPU

A 3-stage pipelined CPU with a 2-bit saturating-counter branch predictor. Forwarding for data hazards, flushing for control hazards, stalling for resource hazards — a large CPI improvement over flushing on every hazard.

Cross-architecture emulator

An ARM to x86-64 emulator using atomic instructions for safe multithreading, with a cache controller coordinating four 4-way set-associative caches over mmap'd virtual memory and MESI keeping them coherent across cores.

University of Texas at Austin — BS Computer Science and Mathematics

Turing Scholars Honors Program. Coursework: Data Structures (Honors), Discrete Math (Honors), Computer Architecture (Honors), Multivariable Calculus, Linear Algebra with Differential Equations, Number Theory, Probability, Real Analysis, and Automated Logical Reasoning (graduate, audited).

Lean 4 and Rocq. C, C++, Verilog, x86 and ARM assembly. Python, Solidity, JavaScript. Git, Linux, GDB.

First place, Texas Venture Group startup pitch competition.