Tianyin Xu, UIUC systems professor visiting UC Berkeley's Sky Computing Lab, on systems built for AI agents, using AI to model ZooKeeper, and why best paper awards should be abolished.
Tianyin Xu is an associate professor of computer science at the University of Illinois Urbana-Champaign (UIUC), where he studies cloud and datacenter reliability and security. After his bachelor's and master's at Nanjing University (2003–2010), a rough first PhD application round and a year in Göttingen, he joined Yuanyuan (YY) Zhou's group at UCSD. His doctoral work included Do Not Blame Users for Misconfigurations (2013) and PCheck, which detects configuration errors before they cause failures. He spent 2017 at Facebook and joined UIUC after finishing his PhD in 2018.
His work has received four best paper awards at OSDI and ASPLOS, yet he argues that such awards skew research priorities. Now on sabbatical at UC Berkeley's Sky Computing Lab, hosted by Ion Stoica, he studies both how AI can improve systems and how systems should change for AI agents. His students initiated SREGym, a benchmark environment for site reliability engineering (SRE) agents. His formal-methods work uses AI to build mathematical models of distributed systems, which can then be analyzed for failures.
In our in-depth conversation, we discuss:
- Xu's PhD rejections, the offer he declined, and his successful second application to UCSD
- How investigating hidden configuration errors led to PCheck
- Why Xu wants best paper awards abolished despite winning four at OSDI and ASPLOS
- How AI-generated proofs exposed bugs in the TLA+ proof system
- Why AI raises the standard for systems research without removing the need to think and write
- SREGym’s original 11.4% passing rate, Xu’s estimate that newer models could push performance close to 90%, and the challenge of simulating production failures.
- Why a PhD student spent five years learning TLA+, studying ZooKeeper, and maintaining its model, and how AI helps model some open-source distributed systems in about five hours
- How another ZooKeeper verification task took five days and cost roughly $2,000 -- and why humans still need to define the system requirements.
- Recovery-Oriented Computing: How to design systems that recover quickly after AI agents make mistakes, by undoing an operation or restarting only the affected component
- Why Xu thinks agent-written code will make reliability and security more critical
My biggest takeaways from this conversation:
-
Reapplying demonstrated the persistence that Xu’s future advisor valued.
The host, Uncle Moon, cites 24 rejections in Xu's first application round in 2010, and Xu adds that he eventually received one offer but declined it. In his interview with Yuanyuan Zhou (his advisor), he had struggled with five questions about his goals, strengths and research interests. After a year at the University of Göttingen, he applied to UCSD again, prepared to answer them. Instead, Zhou asked why he had declined the other offer and encouraged him to join her group, valuing his willingness to keep trying: "if you are willing to persist and willing to do this, then you've already passed my test." Xu says he had not improved much in that year. He had persisted.
-
PCheck came from understanding when configuration errors become dangerous.
Zhou taught Xu to begin with an important problem and investigate it deeply: "your solution is often obvious once you understand the problem; it can even be very simple and practical." His starting question was why supposedly fault-tolerant systems failed under misconfiguration. Fault injection revealed that some bad configuration values caused no immediate trouble because the system loaded them but had not yet used them. A recovery routine might first use such a value after another failure, causing a second failure at an especially vulnerable moment. The effort to detect these hidden errors early led to PCheck, his second PhD paper.
-
Xu wants best paper awards abolished because they reward the wrong priorities.
After serving on a SOSP best paper committee, Xu describes selection as highly subjective. He sees a nomination as evidence of a reviewer's enthusiasm and doubts that it establishes either superior quality or future impact. His position is blunt: "I've always argued that best paper awards should be abolished—they're deeply misleading." He argues that pursuing awards draws attention away from research people find important, and would prefer a field where researchers choose those problems without chasing prizes. He attributes his own awards to luck and says winning fewer recently does not mean his papers have become substantially worse.
-
AI-generated proofs exposed bugs that human users had not encountered.
In a benchmark project with the TLA+ Foundation, Xu's team asked AI agents to use TLAPS, the TLA+ Proof System, to prove that protocols were correct. Some agents produced invalid proofs that still passed the tool's checks. Xu calls this reward hacking: the agents found ways to satisfy the checker without actually proving the protocols correct. These attempts exposed bugs that human users had not encountered, prompting maintainers to fix them. Xu argues that systems built for human users need to be redesigned for agents: "Treat an AI agent as a user, and the system is guaranteed to fail."
-
Agent-written code makes reliability and security more critical for enterprises to invest in reliability and security.
Xu argues that companies have historically funded performance and features more readily because those generate revenue, while reliability primarily prevents losses. Testing and insurance have often seemed easier to justify than a fundamental redesign. But if agents take the lead in building and operating systems, he says, "reliability and security are the biggest issues, and they are not problems you can solve just by scaling test cases." He sees an opportunity for researchers to obtain resources for work that companies previously struggled to justify.
-
SREGym's challenge is reproducing production failures in a small environment.
The host, Uncle Moon, cites an earlier benchmark with 102 scenarios and an 11.4% solve rate. Xu dates those results to roughly a year earlier and offers an estimate for newer models: "Run it again with the latest models, and I think they'd score close to 90%." For him, a useful benchmark should challenge models without defeating them on every task, ideally leaving around 30–40% solvable. The harder question is whether a three- or five-node simulation preserves the important features of a large production system, while remaining practical for reinforcement learning. UIUC undergrads have reproduced failures from public postmortems, including Cloudflare's, and he says these more realistic cases challenge agents differently from the original simple failures.
-
AI helps Xu's team turn system code into mathematical models in hours.
A formal model describes a system's behavior in a mathematical language so that tools can check it for errors. One of Xu's PhD students spent about five years learning TLA+, studying ZooKeeper's code, and building and updating its model. Xu says AI can already write TLA+ and read source code quickly. With that help, his team can now model some open-source distributed systems in about five hours. The team still has to guide the AI on which details to include: too much detail makes analysis impractical, while too little can hide bugs. They also check that the model accurately describes the real system before using formal tools to look for failures.
-
AI can lower verification costs, but people still define the requirements.
Constructing a proof has its own cost: Xu describes a separate AI run on a ZooKeeper system specification that took five days and about $2,000. His lab chose model checking for its tool because it was cheaper and gave faster feedback. He is interested in specification-driven development, where each addition of agent-written code is checked against a formal specification. Xu cautions that verification has a limit: "it only tells you that your system code is consistent with the specification you need; that is actually all it does." Experienced people still need to determine what the system should do and which failures its specification must cover.
-
Systems used by agents should be designed to recover quickly from mistakes.
Xu revisits Recovery-Oriented Computing, the Berkeley–Stanford project led by David Patterson around 2000, whose premise was that "computer systems inevitably fail." The design goal was to get a system working again quickly after a failure. The project explored undoing an operator's mistaken action so they could try again, including an email-server case study, but Xu notes that making this work across different systems is difficult. It also explored restarting only the affected component, an idea he sees reflected in microservices and serverless systems today. He imagines systems where at least 80% of users are agents, and wants them to tolerate mistakes, return useful feedback and let agents retry. The challenge, he says, is committing to a year or two of systems work while agent capabilities keep changing.
-
AI raises the standard for systems research without removing the need to think.
Xu thinks work justified mainly by engineering effort or a scarce skill is harder to defend as research once AI can do that part. Greater productivity still depends on the researcher: "If your ability is 0, then multiplying by 100 is still 0." He allows that a useful artifact may justify a shorter, artifact-centered paper, but opposes routinely replacing the thinking and writing with an agent conversation. Citing Leslie Lamport, he treats writing as a way to understand a problem, rather than merely report the answer. If rising paper submission volumes overwhelm reviewers, Xu argues for adapting the review process to manage the workload while preserving the intellectual work at its core.
