Jane Street Puzzle Solution: Can you reverse engineer an ASIC?

In August 2026, Jane Street announced an interesting hardware reverse-engineering puzzle. In essence, participants were asked to reverse engineer a circuit from its physical layout in GDSII format, with little other information about the design apart from a few hints that made much more sense in retrospect. The challenge is described here: Can you reverse engineer an ASIC?.

To make the task more approachable, Jane Street also provided a warm-up puzzle in the same format. Its repository includes the original Verilog, synthesized netlists, a post-place-and-route DEF file, and the final GDS. Those intermediate artifacts make it possible to study the flow and test extraction tools against a known design.

Interestingly, the challenge happened to align closely with two items on my ever-growing backlog. I have always wanted to learn how to get from a mask layout back to a working circuit, but as always, the projects like that tend to be buried under more urgent day-to-day firefighting. This sounded like the perfect opportunity to try it. And I did.

The challenge sounds relatively simple: here is a GDS file; what does the circuit do?

This is the reverse of the usual chip-design process: here is the circuit; now produce the physical layout for tape-out. Although there are practical reasons to go the other way, such as verification and reverse engineering, most chip design follows the traffic from circuit to layout.

From a bird's-eye view, the circuit-to-GDS pipeline resembles software compilation: it progressively removes human-friendly structure while preserving what is needed to implement the design. Here, we need to travel in the opposite direction. As in software reverse engineering, the exact original source cannot generally be recovered from the result, but enough logic can be reconstructed to understand the behavior.

GDSII is a binary layout format. It stores a hierarchy of structures containing geometric elements such as polygons, paths, and text, together with placement transforms and layer information. Those layout layers are later mapped and processed into fabrication masks.

Producing the GDS file is one of the final steps in the chip-design flow. It is sent for tape-out and used to prepare the fabrication masks. GDSII is a widely supported format, with open-source tools available for viewing it. One of them, suggested by Jane Street, is KLayout. A quick inspection of the puzzle file revealed a chip-like structure and a visual watermark left by the designers, confirming what had already been shown in the challenge post.

I began with the warm-up puzzle and coding agents. Because the warm-up puzzle included every stage from the circuit description to the final GDS file, I used coding agents to develop a tool that reversed the pipeline. Each reverse step was checked against its forward counterpart in the warm-up, which proved invaluable for debugging.

The tool could have been written in any language, but I used Rust for the reference implementation and DeepSeek V4 Flash for most of the agent work, with other models for some harder parts. It was not a "Hello, World!" task, but it was not cosmically hard either. After many prompts, errors, and iterations, the pipeline had four main stages:

• Parse the GDS records, resolve the cell hierarchy, and apply placement transforms.
• Recover top-level port names from GDS TEXT labels.
• Extract nets from routing geometry, cell-pin geometry, and vias.
• Identify SKY130 standard-cell instances and emit a gate-level netlist.

The pipeline emitted Verilog for both the warm-up and the main puzzle. Running iverilog -tnull confirmed that the generated files parsed and elaborated with the cell models. That sounded too good to be true, and it was. An unexpected turn followed soon afterward.

Once I had a netlist of SKY130 standard cells, I could simulate the warm-up. The main puzzle was harder: how could I extract the answer from its netlist?

The circuit had a serial input, I. At that point I did not know the relevant sequence length, and an unconstrained input bit doubles the brute-force search space at every cycle. I initially expected the puzzle to permit an expensive but practical brute-force search. Knowing the answer now, I can only say: not this time.

Another option was to recover a higher-level representation of the main state machine, but the gate-level netlist made that look nontrivial. Understanding more of the circuit might have narrowed the search space, but I went in another direction: good old formal verification.

Bounded Model Checking (BMC) to the rescue. BMC can answer the question, “Can the circuit reach a given state within N clock steps?” by encoding it as a SAT problem. If success can become 1 within that bound, the solver can also return the input sequence that leads to it. That sequence should be our solution!

I first used Yosys to run BMC on the warm-up puzzle, and it worked like a charm. I then repeated the process on the main puzzle, which appeared to solve it: I had success == 1 and an input sequence that led to that state. However, a quick inspection of the waveforms revealed that the resulting output string, supposedly the desired solution, was garbage.

It turned out that our layout-extraction tool was not prepared for several special cases present in the main puzzle but largely absent from the warm-up puzzle. Surprise, surprise. At one point, the extracted model contained 26 undriven logic-input pins, which Yosys could treat as unconstrained and assign whatever values helped satisfy the target condition. It was an underconstrained-model problem. We had success == 1, but the input trace was not valid for the intended circuit and produced a garbage output string. Many similarly spurious traces could reach success == 1.

Back to the drawing board, or rather, the layout. This was the point at which I showed the GDS to the LLM so that I could debug and improve the netlist-extraction tool. What followed was a back-and-forth session involving the LLM, visual inspection, and my own knowledge to guide the investigation. Eventually, we found the following:

• In the layout, all 84 resettable dfrtp cells were disconnected from the top-level rst_n net. The warm-up showed the same pattern while also providing the source netlist as an oracle. I therefore reconnected those reset pins to rst_n and fixed the tool to deal with that edge case.
• The puzzle uses eight additional flops from two cell families: four dfxtp cells with no reset pin and four dfstp cells with an asynchronous set rather than a reset and had 'x' propagating. The gate model were replaced for those cases with a special their model cell where the initial state is fixed.
• One input pin, u_a311o_2_3326.A1, remained genuinely driverless in the extracted mask. BMC runs at the winning bound produced the same winning behavior when it was tied to 0, tied to 1, or left free, so it was not an issue for the result. It was tied to 0 for the final solution to maitain detrminicity.

