5 ms·

Solving the Jane Street reverse engineering challenge

438 points by anitil 12d ago

anitil 12d ago
Hi HN, I recently solved the Jane Street reverse engineering challenge [0], and I wrote a blog post on how I reached the answer. It's a moderately technical and (hopefully) entertaining run through of the process. I hope you enjoy reading it as much as I enjoyed doing the challenge (though, as you'll read, it was also quite a frustrating process). My github is on the post if you were interested in seeing a bit more in detail what my solution looked like, though I intend to write some follow up posts that are a bit more in the weeds of the solution. And frankly, the code I used is pretty ugly but it got the job done. This is my first blog post, so if you have any feedback please let me know. All the writing, all the code was done by me, by hand, in vim. [0] https://blog.janestreet.com/can-you-reverse-engineer-an-asic/ https://blog.janestreet.com/can-you-reverse-engineer-an-asic...
- vzcx 12d ago
  Incredible amount of determination, but you really did make it hard for yourself! You can install librelane to get the whole open silicon tool suite and the sky130 PDK. Circuit extraction can be done with magic. Going from a spice netlist to verilog netlist is pretty mechanical and not a hard transform to write. You almost immediately have something that can be simulated and a good baseline for further reversing.
  - anitil 12d ago
    > Incredible amount of determination That's very kind of you. At some point I had put so much of myself in to it that I was in too deep and the only was out was to keep digging. I'll take a look at librelane thanks!
  - __atx__ 12d ago
    > Circuit extraction can be done with magic. So that was the missing part for me! I did it from scratch (with custom Python script with gdstk and shapely) (the GDS file does have the cells annotated, so not a big problem but still). I was thinking about scripting the "trace net" tool in klayout but decided that's going to probably bring its own can of worms...
    - vzcx 12d ago
      You can give the cell instances a stable name by setting GDS property 98, which I learned about from my reconnaissance of the puzzle author's github and sky130 visualization tool. This way I was able to spot check a pass over the netlist that broke up the regions into a hierarchical design. I'd like to do a full writeup but haven't had the time.
- NamTaf 12d ago
  I really enjoyed the writing, cheers. And yes, you may have done it the hard way, but you probably learnt 10x more by doing that. As for what to do next, I used to spend way too much of my late-2000s time on puzzle hunts (particularly the Melbourne Uni one [1]) and this tickled the same part of my brain. Unfortunately they're no longer a thing, but it definitely sounds like you'd enjoy something similar. [1]: https://www.puzzles.wiki/wiki/MUMS_Puzzle_Hunt https://www.puzzles.wiki/wiki/MUMS_Puzzle_Hunt
  - gjm11 12d ago
    That particular one may be no longer a thing, but there are definitely still plenty of puzzle hunts going on. See e.g. https://en.wikipedia.org/wiki/Puzzle_hunt https://en.wikipedia.org/wiki/Puzzle_hunt which has a list.
- __atx__ 12d ago
  > It turns out that this ‘sky130’ thing is like a … standard? Or something for making chips. Very cool seeing someone completely naive going into this :) If you want to read more about a bit more... cheaty way to do this, I have written about using formal verification machinery to straight up force the solution out of the netlist here: https://atx.name/electronics/asic-re/ https://atx.name/electronics/asic-re/ . Could be a bit of an infohazard, but I think journey is the goal and yours was certainly more educational :)
  - anitil 12d ago
    I'll definitely be reading this thankyou! I think this would have been a much better way to approach it, it's a bit of a joke in the piece that I always do things the hard way, but it's a genuine mystery to me why I operate this way. I should add I have an EE degree (but have never worked as an EE), so even though I don't know industry standards like this sky130 thing, it's not completely foreign to me.
    - sota_pop 12d ago
      Are you me? EE, always manage to go the hard route (inadvertently)…
    - make3 11d ago
      Doing things the hard way is a lot of times "male" bravado (though this is not limited to males in any way ofc), this is a very common thing in junior engineers. Curiosity is good but maturity is trusting that the problem will get hard at some point anyways, that improving the most efficient way is usually also interesting and is more likely to deliver desired things on time or at all, which can be a big deal if what you're trying to deliver it worth it, like.. a new MRI machine that detects new types of cancers, etc. If you don't care about what you're trying to deliver, that's another problem that requires at least some questioning, though I understand people have families to take care of etc.
  - vzcx 12d ago
    Nice solution and good easter egg find!
- optimisticestim 9d ago
  First blog post for me too! I also took a crack at it (late). I also smashed my keyboard at this for a day and wrote up the journey, hopefully mildly entertaining too: https://gabbytab.github.io/blog/asic-puzzle-2026/ https://gabbytab.github.io/blog/asic-puzzle-2026/
zeninkhan 12d ago
[dead]
piker 12d ago
> Well I don’t really know what to work on next Let me help you: work on figuring out how to spend the millions of dollars every year Jane Street will pay you to clock in. I've heard private aviation is expensive, for example. :)
- walrus01 12d ago
  Google says "Jane Street has global office locations in New York, London, Hong Kong, Singapore, Amsterdam, and Chicago" so if you're really at a loss where to spend your money, I would recommend searching for yacht dealerships in those cities. I'm sure it won't be a problem anymore.
