Solving the Jane Street reverse engineering challenge

Posted by anitil 4 days ago

Counter437Comment99OpenOriginal

Comments

Comment by ctippett 4 days ago

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

Comment by darksaints 4 days ago

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.

Comment by chamomeal 4 days ago

Found minizinc/CP-SAT recently and I’m obsessed

Comment by vismit2000 3 days ago

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

Comment by mdritch 4 days ago

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.

Comment by kachnuv_ocasek 4 days ago

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

Comment by mdritch 4 days ago

Sure! Roughly we are using hierarchical models for reads on underlying count or prevalence data. We use those higher-order means or other fit params to kick off remediation tasks at different levels of that hierarchy depending on those higher level params. We assume some correlation between sibling nodes in that hierarchy.

Question: Can one or another of those thresholds in sibling or parent nodes ever be met if some number of the samples are below some floor reading? Or, how many zeros does it take to silence a threshold check on the node itself, a sibling, or a parent?

To make this tractable I have tried gridding fit parameters, freezing randomness, and using simplified algs like original Metropolis-Hastings

Comment by xvilka 4 days ago

To help with such tasks for real chips (given the good quality images) there is Degate[1][2] open source software.

[1] https://www.degate.org/

[2] https://github.com/DegateCommunity/Degate

Comment by karelpeeters 4 days ago

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.

Comment by anitil 4 days ago

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

Comment by __atx__ 4 days ago

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

Comment by pgn 3 days ago

> It's likely that this would now require actually reverse engineering the circuit subcomponents, but that is an entire rabbit hole I do not have time to go down at this point.

This is the route I ended up going! I posted my own writeup here: https://pradyun.net/blog/reverse_engineering.html

Comment by anitil 4 days ago

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.

Comment by make3 3 days ago

Doing things the hard way is a lot of times "male" bravado (though this is not limited to males in any way ofc), this is a very common thing in junior engineers.

Curiosity is good but maturity is trusting that the problem will get hard at some point anyways, that improving the most efficient way is usually also interesting and is more likely to deliver desired things on time or at all, which can be a big deal if what you're trying to deliver it worth it, like.. a new MRI machine that detects new types of cancers, etc.

If you don't care about what you're trying to deliver, that's another problem that requires at least some questioning, though I understand people have families to take care of etc.

Comment by sota_pop 3 days ago

Are you me? EE, always manage to go the hard route (inadvertently)…

Comment by vzcx 4 days ago

Nice solution and good easter egg find!

Comment by NamTaf 4 days ago

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

Comment by gjm11 4 days ago

That particular one may be no longer a thing, but there are definitely still plenty of puzzle hunts going on. See e.g. https://en.wikipedia.org/wiki/Puzzle_hunt which has a list.

Comment by vzcx 4 days ago

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.

Comment by __atx__ 4 days ago

> Circuit extraction can be done with magic.

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

Comment by vzcx 4 days ago

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.

Comment by anitil 4 days ago

> Incredible amount of determination

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!

Comment by optimisticestim 1 day ago

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/

Comment by swiftcoder 4 days ago

I'm not sure I've ever seen such a vicious case of NIH-syndrome. Regardless, congrats on the solve!

Comment by bluGill 4 days ago

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.

Comment by _false 4 days ago

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

Comment by BalistaCRATZ 4 days ago

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

Comment by aavshr 4 days ago

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

Comment by anitil 3 days ago

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

Comment by hosel 4 days ago

oh boy here we go again

Comment by ngriffiths 4 days ago

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

Comment by AlDante2 4 days ago

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

Comment by anitil 4 days ago

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

Comment by anonymousDan 4 days ago

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?

Comment by vzcx 4 days ago

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

Comment by karelpeeters 4 days ago

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

Comment by anitil 4 days ago

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?

Comment by karelpeeters 4 days ago

Yeah I briefly considered switching to a simulator to get the final output, but then luckily realized the Z3 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.

Comment by amelius 4 days ago

If there's a "two stars" solution, then maybe there is also a "three stars" solution?

Comment by __atx__ 4 days ago

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

Comment by seobotaicom 1 day ago

Do you think constraint solvers like Z3 are underused by programmers, or does this kind of problem just happen to be a particularly good fit for them?

Comment by gyanchawdhary 4 days ago

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

Comment by bux93 4 days ago

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

Comment by gyanchawdhary 4 days ago

wow thanks for sharing, will check it out

