alt Hacker NewsSolving the Jane Street reverse engineering challenge
Comments
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.
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...
To help with such tasks for real chips (given the good quality images) there is Degate[1][2] open source software.
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
I'm not sure I've ever seen such a vicious case of NIH-syndrome. Regardless, congrats on the solve!
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
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?
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).
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'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.
Weren't you supposed to wait until the submissions close to publish spoilers?
(Or did they close yesterday?)
Aspirational. This is how I want to spend my available time.
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.
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?
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...)
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)
So cool to see someone who loves challenges. Congrats!
I love this person!
reading the post felt like going down an authentic manic rabbit hole, thanks for sharing your artisanal words @anitil
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
> 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. :)
[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 got one better puzzle. Predict Jane algo moves when they try to manipulate market and frontrun their orders.
Let them taste their own medicine. :)
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
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.
> 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.