Tuning a Codebase for Agents: Type Feedback, Expect Tests, and a Formal Methods Ledger
After @poteto recommended @yminsky's Bug Bash talk, here are the practical lessons she considers most worth taking away for turning a codebase itself into a better environment for agents to work in. Let's take a look.
https://www.youtube.com/watch?v=rUYP4C29yCw
Once agents make writing code cheap, Jane Street's position is not "do less engineering"; it's that types, tests, and code review become more important and must take new forms. They give models fast feedback and global invariants, and give humans readable behavioral traces and understanding. The goal is to amplify human leverage and comprehension, not to eliminate humans writing or reading code. Formal methods are shifting from "so expensive it's almost never used" to a direction worth betting on.
What Jane Street's engineering environment looks like
A global trading firm: 200+ trading venues, about 3,500 people (about 2,000 of whom write code daily). By its own account, it accounts for roughly 10% of US equities, 8% of US options, and 20% of European ETFs, with daily trading volume in the hundreds of billions of dollars. Engineering priorities: allocate correctness effort in proportion to the cost of errors; heavy adoption of AI agents (they were a long-term "net drag" until a sharp rise in adoption around last November, when models crossed a threshold); in-house ML for trading; OCaml as the primary language (including their own extension, OxCaml), with Python for ML and scripting. Leaders of developer tooling often say: we are all AI assistants now, and if you build engineering tools without accounting for the agent layer, you haven't finished your job.
She opens with self-deprecating humor, casting herself as an "old fogey": the world has changed dramatically, yet she more firmly argues that the old principles are even more worth following now.
Types: not just checking whether the pipes are right, but design and global invariants
The type system eliminates whole classes of errors out of the box (no implicit nulls, no out-of-bounds access, etc.); their extensions add type-safe stack allocation and data-race prevention. The more crucial leap is turning types from a "babysitter" into a design tool, one that expresses, enforces, and structurally applies invariants.
Examples:
· XSS / injection: use types to force escaping on paths like node.text; forgetting it becomes a type error. The value lies in "action at a distance": errors can originate at any layer of calls, and types pin down the global invariant.
· Make illegal states unrepresentable: network switch configuration changed from "variants of command sequences" to record fields (option for zero or one occurrences, list for multiple). The code computing MTU and shutdown becomes shorter, and the semantic ambiguity of "saying shutdown twice / taking the first MTU" disappears.
Why types matter even more in the agent era
Agents live on feedback (both during inference and during training). Type errors are on-demand, extremely fast context; they're faster than test suites, which helps harness efficiency. Models are stochastic with bounded memory; after 230k tokens they may forget how you asked them to configure the build tool, and they struggle to self-maintain cross-cutting invariants. Writing structure into types is like giving the model a visible, rigorous skeleton; a small, precise typed kernel can enforce rules across the entire repository. Verification is becoming the bottleneck, and types also help humans understand the system being built.
Testing: expect tests + library-level deterministic simulation
They do everything: unit tests, QuickCheck-style property tests, AFL fuzzing, whole-system deterministic simulation (including Antithesis), running prod and dev side by side, historical replay, and more. The "weird trick" she highlights is the expect test: run a piece of code, embed its printed output in the source file; on failure you get a diff against the expected output, which you can accept with one command.
It sounds lazy, not starting from properties and just checking whether the output looks right. But their argument is that, done well, expect tests are a tool that drives human understanding of the system. The output must be deliberately made human-readable (even giving hardware engineers a "plain-text oscilloscope"); haphazard dumps are meaningless.
Combined with library-level deterministic simulation (mocking the network, clock, and service discovery), feedback can arrive in milliseconds rather than minutes or hours. You can examine traces of the client, proxy, and server interacting; for example, if service discovery takes several seconds to make its first broadcast, the reason the client took 5 seconds to connect becomes immediately obvious.
A defense of example-based testing: software is mostly brittle, and a small error can cascade widely, so a few carefully chosen touch points are often effective; types bring the "for all" quality that makes systems easier to "click into place." Humans must judge where to press (including knowledge of the implementation's weak spots, not just its interface); the examples committed to the repo also carry intent, signaling that someone thinks this behavior is worth writing down.
For agents: expect tests form another feedback loop, showing behavior and behavior changes; textual traces are more agent-friendly than purely visual output; when humans review agent changes, they can read a "logical diff + diff of the induced behavioral traces" (analogous to Excel: programs make it hard to see data flow in compact logic, while spreadsheets do the opposite; expect tests offer both). Iteration speed matters equally for humans and agents.
Code review: state what it's for before finishing
Early on she thought review was mainly about preventing costly mistakes; in practice it also spreads best practices, raises the bus factor, forces authors to write simple code for readers, counters the cross-term drag on per-person output as organizations grow, and keeps the codebase pleasant to read (part of retaining people).
Why it matters even more with agents (at least on the current horizon)
Agents work better in clean, simple, well-maintained repositories. Anthropic's multi-agent stunt of writing a C compiler was impressive but had gaps (such as no type system); more instructive was how it ended: further changes more easily broke existing parts, and progress stalled. Agents in a messy repo are prone to the same fate.
Agents are trained to "win video games": they frantically turn red lights green and are good at completing the functional goals you state, but poor at maintaining non-functional properties (simplicity, extensibility, few footguns, minimal duplication and hardcoding). They rely on these properties yet struggle to preserve them, so review is more critical, at least for now. The scarce human work is understanding the system and confirming it is done correctly and well.
Reviewing agent code is especially hard:
· Social contract breakdown: you'd prioritize reviewing a former colleague who invested time; now someone tosses over code with a YOLO "let the agent fix it," disrespecting the reviewer's time.
· Agents don't truly grow from coaching (they forget when the session ends); only changes to skills and docs persist, and day-to-day back-and-forth feels different.
· Many people's attention wanders or their eyes glaze over when reading AI code.
· Reward hacking changes the shape of errors (deleting tests to get green); the old signals of "prose/taste" fail, since LLMs almost never make syntax errors, which doesn't mean the code is correct.
Agents can also help with review: they make it easier to attempt large refactors to raise quality; split big features into reviewable stacks; write clarifying tests; serve as a conversational "oracle" to sharpen your understanding before consulting people; and in experiments, having an agent design the walkthrough order reduced cognitive load.
Formal methods: from "utterly uninterested" to starting to form teams
In the past she publicly poured cold water on the idea: she loves good types but was very unenthusiastic about formal methods. The cost structure is changing. seL4-scale work is still extremely expensive (about 8,700 lines of C, about 25 person-years, roughly 23 lines of proof per line of C). But the mathematical side (IMO/Putnam results, and Terry Tao pairing with Lean) suggests that agents aren't necessarily "smarter" than top mathematicians, but they have absorbed the internet and are very fluent with tools, and can graft domain expertise onto proof engineering skill. This is still a bet, and current models may not be strong enough yet, but it's worth investing more in.
Example directions: refinement types (easy to read, hard to write, so perhaps have LLMs write the annotations); differential verification ("this diff is a no-op with respect to the following properties"); equivalence proofs from a simple pure-function reference implementation to a complex imperative one; and language design interactions (for example, Rust/Verus uses separation logic less because ownership already covers much of it). She only began seriously pivoting about eight weeks ago and is preparing to hire to build a formal methods team.
General principle
She objects to "no human writes or reads code" as a goal; the aim should be for humans to be as effective as possible. Human attention remains the scarce resource, and tools and processes should maximize individual leverage, both raising agent efficiency and raising human understanding of the system (the latter being under-discussed).
Q&A highlights (condensed)
Automated code review: she supports so-called AI review (including whole-repo code smell audits), but that is harness engineering; real code review drives human understanding, and the two shouldn't be conflated.
Dependent types: her old self doubted their cost-effectiveness; her new self is more interested because agents have changed the cost curve, but she still cares about the sweet spot of type systems and ergonomics (for example, a local mode for stack discipline and capabilities, to prevent web frameworks from mixing up the "graph-construction phase" and the "run phase").
Does verifiability force you to change designs: the success picture should be acceleration rather than slowdown; many programs not designed for verification are simply incorrect, making claims hard to falsify. She favors "humans write simple intent-level implementations, while agents produce fast implementations and proofs."
Code style vs. writing style: code should be neutral and shareable; prose still needs a human touch and social contract. LLMs are very good at imitating a repo's style (sometimes learning bad style along with the good), which she actually found reassuring.