- bko 12d ago
  A lot of places claim they want to hire extremely smart autists, and some do. But these types of employees are incredibly hard to manage. Imagine herding cats. So if you don't invest a lot of effort in building an environment to let this person cook, go down the right rabbit holes and not rub others the wrong way, a person like this is a huge liability to the org.
  - folkrav 12d ago
    Please, explain how you determined this person was an "extremely smart autist".
    - anitil 12d ago
      I took it as a compliment!
      - folkrav 12d ago
        I find it hard to believe that saying autistic people are "incredibly hard to manage", that managing them is like "herding cats" and their presence is a "huge liability to the org" is anywhere near complimentary. Autism presents in thousands of ways, and the portrayal is, at best, caricatural.
charcircuit 12d ago
I wonder how far a LLM could get with this. It will be cool when we get to the point where you can decap a chip, take a picture, and then an LLM can create an emulator for that chip.
- vzcx 12d ago
  This would need good image recognition, but maybe not so far out of the realm of possibility. These GDS design files have a lot more structure to them.
- anitil 12d ago
  I'd say they could solve it much faster than I could. Some of the other commenters are mentioning tools that would have made this so much easier, and I'd assume an LLM would know to use them
- marethyu 12d ago
  I tried and ChatGPT 5.6 managed to figure out the answer within an hour.
gyanchawdhary 12d ago
curious what the actual use case for a challenge like this is from Jane Streets side .. guess the obvious one is trading even closer to the wire .. being able to reverse engineer .. inspect circuits to uncover flaws or optimisations that shave latency or improve determinism in the trading stack .. but I wonder if there are other less obvious applications ..
- bux93 12d ago
  Probably this is just an unfamiliar domain for most non-hardware folks, so it's a nice challenge that might introduce Jane Street to some people they might want to interview for non-hardware roles. But, they do have a hardware division, and Jane Street has a podcast that talks about some of the things they do https://signalsandthreads.com/?tag=hardware https://signalsandthreads.com/?tag=hardware
  - gyanchawdhary 12d ago
    wow thanks for sharing, will check it out
- Andrew-Koper 12d ago
  I read their posts and podcasts. They high frequency trade. They work in micro- and nano-seconds. I don't know what I'm talking about here, don't quote me, but a top guy said they 'process packets' the data is starting to be sent out while it's still arriving. Close to the wire/metal
karelpeeters 12d ago
Congrats on solving the challenge! I also briefly wrote about my approach here, with less pictures but going into slightly more detail about how to convert circuits to z3 equations: https://gist.github.com/KarelPeeters/dba417c2690cf0505ac9079ca1c609ab https://gist.github.com/KarelPeeters/dba417c2690cf0505ac9079...
- anitil 12d ago
  That's really interesting that you actually used z3 to extract the output from the circuit! It hadn't occurred to me that it would be possible to do that. I suppose I got a little fixated on my approach of running a verilog simulation, and I only used z3 to solve one part (though the hardest part I think). How did you get a $DAYJOB involving formal verification?
  - karelpeeters 12d ago
    Yeah I briefly considered switching to a simulator to get the final output, but then luckily realized the Z3 setup I had was already acting as a super-powered simulator anyway! I'm not actually using formal verification at $DAYJOB, there we're using MILP solvers (which are closely related to SAT solvers) as part of the compilation flow when scheduling operations onto hardware accelerators. I have been interested in formal verification for hardware for a while, but so far haven't found an opportunity to apply it. There are some great resources online though: the ZipCpu blog at https://zipcpu.com/formal/formal.html https://zipcpu.com/formal/formal.html and SymbiYosys website at https://symbiyosys.readthedocs.io/en/latest/ https://symbiyosys.readthedocs.io/en/latest/. I hindsight I could probably have used SymbiYosys instead of Z3, it would have saved me from having to walk the graph and map the gates to equations myself.
anon-3988 12d ago
I have used Codex (Sol 5.6 or whatever) to solve this problem. It turns the problem into Z3, then iteratively work through the problems until it figured out the solution. Personally, I did not learn that much from that experience. So I am glad that there's other people working on it as well. I am mostly interested in the techniques used to solve this.
- seritools 12d ago
  > Personally, I did not learn that much from that experience. What did you expect?
  - anon-3988 12d ago
    I understand the sentiment, but in a world where these kinds of problems (And problems at work) that can trivially be solved by LLMs; what kind of value can I provide? That itself is a learning experience. What is even the point of technical interview questions or take home questions? This means that I am now open to hiring completely non-technical person, as long as they have a good personality and management skills more than a competent developer.
    - chermi 12d ago
      "I understand the sentiment, but in a world where these kinds of problems (And problems at work) that can trivially be solved by LLMs; what kind of value can I provide?" This is sad conclusion. Maybe you're more right than wrong, but my answer to the "value" question would be: Solving even harder problems based on lessons from solving easier ones? Pretty similar to the trajectory in this blog post. Perhaps aided additionally by llms and other tools that can solve the subproblems so you can focus on the less obvious/automatable aspects of the problem? But note the tension, only by being involved in the problem solving to some extent do you become better at it. So if your default is to say "An LLM can or will soon be able to solve it, why bother?", then your situation will become more desperate and your outlook more negative in a self-reinforcing way.
