Metadata

This NeurIPS'26 workshop paper takes TLA+ specs from GitHub, translates them into Verus, and has LLM agents prove the safety and liveness properties in the specs. The motivation The paper aims to address two problems it raises with TLA+. First, nothing ties the spec to the code, so they drift apart. And second, it claims that proof support is thin: TLC only checks small configurations, and TLAPS is weak on liveness. They abandon pursuing the first weakness they raise at the onset of the paper. Closing it needs a proof that the generated Rust code (which it turns out TLA-Verus doesn't produce anyway) refines the spec, so they list this as future work. It gets worse though. There is no refinement proof between the TLA+ spec and the Verus spec either. Nothing establishes that the translated Verus spec means what the original meant. (Trace validation, meanwhile, is a viable way of tying TLA+ to implementation code, and has been getting a lot of attention recently. ) They dedicate ...

I have come to suspect that to most people thinking is painful. Some of us are addicted to thinking. Some of us find it a necessity. Johnny enjoyed it. I even have the suspicion that he enjoyed almost nothing else. -- Edward Teller, eulogizing John von Neumann I listened to Ananyo Bhattacharya's " The Man from the Future: The Visionary Life of John von Neumann " in my car during the many commute hours Bay Area traffic afforded me. I thought I should share the Johnny phenomena here. I knew about von Neumann being a very influential mathematician/scientist/engineer but the full list still left me bedazzled. In his 53 years of life (1903-1957), von Neumann seeded so many fields. Every time there was an important discovery in physics, mathematics or computation, John von Neumann was there. Set theory and the foundations of mathematics. The mathematical formulation of quantum mechanics. Operator algebras (still called von Neumann algebras). Ergodic theory. Game theory. Expect...

I listened to a recent episode of Cal Newport's "Deep Questions" podcast, where he interviews Emile P. Torres. Cal says that if you want to understand what is happening in AI, you have to understand the futurist ideologies that shape the people running the frontier labs. Torres is a researcher who studies eschatological and utopian movements. They spent a decade inside this movement as a true believer, published in it, worked as a research assistant to Ray Kurzweil, did a stint at Cambridge's Centre for the Study of Existential Risk, and then defected in 2019. TESCREAL Torres coined " TESCREAL " with the computer scientist Timnit Gebru around late 2022. They were trying to name the seven ideological drivers behind the race to build artificial superintelligence : Transhumanism, Extropianism, Singularitarianism, Cosmism, Rationalism, Effective Altruism, and Longtermism. This is also roughly the chronological order these ideologies emerged over the last 40 yea...

This is the second half of my HPTS 2026 notes. Day 1 was mostly about AI and the importance of specifications . Day 2 and day 3 cover hardware, object storage, failures, consensus, and lakehouses. Session 5: Hardware will save us all (chair: Natassa Ailamaki) The Fastest Way to be the Fastest (Bobbi Yogatama, NVIDIA) GPUs and databases have a love-hate relationship, and Bobbi listed the three reasons: limited GPU memory capacity, the interconnect bottleneck, and engineering complexity. The first two are being fixed by the hardware roadmap. HBM is getting larger and faster. Interconnects and network fabrics are getting faster. But engineering complexity requires some work. No one is eager to rewrite their database to get it work with a GPU. Bobbi introduced Sirius , a GPU-native composable analytics engine. It offers a drop-in accelerator for your existing database, with GPU-native execution underneath. MICE is the design principle: modular, interoperable, composable, extensible. Bobbi ...

Jim Gray started HPTS  42 years ago, and it still runs the same way at Asilomar with 0 proceedings, 1 track, 100 invited people, and ample discussion breaks. It's one of my favorite events, and I look forward to attending it every two years. This is my...umm...fifth HPTS. I have been attending all of them since 2015 , but I seem to have missed it in 2019 . Yep, my life is a blur, even for me. Here are my notes from day 1. I will put day 2 and day 3 in a second post. Keynote: Reality is the Final Verifier. Two Key Gaps in Agentic Software Engineering (Ion Stoica, UC Berkeley) Ion started with the promising parts. LLMs are able to solve difficult math problems, and provide proofs for conjectures that have been outstanding for many decades (Ok, maybe this is not as promising to mathematicians). LLMs also play scientist with AlphaEvolve, and OpenEvolve. In summer 2025 Berkeley ran a seminar where students applied agentic tools to research problems. They took a published state-of-the-a...

Atlas Infinite , which dropped in public preview on September 29 alongside MongoDB 9.0, delivers a significant architectural update payload: compute-storage disaggregation. Separating compute from storage is not new , and there are well-known ways to do it. But what makes Atlas Infinite interesting is how MongoDB departs from the standard design to keep WiredTiger's efficiency and to ensure that the shared storage layer never sees customer data unencrypted. I am giving a high level overview of the architecture here distilling from the MongoDB Engineering blog post by Abhishek Chauhan, who led the effort. For detailed coverage, I refer you to that post. It is a great read, and parts 2 and 3 will drop soon. Why not earlier, and why now Disaggregated databases have existed for some time, so why did MongoDB wait? This is mainly because MongoDB didn't need disaggregation to scale out: when a workload outgrew one machine, sharding spread it across many nodes in a seamless manner.  M...

General methods that scale with computation will inevitably displace hand-engineered domain knowledge! Sutton’s Bitter Lesson hangs like a Sword of Damocles over all of us. This paper, which just dropped, applies that lesson to data agents, and says that as LLMs improve, they will quickly absorb the agent scaffolding researchers have spent the last few years painstakingly building. It argues that researchers should instead work on building curated contextual information about the data environment (aka. persistent semantic context) to help data agents be efficient across many queries. The Bitter Lesson for Data Agents The evaluation section aims to capture the Bitter Lesson in action. The authors compared general coding agents (the Codex harness with no task-specific engineering) against state-of-the-art human-designed data agents on two benchmarks, TAG-Bench and DAB. They use the same models on both sides, so the only variable is the scaffolding. They find that: Although the human-d...