alt Hacker NewsSolving the Jane Street Reverse Engineering Challenge
Comments
> 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. :)
> 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.
To help with such tasks for real chips (given the good quality images) there is Degate[1][2] open source software.
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
Aspirational. This is how I want to spend my available time.
I'm not sure I've ever seen such a vicious case of NIH-syndrome. Regardless, congrats on the solve!
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
Hi Chris,
just for info: 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).
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...
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/dba417c2690cf0505ac9079...
If there's a "two stars" solution, then maybe there is also a "three stars" solution?
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?
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.
Weren't you supposed to wait until the submissions close to publish spoilers?
(Or did they close yesterday?)
reading the post felt like going down an authentic manic rabbit hole, thanks for sharing your artisanal words @anitil
So cool to see someone who loves challenges. Congrats!
I love this person!
So good
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 ..
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.
nice one
[dead]
[dead]
[dead]
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.
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.