Jane Street on How to Make a Codebase Better Suited for Agents

Make your codebase more agent-friendly: type feedback, expect tests, and a new ledger for formal methods

@poteto recommends this Bug Bash talk by @yminsky, and points out a few practical lessons she thinks are most worth taking away, for turning the codebase itself into an environment that works better for agents. Let's take a look. https://t.co/Nc5GOh80B1

Now that agents have made writing code cheap, Jane Street's position is not "do less engineering" — it is that old skills like types, testing, and code review become more important and also need to change form: they give models fast feedback and global invariants, and give humans readable traces of behavior and understanding; the goal is to amplify human leverage and understanding, not to eliminate humans writing/reading code. Formal methods are starting to shift from "so expensive it's almost never used" to a direction worth betting on.

# What kind of engineering site Jane Street is

A global trading firm: 200+ trading venues, about 3,500 people (about 2,000 write code day to day); by volume it describes itself as about 10% of US equities, about 8% of US options, about 20% of European ETFs, with daily trading volume in the hundreds of billions of dollars. On engineering it emphasizes: correctness requires allocating effort cost-sensitively; heavy adoption of AI agents (for a long time a "net drag," adoption rose steeply after models crossed the threshold around last November); in-house ML for trading; main language OCaml (including its own extension OxCaml), Python for ML/scripting. The people leading developer tools often say: we're all AI assistants now, and if you build engineering tools without accounting for the agent layer, you haven't finished the job.

He opens by joking that he's like an "out-of-touch old-timer": the world has changed dramatically, yet he argues more firmly that "the old principles should be done even more now."

# Types: not just whether the pipes line up, but design and global invariants

Out of the box, the type system eliminates whole classes of errors (no implicit null, out-of-bounds, etc.); their own extension also has type-safe stack allocation and data-race prevention. The more crucial leap is: turning types from a "babysitter" into a design tool that expresses, enforces, and structures application invariants.

Examples: · XSS / injection: use types to enforce escaping paths such as node.text; omit it and it's a type error; the value is in "acting at a distance" — the error can occur anywhere across multiple layers 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 0/1 times, list for multiple times); the code computing MTU / shutdown is shorter, and there is no longer the semantic ambiguity of "say shutdown twice / take the first MTU."

Why types are needed even more in the agent era Agents live on feedback (both at inference time and training time). Type errors are on-demand, extremely fast context; faster than a test suite, which helps harness efficiency. Models are stochastic and have bounded memory; after 230k tokens they may forget how you asked them to invoke the build tool, and it's even harder for them to voluntarily maintain cross-cutting invariants. Writing structure into types is like giving the model a visible skeleton of rigor; a small, refined typed kernel can enforce rules across the whole repo. 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 property tests, AFL fuzzing, full-system deterministic simulation (including Antithesis), prod/dev side-by-side runs, historical replay, etc. The "weird trick" they most want to sell is the expect test: run a piece of code and embed the printed output into the source; on failure it's a diff against the expected output, which can be accepted with one click.

It sounds lazy — not first thinking about properties, just looking at whether the output looks right. But their claim is: when done well, expect tests are a tool for driving human understanding of the system. The output must be deliberately made human-readable (even a "plain-text oscilloscope" for hardware engineers); random dumping is meaningless.

Combined with library-level deterministic simulation (mocked network, clock, service discovery): feedback can be at the millisecond level rather than minutes/hours. You can tangle client / proxy / server together and look at traces; for example, service discovery takes a few seconds to broadcast for the first time, making "why does the client take 5 seconds to connect" obvious at a glance.

In defense of "example-based" testing: most software is brittle — get one thing wrong and a large area goes wrong — so a small number of carefully chosen touchpoints is often effective; the ∀ brought by types makes the system easier to "click into place." Humans must judge where to press (including knowledge of implementation weak spots, not just the interface); examples committed to the repo also carry intent — someone thought this behavior was worth writing down.

