Solving the Jane Street reverse engineering challenge (jestoph.com)

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.

z3 or constraint programming comes in very handy in at least one challenge every year in Advent of Code! https://adventofcode.com

Can you share more about the connection between MCMC and SAT/SMT? That's a crossover I never thought I'd see.

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.

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.

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

> 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 :)

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/

I first thought you were teasing Jane Street instead of OP. Maybe shows that OP is a good culture fit for Jane Street :)

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.

oh boy here we go again

Oh no! Thanks for that, I must have read it 10 times before posting but somehow didn't spot that it was wrong

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

Hardcaml compiles to verilog and then you use the horrendous vendor toolchains.

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?

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).

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

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

> Submissions close on September 4th, 2026.

https://blog.janestreet.com/can-you-reverse-engineer-an-asic...

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!

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

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.

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

I tried and ChatGPT 5.6 managed to figure out the answer within an hour.

Z3 is an SMT solver, not a SAT solver. You'd probably be looking for something more like Yices, Bitwuzla, cvc5, etc.

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.

You're very welcome!