- gnyman 12d ago
dhzzwgzua 12d ago
I also look at it and got the same result as well, but I did not submit it. I also figured out the purpose of the circuit: it is a 11x11 Star Battle checker (2 stars per row/column/region, no touching)
- anitil 12d ago
  That is incredible! I've never heard of a Star Battle checker, but that explains the output! Another commenter pointed out there was also some morse code in the layout
amelius 12d ago
If there's a "two stars" solution, then maybe there is also a "three stars" solution?
- __atx__ 12d ago
  I checked and the solution is unique (at least within some reasonable bounds in terms of runtime etc, it's possible there is a 1000 bits long special solution hidden somewhere, but due to the relatively small amount of flops I doubt it).
xvilka 12d ago
To help with such tasks for real chips (given the good quality images) there is Degate[1][2] open source software. [1] https://www.degate.org/ https://www.degate.org/ [2] https://github.com/DegateCommunity/Degate https://github.com/DegateCommunity/Degate
- karelpeeters 12d ago
  Degate is even a bit overkill, it is meant for when you only have images of the physical chip. This challenge has the full GDS files, which are the files that are sent to the fab for manufacturing. They still contain information about all of the separate layers. In this case they even contained the stdcell names, making even full transistor and logic function extraction unnecessary.
BalistaCRATZ 12d ago
Nice! I ended up using the KLayout Python API to parse the GDS and extract the netlist, which was actually quite nice to use. Also, yosys has support for doing “assertion checking”, which I used in my solution: https://sunaabh.com/systems/2026/08/18/jspuzzle.html https://sunaabh.com/systems/2026/08/18/jspuzzle.html
swiftcoder 12d ago
I'm not sure I've ever seen such a vicious case of NIH-syndrome. Regardless, congrats on the solve!
- _false 12d ago
  I first thought you were teasing Jane Street instead of OP. Maybe shows that OP is a good culture fit for Jane Street :)
- bluGill 12d ago
  Since this was for fun, and the goal was learning at least as much as solving the problem that is just fine. More people should get NIH for those purposes. Now if he is presenting his tools as a good way to solve this problem, something you should use, or any such - that would be a bad thing. Good tools for this are complex and need to be done as part of a large team. If good tools that others should use is the goal then he should join some other group making those tools. I'm sure there is an existing open source project (maybe KiCAD - I'm not in this space so that is the only name I can come up with but maybe their goals are different?) that does this and would welcome more help.
mring33621 12d ago
I love this person!
dahshanlabs 12d ago
nice one
fabflying 12d ago
So good
motoxpro 12d ago
So cool to see someone who loves challenges. Congrats!
AlDante2 12d ago
Hi Chris, just for info: https://en.wikipedia.org/wiki/GDSII https://en.wikipedia.org/wiki/GDSII will tell you about the GDS format. It apparently stands for Graphic Data System II (originally developed by Calma in the late 1970s).
- anitil 12d ago
  No spoilers! But thanks I did find out after I published, I just thought it was funnier not to know while I was working on it
ctippett 12d ago
> I ended up using a tool called ‘z3’. It’s kind of magical? Every time it finds a solution I get a surge of joy. This resonates so much. I had a similar feeling after going to my very first operations research lecture. Solving seemingly incomprehensibly complex problems by framing them as a bunch of simple constraints and getting a solution seemed like such magic.
- darksaints 12d ago
  Yeah this was my experience too. I have an undergrad business degree, but got nerd sniped by an optimization problem, found a solution with constraint programming, and ended up going down a 15 year operations research rabbit hole with it. Many people say that the way to tackle a hard problem is to break it down into smaller problems. I disagree. The best way to tackle a hard problem is to break it down into a defined search space and as many seemingly-redundant constraints as you can possibly list, then dump it all into a solver, go take a nap for a few hours or possibly a month, then come back to the problem solved for you.
  - chamomeal 12d ago
    Found minizinc/CP-SAT recently and I’m obsessed
- vismit2000 11d ago
  z3 or constraint programming comes in very handy in at least one challenge every year in Advent of Code! https://adventofcode.com https://adventofcode.com
eru 12d ago
Weren't you supposed to wait until the submissions close to publish spoilers? (Or did they close yesterday?)
- moebrowne 12d ago
  > Submissions close on September 4th, 2026. https://blog.janestreet.com/can-you-reverse-engineer-an-asic/ https://blog.janestreet.com/can-you-reverse-engineer-an-asic...