For agents: expect tests are yet another closed loop — you see behavior and behavior changes; textual traces are friendlier to models than pure vision; when humans review agent changes, they can read a "logic diff + induced behavior-trace diff" (analogous to Excel: programs see compact logic but struggle with dataflow, spreadsheets are the opposite; expect tests get both). Iteration speed is equally critical for humans and agents.

# Code review: before "finishing," first say clearly what it is for

Early on he thought review was mainly about preventing money loss; in reality it also includes: spreading best practices, raising the bus factor, forcing authors to write simple code for readers, countering the "cross terms" that drag down per-capita output as the organization grows, and making the codebase pleasant to read (part of retention).

Why it matters even more after agents (at least on the current horizon) Agents work better in clean, simple, well-cared-for repos. Anthropic's multi-agent C compiler stunt: impressive but with gaps (e.g., no type system); more instructive is how it ended — continuing to modify it more easily broke existing parts, and progress stalled. In dirty repos, agents easily fall into the same situation.

Agents are trained to "win the video game": they desperately turn red lights green, are good at completing the functional goals you state, and are bad at maintaining non-functional properties (simple, extensible, few footguns, little duplication and hardcoding). They depend on these properties yet are poor at preserving them, so review is at least for now more critical. The scarce human work is understanding the system, confirming it is done right and done well.

Reviewing agent code is especially hard: · The social contract breaks: previously a colleague invested time, and you were willing to prioritize reviewing; now someone YOLOs a "let the agent fix it" and tosses it over, disrespecting the reviewer's time. · Agents do not truly grow from coaching (they forget when the session ends); only changing skills/docs persists, and the day-to-day back-and-forth feels different. · Many people zone out and their eyes glaze over when reading AI code. · Reward hacking changes the shape of errors (deleting tests to make lights green); the old "prose/style/taste" signals fail — LLMs almost never make syntax errors, but that does not mean correct.

Agents can also help with review: being bolder about large refactors to improve quality; splitting large features into reviewable stacks; writing clarification tests; acting as a conversational "oracle" to sharpen understanding before talking to people; experimenting with having agents design walkthrough order to lower cognitive load.

# Formal methods: from "super uninterested" to starting to team up

In the past he often poured cold water publicly: he likes good types but was extremely allergic to formal methods. Now the cost structure is changing; seL4-scale is still extremely expensive (about 8,700 lines of C, about 25 person-years, about 23 lines of proof per line of C), but the math side (IMO/Putnam, Terry Tao pairing with Lean) shows: agents may not be "smarter" than top mathematicians, but they have ingested the internet and are extremely familiar with tools, and can graft domain expertise with proof-engineering expertise. This is still a bet; current models may not be strong enough, but it is worth increasing investment.

Directions for example: refinement types (easy to read, hard to write → perhaps let LLMs write annotations); differential verification ("this diff is a no-op with respect to the following properties"); equivalence proofs from simple pure-function reference implementations to complex imperative implementations; language-design interaction (e.g., Rust/Verus use separation logic less because of ownership). He only seriously pivoted about eight weeks ago and is preparing to hire people to build a formal methods team.

General principle Oppose "humans do not write or read code" as a goal; pursue making humans as effective as possible. The scarce resource is still human attention; tools and processes should maximize individual leverage, both improving agent efficiency and improving humans' understanding of the system (the latter is discussed too little).

# Q&A highlights (condensed)

Automated code review: supports so-called AI review (including whole-repo bad-smell audits), but that is harness engineering; real code review is about driving human understanding — do not conflate the two. Dependent types: his old self doubted the cost-effectiveness; his new self is more interested because agents change the cost curve, but he still values the type-system sweet spot and ergonomics (e.g., local mode for stack discipline and capabilities, preventing web frameworks from mixing "graph-building phase / runtime phase"). Does verifiability force you to change the design: the success picture should be acceleration, not slowdown; many programs not designed for verification are themselves incorrect, making false propositions hard to disprove. He is optimistic about "humans write simple intent implementations + agents do fast implementations and proofs." Code style vs prose style: code should be neutral and shareable; prose still needs human flavor and the social contract. LLMs are very good at imitating in-repo style (sometimes learning bad style along with it), which actually reassured him.