Comment by Andrew-Koper 4 days ago

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

Comment by eru 4 days ago

Weren't you supposed to wait until the submissions close to publish spoilers?

(Or did they close yesterday?)

Comment by moebrowne 4 days ago

> Submissions close on September 4th, 2026.

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

Comment by anitil 3 days ago

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!

Comment by eru 3 days ago

Their logistics were a bit weird: they asked not to post spoilers, but also ask you to link to your write-up.

In any case, I had it all worked out already. But looking at other people's submissions today showed me that I found some easter eggs other hadn't. That was encouraging. (And I missed some that others found, of course.)

Comment by anitil 1 day ago

I was confused about that too - I ended up posting an empty page to generate the link ahead of time (and hoping that it wouldn't get picked up by anything), then actually posting the solution later.

I also realised I'd missed a lot of easter eggs, like the morse code - I wish I'd spotted that!

Comment by 3 days ago

Comment by aatd86 4 days ago

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

Comment by userbinator 4 days ago

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.

Comment by dhzzwgzua 4 days ago

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)

Comment by anitil 3 days ago

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

Comment by charcircuit 4 days ago

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.

Comment by anitil 4 days ago

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

Comment by marethyu 4 days ago

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

Comment by vzcx 4 days ago

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.

Comment by chermi 4 days ago

Aspirational. This is how I want to spend my available time.

Comment by skr3178 4 days ago

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.

Comment by 4 days ago

Comment by thisisauserid 4 days ago

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?

Comment by nostrebored 4 days ago

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.

Comment by myng111 4 days ago

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

Comment by karelpeeters 4 days ago

In general that's true, but to reason about boolean circuits like in this challenge we only need a SAT solver. Z3 is just used for it's convenient API.

Comment by motoxpro 4 days ago

So cool to see someone who loves challenges. Congrats!

Comment by mring33621 4 days ago

I love this person!

Comment by emptyheaded 4 days ago

reading the post felt like going down an authentic manic rabbit hole, thanks for sharing your artisanal words @anitil

Comment by anitil 3 days ago

You're very welcome!

Comment by fabflying 4 days ago

So good

Comment by dahshanlabs 4 days ago

nice one

Comment by piker 4 days ago

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

Comment by bko 4 days ago

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.

Comment by vovavili 4 days ago

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.

Comment by bluGill 4 days ago

There are a lot of incredibly smart non-autists. Or maybe slightly autistic, but enough awareness of the real world that they can be managed.

Comment by Emma_Goldman 4 days ago

The strong affinity between autism and intelligence seems strongest in technical fields, and engineering and computer science in particular. Autism does not seem to be over-represented to anywhere near the same degree in many other domains that are full of intelligent people.

Comment by skinfaxi 4 days ago

Is this just from your direct experience or do you have data to back that up? Are you talking about credentialed engineering like mechanical or civil engineering or just software developers?

Comment by strken 4 days ago

https://pmc.ncbi.nlm.nih.gov/articles/PMC9058071/ (if "strong affinity" means "bimodal distribution and I ignore the lower pole")

https://pubmed.ncbi.nlm.nih.gov/38497251/ (if "engineering and computer science" means "IT")

I don't know if it's actually true but the idea is interesting.

Comment by Emma_Goldman 4 days ago

There's plenty of data on the clustering of high-functioning autistic workers in engineering and computer science, and the massively disproportionate share of autistic children with fathers and grandfathers in those fields. I work across technical and non-technical academic fields and the difference is quite obvious. It also follows naturally from some of the common presentations of autism, e.g., the high co-occurrence of dyslexia.

Comment by ambicapter 4 days ago

There's this trend on the internet to attribute success at any remotely technically challenging problem to the glorious power of autism.

Comment by bob1029 4 days ago

Good mentorship can make all the difference in the universe.

Comment by karmakurtisaani 4 days ago

I can be a glorified slightly above average ticket pusher, where do I sign up for a million per year job?!

Comment by Hydraulix989 4 days ago

> A lot of companies who claim to want highly intelligent and autonomous engineers by revealed preference actually want glorified slightly above average ticket pushers.

No. FAANG companies and quant firms want people who are independent and self-directed, not people who need to be told what to do.

Comment by folkrav 4 days ago

Please, explain how you determined this person was an "extremely smart autist".

Comment by anitil 4 days ago

I took it as a compliment!

Comment by folkrav 4 days ago