- anitil 12d ago
  I emailed them and asked as I'm in Sydney and didn't want to mess it up - they said to wait until the end of my workday, so I posted it at roughly 5:30 my time. I hope I didn't spoil it!
  - eru 11d ago
    Their logistics were a bit weird: they asked not to post spoilers, but also ask you to link to your write-up. In any case, I had it all worked out already. But looking at other people's submissions today showed me that I found some easter eggs other hadn't. That was encouraging. (And I missed some that others found, of course.)
    - deleted 11d ago
      [deleted]
    - anitil 9d ago
      I was confused about that too - I ended up posting an empty page to generate the link ahead of time (and hoping that it wouldn't get picked up by anything), then actually posting the solution later. I also realised I'd missed a lot of easter eggs, like the morse code - I wish I'd spotted that!
aavshr 12d ago
There's a typo on your link to the two stars image. It should be `/img/two-stars.png` instead it's right now `/img/two-starts.pgn`. For those interested in the image itself: https://jestoph.com/img/two-stars.png https://jestoph.com/img/two-stars.png
- hosel 12d ago
  oh boy here we go again
- anitil 12d ago
  Oh no! Thanks for that, I must have read it 10 times before posting but somehow didn't spot that it was wrong
skr3178 12d ago
Solving the puzzle with the assistance of a lower capability LLM model (even though I had access to more) turned out to be fun and good learning experience.
Taurenking 12d ago
[dead]
emptyheaded 12d ago
reading the post felt like going down an authentic manic rabbit hole, thanks for sharing your artisanal words @anitil
- anitil 12d ago
  You're very welcome!
thisisauserid 12d ago
I know nothing about z3 but it's from Microsoft. Would Google's OR-Tools component CP-SAT also be useful for something like this?
- myng111 12d ago
  Z3 is an SMT solver, not a SAT solver. You'd probably be looking for something more like Yices, Bitwuzla, cvc5, etc.
  - karelpeeters 12d ago
    In general that's true, but to reason about boolean circuits like in this challenge we only need a SAT solver. Z3 is just used for it's convenient API.
- nostrebored 12d ago
  z3 is also just so thoroughly optimized that even if your formulation of the constraints is inefficient it is faster. it is a great library that lets you solve pretty complicated DP problems with a few dozen lines of code.
mdritch 12d ago
I love z3. I used it for the first time for Jane Street's puzzle last year involving a hashing alg disguised as a neural network. I use a lot of MCMC at work and I have made a few small investigations into MCMC model formal verification via z3, but nothing real yet. This has inspired me to pick that back up.
- kachnuv_ocasek 12d ago
  Can you share more about the connection between MCMC and SAT/SMT? That's a crossover I never thought I'd see.
  - mdritch 12d ago
    Sure! Roughly we are using hierarchical models for reads on underlying count or prevalence data. We use those higher-order means or other fit params to kick off remediation tasks at different levels of that hierarchy depending on those higher level params. We assume some correlation between sibling nodes in that hierarchy. Question: Can one or another of those thresholds in sibling or parent nodes ever be met if some number of the samples are below some floor reading? Or, how many zeros does it take to silence a threshold check on the node itself, a sibling, or a parent? To make this tractable I have tried gridding fit parameters, freezing randomness, and using simplified algs like original Metropolis-Hastings
deleted 12d ago
[deleted]
chermi 12d ago
Aspirational. This is how I want to spend my available time.
josu 12d ago
I gave the problem to chatGPT 5.6 Sol Pro and this was the result: > Worked for 12m 36s > Solved https://chatgpt.com/s/t_6a9aed0b09988191b0f2850dee056b48 https://chatgpt.com/s/t_6a9aed0b09988191b0f2850dee056b48 Edit: It didn't independently solve it. > 1. Used the public reconstruction to obtain the recovered RTL/constraint structure, including the 11×11 region map and the fact that it is a two-stars-per-row/column/region, non-touching puzzle. > 2. Then independently wrote and ran my own exhaustive solver against that recovered constraint system.
- karelpeeters 12d ago
  Looks like it did not actually solve it, but instead it just found an existing solution at https://github.com/NotCleo/GDS-to-RTL https://github.com/NotCleo/GDS-to-RTL and verified parts of it? I have no doubt that modern agents can solve challenges like this even without external help, but you should at least briefly look at the output before posting it online!
  - josu 12d ago
    Thanks for pushing back, I've edited my initial post. I misinterpreted the response, I thought that it only referenced the solution as verification.
  - deleted 12d ago
    [deleted]
aatd86 12d ago
I don't think I can ever be motivated by such challenges. It's either I'm getting up to speed to the state of the art from the very basics and then I can try to figure out if something was missing along the way or solve unsolved useful problems, or I will not be interested. I just can't tinker for the sake of tinkering. Too goal oriented I guess. Just me? (that is also why school started to bore me right before high school and why I learn better on my own, I did go too College but thank god I didn't do CompSci or that would have disgusted me...)
anonymousDan 12d ago
Interesting that they have their own open-source OCaml toolchain for chip design. I thought received wisdom was that everyone in industry is still tied to horrendous vendor toolchains. Is this a realistic alternative for production-grade chip design?
- vzcx 12d ago
  Hardcaml compiles to verilog and then you use the horrendous vendor toolchains.
ngriffiths 12d ago
Oh no The neural net engineering challenge was so awesome, I got really into it, spent way too much time and then was shocked when I actually managed to solve it. Since then I've gotten interested in... hardware. God help me
siramikvarze 12d ago
[dead]
paretolaw 12d ago
I got one better puzzle. Predict Jane algo moves when they try to manipulate market and frontrun their orders. Let them taste their own medicine. :)
userbinator 12d ago
I'm probably not exaggerating if I say that the majority of people on the planet who have the knowledge and skills to easily do this, and are doing it for a living, are in the Far East.
seobotaicom 9d ago
Do you think constraint solvers like Z3 are underused by programmers, or does this kind of problem just happen to be a particularly good fit for them?

438 points by anitil 12d ago

Hi HN, I recently solved the Jane Street reverse engineering challenge [0], and I wrote a blog post on how I reached the answer. It's a moderately technical and (hopefully) entertaining run through of the process. I hope you enjoy reading it as much as I enjoyed doing the challenge (though, as you'll read, it was also quite a frustrating process). My github is on the post if you were interested in seeing a bit more in detail what my solution looked like, though I intend to write some follow up posts that are a bit more in the weeds of the solution. And frankly, the code I used is pretty ugly but it got the job done. This is my first blog post, so if you have any feedback please let me know. All the writing, all the code was done by me, by hand, in vim. [0] https://blog.janestreet.com/can-you-reverse-engineer-an-asic/ https://blog.janestreet.com/can-you-reverse-engineer-an-asic...

