Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- If there's a "two stars" solution, then maybe there is also a "three stars" solution?by amelius
- 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).by __atx__
- 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...
by karelpeeters - 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?by anitil
- 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?by anonymousDan
- Hardcaml compiles to verilog and then you use the horrendous vendor toolchains.by vzcx
- 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).
by AlDante2 - 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 itby anitil
- 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
by ngriffiths - 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
by aavshr - oh boy here we go againby hosel
- Oh no! Thanks for that, I must have read it 10 times before posting but somehow didn't spot that it was wrongby anitil
- 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
by BalistaCRATZ - I'm not sure I've ever seen such a vicious case of NIH-syndrome. Regardless, congrats on the solve!by swiftcoder
- I first thought you were teasing Jane Street instead of OP. Maybe shows that OP is a good culture fit for Jane Street :)by _false
- 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.
by bluGill - 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...
by anitil - 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/
- 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.
by vzcx - 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.
by NamTaf - > 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 :)
by __atx__ - To help with such tasks for real chips (given the good quality images) there is Degate[1][2] open source software.by xvilka
- 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.by karelpeeters
- 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.by mdritch
- Can you share more about the connection between MCMC and SAT/SMT? That's a crossover I never thought I'd see.
- > 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.
by ctippett - z3 or constraint programming comes in very handy in at least one challenge every year in Advent of Code! https://adventofcode.comby vismit2000
- 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.
by darksaints