After those fixes, BMC produced an input trace whose output stream was coherent and reproducible. That was the solution. One successful Yosys run took about seven seconds, which is remarkable compared with the number of explicit input traces that could be simulated in the same time.

One important disclosure: I showed the puzzle’s GDS file to an LLM, so I cannot claim that the solution was AI-free. The debugging effort required to find and fix the missing edge cases in the netlist extractor was so intensive that I am not sure how long the same work would have taken without LLM assistance. It certainly would have taken much, much longer. On the positive side, all the fixes were incorporated into the tools, so the pipeline can now run without further intervention for both tested cases (N = 2): the warm-up and the main puzzle. That, however, does not change how it was developed.

Jane Street raided my backlog again. This time, my notes pointed to a paper led by Ryan Babbush et al., Securing Elliptic Curve Cryptocurrencies against Quantum Vulnerabilities: Resource Estimates and Mitigations. The paper demonstrates a useful pattern: prove possession of a hidden artifact and show that it passes a checker without revealing the artifact itself. That sounded useful for this puzzle.

The precise goal was to prove possession of a winning trace for a committed model without revealing the trace, answer string, or winning step. More precisely:

There exists a per-cycle input stream W such that stepping the committed model N from an all-zero initial state makes success == 1 at some step. W, its length, the success step, and all output bytes remain private.

N is the compact binary circuit model that the proof simulates. It is produced by converting the repaired netlist to BTOR2 and then to the binary format consumed by the checker. Only its SHA-256 fingerprint, H(N), is public.

The checker runs a Rust program inside SP1, a RISC-V zero-knowledge virtual machine. It receives the model and input stream privately, starts the model from its all-zero state, and executes the hidden number of steps. The execution fails unless success becomes 1 during at least one of those steps. A Groth16 proof over the BN254 curve makes the final result small and zero-knowledge.

This resembles the architecture used in the Google paper. Google’s checker evaluates a hidden reversible circuit using pseudorandom tests derived from that circuit. Here, the hidden input stream is itself the witness, and the checker performs one sequential replay. The checker is win-only: a proof can complete only if success becomes 1.

The checker’s committed public output is exactly 36 bytes: 32 bytes for H(N) and four bytes for PASS = 1. The witness length, success timing, and output bytes are not committed. The resulting proof verified successfully. Tamper tests confirmed that a one-byte change to the proof is rejected during Groth16 verification and that a change to the guest ELF is rejected by the ELF-to-program-key binding. The complete public ZKP verification bundle can be downloaded here.

Verification has two automated steps:

1. Run bash build_guest.sh to rebuild the checker using the pinned SP1 Docker toolchain and require byte equality with guest.elf.
2. Run bash verify3.sh to derive the verification key from guest.elf, require exactly 36 public bytes, and cryptographically verify the Groth16 proof against the published pins.

The logs provide optional supporting evidence. win_v3_prove.log contains a sanitized record of the original proving run, while tamper_v3.log records the expected rejection of modified proof and ELF artifacts. You can also audit guest_source/main.rs and guest_source/stepper_lib.rs to understand the statement and transition semantics enforced by the program.

It is worth noting that the ZK pipeline begins only after the GDS has been reverse engineered into a repaired netlist:
netlist -> BTOR2 -> serialized core N

The proof binds the witness to H(N), but it does not prove that N was faithfully derived from the public GDS. In principle, a prover could construct a different model in which success trivially becomes 1, commit to that model, and prove a witness for it. Publishing H(N) prevents the model from being replaced after it has been committed, but it does not establish the model’s origin.

This is a major limitation of the current approach as an end-to-end proof of the puzzle’s solution.

This ZKP was built as a quick experimental prototype to demonstrate the feasibility of the approach. It has not been formally audited and may still contain issues that need to be addressed.

1. Developing a GDS-to-netlist extraction tool was manageable, but this was a relatively simple circuit. Similarly, building a SystemVerilog compiler for a small, targeted subset of the language is not too difficult; the real challenge is handling all the edge cases. The same applies here, so the complexity of building a general-purpose extraction tool should not be underestimated.
2. Interestingly, if I were designing such a puzzle, my instinct would be to make the solution discoverable through brute force, even at a significant computational cost. This puzzle took a different route.
3. BMC does not overfit, but an underconstrained model can produce misleading results. If the solver is free to choose the values of undriven pins, it can make the circuit do almost anything.
4. Fixing the corner cases in the GDS-to-netlist extraction took considerable effort, even with LLM assistance.
5. Formal verification is an incredibly powerful tool. Finding a counterexample, which in this case was the solution, in about seven seconds was mind-blowing compared with the time a brute-force search would have required.
6. The authors hinted that special attention should be paid to reset behavior, considering how the input sequence worked. Surprisingly, handling reset as part of the input was no issue for BMC, though it would likely have been a headache for a brute-force search.
7. BMC “dislikes” x values or, more precisely, unknown and undriven signals made the model underconstrained, allowing the solver to choose values that the intended circuit would never produce. The solver did its job; the model was the problem.
8. The ZKP took considerably longer to generate, which was unsurprising because it was run on a good old CPU.

Overall, it was an interesting challenge. It motivated me to continue developing more general end-to-end tools for reverse engineering GDS layouts and generating zero-knowledge proofs of circuit behavior.