vzcx 12d ago
Incredible amount of determination, but you really did make it hard for yourself! You can install librelane to get the whole open silicon tool suite and the sky130 PDK. Circuit extraction can be done with magic. Going from a spice netlist to verilog netlist is pretty mechanical and not a hard transform to write. You almost immediately have something that can be simulated and a good baseline for further reversing.
- anitil 12d ago
  > Incredible amount of determination That's very kind of you. At some point I had put so much of myself in to it that I was in too deep and the only was out was to keep digging. I'll take a look at librelane thanks!
- __atx__ 12d ago
  > Circuit extraction can be done with magic. So that was the missing part for me! I did it from scratch (with custom Python script with gdstk and shapely) (the GDS file does have the cells annotated, so not a big problem but still). I was thinking about scripting the "trace net" tool in klayout but decided that's going to probably bring its own can of worms...
  - vzcx 12d ago
    You can give the cell instances a stable name by setting GDS property 98, which I learned about from my reconnaissance of the puzzle author's github and sky130 visualization tool. This way I was able to spot check a pass over the netlist that broke up the regions into a hierarchical design. I'd like to do a full writeup but haven't had the time.
NamTaf 12d ago
I really enjoyed the writing, cheers. And yes, you may have done it the hard way, but you probably learnt 10x more by doing that. As for what to do next, I used to spend way too much of my late-2000s time on puzzle hunts (particularly the Melbourne Uni one [1]) and this tickled the same part of my brain. Unfortunately they're no longer a thing, but it definitely sounds like you'd enjoy something similar. [1]: https://www.puzzles.wiki/wiki/MUMS_Puzzle_Hunt https://www.puzzles.wiki/wiki/MUMS_Puzzle_Hunt
- gjm11 12d ago
  That particular one may be no longer a thing, but there are definitely still plenty of puzzle hunts going on. See e.g. https://en.wikipedia.org/wiki/Puzzle_hunt https://en.wikipedia.org/wiki/Puzzle_hunt which has a list.
__atx__ 12d ago
> It turns out that this ‘sky130’ thing is like a … standard? Or something for making chips. Very cool seeing someone completely naive going into this :) If you want to read more about a bit more... cheaty way to do this, I have written about using formal verification machinery to straight up force the solution out of the netlist here: https://atx.name/electronics/asic-re/ https://atx.name/electronics/asic-re/ . Could be a bit of an infohazard, but I think journey is the goal and yours was certainly more educational :)
- anitil 12d ago
  I'll definitely be reading this thankyou! I think this would have been a much better way to approach it, it's a bit of a joke in the piece that I always do things the hard way, but it's a genuine mystery to me why I operate this way. I should add I have an EE degree (but have never worked as an EE), so even though I don't know industry standards like this sky130 thing, it's not completely foreign to me.
  - sota_pop 12d ago
    Are you me? EE, always manage to go the hard route (inadvertently)…
  - make3 11d ago
    Doing things the hard way is a lot of times "male" bravado (though this is not limited to males in any way ofc), this is a very common thing in junior engineers. Curiosity is good but maturity is trusting that the problem will get hard at some point anyways, that improving the most efficient way is usually also interesting and is more likely to deliver desired things on time or at all, which can be a big deal if what you're trying to deliver it worth it, like.. a new MRI machine that detects new types of cancers, etc. If you don't care about what you're trying to deliver, that's another problem that requires at least some questioning, though I understand people have families to take care of etc.
- vzcx 12d ago
  Nice solution and good easter egg find!
optimisticestim 9d ago
First blog post for me too! I also took a crack at it (late). I also smashed my keyboard at this for a day and wrote up the journey, hopefully mildly entertaining too: https://gabbytab.github.io/blog/asic-puzzle-2026/ https://gabbytab.github.io/blog/asic-puzzle-2026/

zeninkhan 12d ago

[dead]

piker 12d ago

> Well I don’t really know what to work on next Let me help you: work on figuring out how to spend the millions of dollars every year Jane Street will pay you to clock in. I've heard private aviation is expensive, for example. :)