I find it hard to believe that saying autistic people are "incredibly hard to manage", that managing them is like "herding cats" and their presence is a "huge liability to the org" is anywhere near complimentary. Autism presents in thousands of ways, and the portrayal is, at best, caricatural.

Comment by bko 4 days ago

Okay dude, don't need to white knight autists. There's a particular archetype of extremely intelligent and technical yet socially unaware or prickly people that's not unfounded in reality. These are the people who do incredible feats. You need a degree of unagreeableness and arrogance to go against the grain and accomplish great things.

It's a thing, I assure you. And it's pretty common parlance in online / technical culture. We don't need to word police this thing.

Comment by walrus01 4 days ago

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.

Comment by verteu 4 days ago

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

Does Jane Street really pay that much? Of course 7 figures is possible, but these median comps seem lower than FAANG (and with much higher workload): https://www.levels.fyi/companies/jane-street/salaries/softwa...

Comment by siramikvarze 4 days ago

[dead]

Comment by zeninkhan 4 days ago

[dead]

Comment by Taurenking 4 days ago

[dead]

Comment by paretolaw 4 days ago

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

Comment by anon-3988 4 days ago

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.

Comment by seritools 4 days ago

> Personally, I did not learn that much from that experience.

What did you expect?

Comment by anon-3988 4 days ago

I understand the sentiment, but in a world where these kinds of problems (And problems at work) that can trivially be solved by LLMs; what kind of value can I provide?

That itself is a learning experience. What is even the point of technical interview questions or take home questions? This means that I am now open to hiring completely non-technical person, as long as they have a good personality and management skills more than a competent developer.

Comment by chermi 4 days ago

"I understand the sentiment, but in a world where these kinds of problems (And problems at work) that can trivially be solved by LLMs; what kind of value can I provide?"

This is sad conclusion. Maybe you're more right than wrong, but my answer to the "value" question would be:

Solving even harder problems based on lessons from solving easier ones? Pretty similar to the trajectory in this blog post. Perhaps aided additionally by llms and other tools that can solve the subproblems so you can focus on the less obvious/automatable aspects of the problem?

But note the tension, only by being involved in the problem solving to some extent do you become better at it. So if your default is to say "An LLM can or will soon be able to solve it, why bother?", then your situation will become more desperate and your outlook more negative in a self-reinforcing way.

Comment by gnyman 4 days ago

The fact that agents can solve these is telling and the Infosec Capture The Flag community is trying to figure out how to approach.

I recently solved a (in)famously hard challenge (disobey conference hacker ticket) more or less by accident. I say by accident because I have always ignored this challenges as they generally require a lot of patience and motivation to solve. Some years they haven't been solved at all. This year I had a GPT sub with some unused quota so I thought let's see how far it gets.

And it crunched through the whole thing in an evening and morning (occasional poking from me to keep going and steer it right).

Like anon, I learned nothing except that the agents have become really good at solving puzzles. Last time I had thrown a puzzle on them was Advent of code, with GPT3 I think and it struggled so much I gave up my experiment on day 7 or something.

Comment by yuye 4 days ago

>I have used Codex (Sol 5.6 or whatever) to solve this problem.

>Personally, I did not learn that much from that experience

Fire is hot, water is wet, etc

Comment by topham 4 days ago

If learning is the point then obviously that was a missed opportunity.

If success was the intent, then it's a win.

While challenges are fun, sometimes the requirement is simply to achieve the end goal, with no other point than that.

If your job is to stop terrorists, and that includes hacking into a system and extracting their plans, the "fun" of it isn't the point, only the end goal it's important. Sometimes when we do things like this for fun we forget that someone else out there absolutely needs to achieve the result and doesn't care how it's achieved.

It's the part of penetration testing some people miss. (It's not generally a fun job, almost everyone I know that did it got out as soon as possible. They weren't solving problems, they just running audit scripts and generating reports.)

Comment by josu 4 days ago

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.

Comment by karelpeeters 4 days ago

Looks like it did not actually solve it, but instead it just found an existing solution at https://github.com/NotCleo/GDS-to-RTL and verified parts of it?

I have no doubt that modern agents can solve challenges like this even without external help, but you should at least briefly look at the output before posting it online!

Comment by josu 4 days ago

Thanks for pushing back, I've edited my initial post. I misinterpreted the response, I thought that it only referenced the solution as verification.

Comment by 4 days ago