- Author
- Yaron Minsky, Jane Street
- Published
- 7 June 2026
- Kind
- Company blog post announcing a new team and hiring
- Original
- blog.janestreet.com/formal-methods-at-jane-street-index/
- Subject
- Checkable specs for coding agents
- Themes
- Checking the work
What it is
Yaron Minsky has been at Jane Street since 2002. The post announces a new formal methods team. It explains the change of heart and why Jane Street can do this work.
What it says
- Minsky says Jane Street judged formal methods too costly. Hardware synthesis was a special case.
- The post uses seL4 as its cost example. Verifying 8,700 lines of C took 25 person-years.
- Minsky argues agentic coding lowers the cost. Models help more people use these tools, but cannot build hard proofs alone.
- The post says agent-written code tends toward slop. Verification is the bottleneck, and formal methods could ease review.
- Minsky argues agents thrive on feedback. Tests cannot cover the state space the way types can.
- The post claims Jane Street controls its language, OxCaml. It also says users there are eager for new type-system features.
What evidence it gives
The post offers argument and the seL4 cost figures. Minsky mentions experience with agents in OxCaml but gives no measurements. No benchmark or case study is presented.
Interests and limits
Jane Street is hiring for this team. The post also serves as a job notice. The claims about agents and verification are the author's judgment, not tested results. The scope is one firm and its own language.
Connections
These links are this wiki's own reading, not claims the sources make.
- Structural Backpressure Beats Smarter Agents. Minsky's cost example is seL4, at 25 person-years for 8,700 lines. Brooks claims much less, covering only invariants someone specified. The two mark ends of one scale. How much guarantee does each hour of specification buy?