walrus01 12d ago
Google says "Jane Street has global office locations in New York, London, Hong Kong, Singapore, Amsterdam, and Chicago" so if you're really at a loss where to spend your money, I would recommend searching for yacht dealerships in those cities. I'm sure it won't be a problem anymore.
bko 12d ago
A lot of places claim they want to hire extremely smart autists, and some do. But these types of employees are incredibly hard to manage. Imagine herding cats. So if you don't invest a lot of effort in building an environment to let this person cook, go down the right rabbit holes and not rub others the wrong way, a person like this is a huge liability to the org.
- folkrav 12d ago
  Please, explain how you determined this person was an "extremely smart autist".
  - anitil 12d ago
    I took it as a compliment!
    - folkrav 12d ago
      I find it hard to believe that saying autistic people are "incredibly hard to manage", that managing them is like "herding cats" and their presence is a "huge liability to the org" is anywhere near complimentary. Autism presents in thousands of ways, and the portrayal is, at best, caricatural.

charcircuit 12d ago

I wonder how far a LLM could get with this. It will be cool when we get to the point where you can decap a chip, take a picture, and then an LLM can create an emulator for that chip.

vzcx 12d ago
This would need good image recognition, but maybe not so far out of the realm of possibility. These GDS design files have a lot more structure to them.
anitil 12d ago
I'd say they could solve it much faster than I could. Some of the other commenters are mentioning tools that would have made this so much easier, and I'd assume an LLM would know to use them
marethyu 12d ago
I tried and ChatGPT 5.6 managed to figure out the answer within an hour.

gyanchawdhary 12d ago

curious what the actual use case for a challenge like this is from Jane Streets side .. guess the obvious one is trading even closer to the wire .. being able to reverse engineer .. inspect circuits to uncover flaws or optimisations that shave latency or improve determinism in the trading stack .. but I wonder if there are other less obvious applications ..

bux93 12d ago
Probably this is just an unfamiliar domain for most non-hardware folks, so it's a nice challenge that might introduce Jane Street to some people they might want to interview for non-hardware roles. But, they do have a hardware division, and Jane Street has a podcast that talks about some of the things they do https://signalsandthreads.com/?tag=hardware https://signalsandthreads.com/?tag=hardware
- gyanchawdhary 12d ago
  wow thanks for sharing, will check it out
Andrew-Koper 12d ago
I read their posts and podcasts. They high frequency trade. They work in micro- and nano-seconds. I don't know what I'm talking about here, don't quote me, but a top guy said they 'process packets' the data is starting to be sent out while it's still arriving. Close to the wire/metal

karelpeeters 12d ago

Congrats on solving the challenge! I also briefly wrote about my approach here, with less pictures but going into slightly more detail about how to convert circuits to z3 equations: https://gist.github.com/KarelPeeters/dba417c2690cf0505ac9079ca1c609ab https://gist.github.com/KarelPeeters/dba417c2690cf0505ac9079...

anitil 12d ago
That's really interesting that you actually used z3 to extract the output from the circuit! It hadn't occurred to me that it would be possible to do that. I suppose I got a little fixated on my approach of running a verilog simulation, and I only used z3 to solve one part (though the hardest part I think). How did you get a $DAYJOB involving formal verification?
- karelpeeters 12d ago
  Yeah I briefly considered switching to a simulator to get the final output, but then luckily realized the Z3 setup I had was already acting as a super-powered simulator anyway! I'm not actually using formal verification at $DAYJOB, there we're using MILP solvers (which are closely related to SAT solvers) as part of the compilation flow when scheduling operations onto hardware accelerators. I have been interested in formal verification for hardware for a while, but so far haven't found an opportunity to apply it. There are some great resources online though: the ZipCpu blog at https://zipcpu.com/formal/formal.html https://zipcpu.com/formal/formal.html and SymbiYosys website at https://symbiyosys.readthedocs.io/en/latest/ https://symbiyosys.readthedocs.io/en/latest/. I hindsight I could probably have used SymbiYosys instead of Z3, it would have saved me from having to walk the graph and map the gates to equations myself.

anon-3988 12d ago

I have used Codex (Sol 5.6 or whatever) to solve this problem. It turns the problem into Z3, then iteratively work through the problems until it figured out the solution. Personally, I did not learn that much from that experience. So I am glad that there's other people working on it as well. I am mostly interested in the techniques used to solve this.

seritools 12d ago
> Personally, I did not learn that much from that experience. What did you expect?
- anon-3988 12d ago
  I understand the sentiment, but in a world where these kinds of problems (And problems at work) that can trivially be solved by LLMs; what kind of value can I provide? That itself is a learning experience. What is even the point of technical interview questions or take home questions? This means that I am now open to hiring completely non-technical person, as long as they have a good personality and management skills more than a competent developer.
  - chermi 12d ago
    "I understand the sentiment, but in a world where these kinds of problems (And problems at work) that can trivially be solved by LLMs; what kind of value can I provide?" This is sad conclusion. Maybe you're more right than wrong, but my answer to the "value" question would be: Solving even harder problems based on lessons from solving easier ones? Pretty similar to the trajectory in this blog post. Perhaps aided additionally by llms and other tools that can solve the subproblems so you can focus on the less obvious/automatable aspects of the problem? But note the tension, only by being involved in the problem solving to some extent do you become better at it. So if your default is to say "An LLM can or will soon be able to solve it, why bother?", then your situation will become more desperate and your outlook more negative in a self-reinforcing way.
