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.
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?
Yeah I briefly considered switching to a simulator to get the final output, but then luckily realized the Z3 problem 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 and SymbiYosys website at 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.
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. :)
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.
A lot of companies who claim to want highly intelligent and autonomous engineers by revealed preference actually want glorified slightly above average ticket pushers.
At least by the looks of it, Jane Street appears to be an odd one to genuinely value competence.
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.
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.
> 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/ . Could be a bit of an infohazard, but I think journey is the goal and yours was certainly more educational :)
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.
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.
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.
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...
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.
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.
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
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 ..
Also, yosys has support for doing “assertion checking”, which I used in my solution: https://sunaabh.com/systems/2026/08/18/jspuzzle.html
[1] https://www.degate.org/
[2] https://github.com/DegateCommunity/Degate
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 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...
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 and SymbiYosys website at 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.
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. :)
At least by the looks of it, Jane Street appears to be an odd one to genuinely value competence.
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...
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/ . Could be a bit of an infohazard, but I think journey is the goal and yours was certainly more educational :)
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.
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
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.
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!
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...
I'd like to do a full writeup but haven't had the time.
These GDS design files have a lot more structure to them.