gnyman 12d ago

dhzzwgzua 12d ago

I also look at it and got the same result as well, but I did not submit it. I also figured out the purpose of the circuit: it is a 11x11 Star Battle checker (2 stars per row/column/region, no touching)

anitil 12d ago
That is incredible! I've never heard of a Star Battle checker, but that explains the output! Another commenter pointed out there was also some morse code in the layout

amelius 12d ago

If there's a "two stars" solution, then maybe there is also a "three stars" solution?

__atx__ 12d ago
I checked and the solution is unique (at least within some reasonable bounds in terms of runtime etc, it's possible there is a 1000 bits long special solution hidden somewhere, but due to the relatively small amount of flops I doubt it).

xvilka 12d ago

To help with such tasks for real chips (given the good quality images) there is Degate[1][2] open source software. [1] https://www.degate.org/ https://www.degate.org/ [2] https://github.com/DegateCommunity/Degate https://github.com/DegateCommunity/Degate

karelpeeters 12d ago
Degate is even a bit overkill, it is meant for when you only have images of the physical chip. This challenge has the full GDS files, which are the files that are sent to the fab for manufacturing. They still contain information about all of the separate layers. In this case they even contained the stdcell names, making even full transistor and logic function extraction unnecessary.

BalistaCRATZ 12d ago

Nice! I ended up using the KLayout Python API to parse the GDS and extract the netlist, which was actually quite nice to use. Also, yosys has support for doing “assertion checking”, which I used in my solution: https://sunaabh.com/systems/2026/08/18/jspuzzle.html https://sunaabh.com/systems/2026/08/18/jspuzzle.html

swiftcoder 12d ago

I'm not sure I've ever seen such a vicious case of NIH-syndrome. Regardless, congrats on the solve!

_false 12d ago
I first thought you were teasing Jane Street instead of OP. Maybe shows that OP is a good culture fit for Jane Street :)
bluGill 12d ago
Since this was for fun, and the goal was learning at least as much as solving the problem that is just fine. More people should get NIH for those purposes. Now if he is presenting his tools as a good way to solve this problem, something you should use, or any such - that would be a bad thing. Good tools for this are complex and need to be done as part of a large team. If good tools that others should use is the goal then he should join some other group making those tools. I'm sure there is an existing open source project (maybe KiCAD - I'm not in this space so that is the only name I can come up with but maybe their goals are different?) that does this and would welcome more help.

mring33621 12d ago

I love this person!

dahshanlabs 12d ago

nice one

fabflying 12d ago

So good

motoxpro 12d ago

So cool to see someone who loves challenges. Congrats!

AlDante2 12d ago

Hi Chris, just for info: https://en.wikipedia.org/wiki/GDSII https://en.wikipedia.org/wiki/GDSII will tell you about the GDS format. It apparently stands for Graphic Data System II (originally developed by Calma in the late 1970s).

anitil 12d ago
No spoilers! But thanks I did find out after I published, I just thought it was funnier not to know while I was working on it

ctippett 12d ago

> I ended up using a tool called ‘z3’. It’s kind of magical? Every time it finds a solution I get a surge of joy. This resonates so much. I had a similar feeling after going to my very first operations research lecture. Solving seemingly incomprehensibly complex problems by framing them as a bunch of simple constraints and getting a solution seemed like such magic.

darksaints 12d ago
Yeah this was my experience too. I have an undergrad business degree, but got nerd sniped by an optimization problem, found a solution with constraint programming, and ended up going down a 15 year operations research rabbit hole with it. Many people say that the way to tackle a hard problem is to break it down into smaller problems. I disagree. The best way to tackle a hard problem is to break it down into a defined search space and as many seemingly-redundant constraints as you can possibly list, then dump it all into a solver, go take a nap for a few hours or possibly a month, then come back to the problem solved for you.
- chamomeal 12d ago
  Found minizinc/CP-SAT recently and I’m obsessed
vismit2000 11d ago
z3 or constraint programming comes in very handy in at least one challenge every year in Advent of Code! https://adventofcode.com https://adventofcode.com

eru 12d ago

Weren't you supposed to wait until the submissions close to publish spoilers? (Or did they close yesterday?)

moebrowne 12d ago
> Submissions close on September 4th, 2026. https://blog.janestreet.com/can-you-reverse-engineer-an-asic/ https://blog.janestreet.com/can-you-reverse-engineer-an-asic...
anitil 12d ago
I emailed them and asked as I'm in Sydney and didn't want to mess it up - they said to wait until the end of my workday, so I posted it at roughly 5:30 my time. I hope I didn't spoil it!
- eru 11d ago
  Their logistics were a bit weird: they asked not to post spoilers, but also ask you to link to your write-up. In any case, I had it all worked out already. But looking at other people's submissions today showed me that I found some easter eggs other hadn't. That was encouraging. (And I missed some that others found, of course.)
  - deleted 11d ago
    [deleted]
  - anitil 9d ago
    I was confused about that too - I ended up posting an empty page to generate the link ahead of time (and hoping that it wouldn't get picked up by anything), then actually posting the solution later. I also realised I'd missed a lot of easter eggs, like the morse code - I wish I'd spotted that!

aavshr 12d ago

There's a typo on your link to the two stars image. It should be `/img/two-stars.png` instead it's right now `/img/two-starts.pgn`. For those interested in the image itself: https://jestoph.com/img/two-stars.png https://jestoph.com/img/two-stars.png

hosel 12d ago
oh boy here we go again
anitil 12d ago
Oh no! Thanks for that, I must have read it 10 times before posting but somehow didn't spot that it was wrong

skr3178 12d ago

Solving the puzzle with the assistance of a lower capability LLM model (even though I had access to more) turned out to be fun and good learning experience.

Taurenking 12d ago

[dead]

emptyheaded 12d ago

reading the post felt like going down an authentic manic rabbit hole, thanks for sharing your artisanal words @anitil

anitil 12d ago
You're very welcome!

thisisauserid 12d ago

I know nothing about z3 but it's from Microsoft. Would Google's OR-Tools component CP-SAT also be useful for something like this?

myng111 12d ago
Z3 is an SMT solver, not a SAT solver. You'd probably be looking for something more like Yices, Bitwuzla, cvc5, etc.
- karelpeeters 12d ago
  In general that's true, but to reason about boolean circuits like in this challenge we only need a SAT solver. Z3 is just used for it's convenient API.
nostrebored 12d ago
z3 is also just so thoroughly optimized that even if your formulation of the constraints is inefficient it is faster. it is a great library that lets you solve pretty complicated DP problems with a few dozen lines of code.

mdritch 12d ago

I love z3. I used it for the first time for Jane Street's puzzle last year involving a hashing alg disguised as a neural network. I use a lot of MCMC at work and I have made a few small investigations into MCMC model formal verification via z3, but nothing real yet. This has inspired me to pick that back up.

kachnuv_ocasek 12d ago
Can you share more about the connection between MCMC and SAT/SMT? That's a crossover I never thought I'd see.
- mdritch 12d ago
  Sure! Roughly we are using hierarchical models for reads on underlying count or prevalence data. We use those higher-order means or other fit params to kick off remediation tasks at different levels of that hierarchy depending on those higher level params. We assume some correlation between sibling nodes in that hierarchy. Question: Can one or another of those thresholds in sibling or parent nodes ever be met if some number of the samples are below some floor reading? Or, how many zeros does it take to silence a threshold check on the node itself, a sibling, or a parent? To make this tractable I have tried gridding fit parameters, freezing randomness, and using simplified algs like original Metropolis-Hastings

deleted 12d ago

[deleted]

chermi 12d ago

Aspirational. This is how I want to spend my available time.

josu 12d ago

I gave the problem to chatGPT 5.6 Sol Pro and this was the result: > Worked for 12m 36s > Solved https://chatgpt.com/s/t_6a9aed0b09988191b0f2850dee056b48 https://chatgpt.com/s/t_6a9aed0b09988191b0f2850dee056b48 Edit: It didn't independently solve it. > 1. Used the public reconstruction to obtain the recovered RTL/constraint structure, including the 11×11 region map and the fact that it is a two-stars-per-row/column/region, non-touching puzzle. > 2. Then independently wrote and ran my own exhaustive solver against that recovered constraint system.

karelpeeters 12d ago
Looks like it did not actually solve it, but instead it just found an existing solution at https://github.com/NotCleo/GDS-to-RTL https://github.com/NotCleo/GDS-to-RTL and verified parts of it? I have no doubt that modern agents can solve challenges like this even without external help, but you should at least briefly look at the output before posting it online!
- josu 12d ago
  Thanks for pushing back, I've edited my initial post. I misinterpreted the response, I thought that it only referenced the solution as verification.
- deleted 12d ago
  [deleted]

aatd86 12d ago

I don't think I can ever be motivated by such challenges. It's either I'm getting up to speed to the state of the art from the very basics and then I can try to figure out if something was missing along the way or solve unsolved useful problems, or I will not be interested. I just can't tinker for the sake of tinkering. Too goal oriented I guess. Just me? (that is also why school started to bore me right before high school and why I learn better on my own, I did go too College but thank god I didn't do CompSci or that would have disgusted me...)

anonymousDan 12d ago

Interesting that they have their own open-source OCaml toolchain for chip design. I thought received wisdom was that everyone in industry is still tied to horrendous vendor toolchains. Is this a realistic alternative for production-grade chip design?

vzcx 12d ago
Hardcaml compiles to verilog and then you use the horrendous vendor toolchains.

ngriffiths 12d ago

Oh no The neural net engineering challenge was so awesome, I got really into it, spent way too much time and then was shocked when I actually managed to solve it. Since then I've gotten interested in... hardware. God help me

siramikvarze 12d ago

[dead]

paretolaw 12d ago

I got one better puzzle. Predict Jane algo moves when they try to manipulate market and frontrun their orders. Let them taste their own medicine. :)

userbinator 12d ago

I'm probably not exaggerating if I say that the majority of people on the planet who have the knowledge and skills to easily do this, and are doing it for a living, are in the Far East.

seobotaicom 9d ago

Do you think constraint solvers like Z3 are underused by programmers, or does this kind of problem just happen to be a particularly good fit for them?