# AES in 106 gates: what Swapnil Jain's new circuit records beat, and what Lean checked

> Satyajit Ghana — Head of Engineering @ Inkers Technology
> canonical: https://ai.thesatyajit.com/articles/aes-circuits-lean
> date: 2026-10-11
> tags: security, formal-methods, algorithms, math, hardware, verifiers

Swapnil Jain, whose Lean-checked track ran alongside the [integer-multiplication exponent race](/articles/integer-mult-exponent-race) earlier this week, posted something with a much more physical subject on 11 October:

> new records for AES, the cipher on billions of chips, beating circuits from 2010: GF(2^8) multiplier: 117 → 112 gates, same depth (−4.3%); S-box: 113 → 106 (−6.2%); Inverse S-box: 121 → 109 (−9.9%). Every circuit is Lean-verified.

Gate-count records for the AES S-box are a small, old, competitive field, and claims in it usually go wrong in one of three places: the gate model (which gates count, and whether a NOT is free), the baseline (which circuit you beat, and whether a newer one already sits lower), and depth (a smaller circuit that is three times deeper is a different product). So I did what the repository invites anyone to do, with my own code instead of the author's. I parsed every circuit in [Swapnil-jain/gf2m-circuits](https://github.com/Swapnil-jain/gf2m-circuits), plus the prior circuits it compares against, simulated each one over all 256 inputs (all 65,536 input pairs for the multipliers) against an S-box and a field multiplication I computed from scratch, and recounted every gate and every level.

The short version: every circuit is correct, and every gate count, depth and AND depth in the papers matches mine exactly. The multiplier claim is right as stated. The two S-box numbers are right too, but "beating circuits from 2010" is the wrong frame for them. In 2026 NIST published a 110-gate forward S-box and a 112-gate inverse in the same gate model, so against the newest circuits the gains are 4 gates and 3 gates, and Jain's smaller circuits are deeper. His paper says all of this in its abstract. The post compresses it away.

<RepoCard repo="Swapnil-jain/gf2m-circuits" />

## Why anyone counts gates in an S-box

AES does four things per round, and three of them are linear over $\mathbb{F}_2$: ShiftRows moves bytes, MixColumns is a fixed matrix, AddRoundKey is XOR. Linear maps are cheap; you can build them from XOR gates alone. The S-box, applied to each of the 16 state bytes every round, is the only nonlinear part. It is inversion in $\mathbb{F}_{2^8}$ (modulus $x^8+x^4+x^3+x+1$, with 0 mapped to 0) followed by a fixed affine map. In a lookup-table implementation none of this matters. It matters wherever the S-box has to be a circuit:

- **Hardware.** An AES core is mostly S-boxes. Fewer gates is less area and less switching power, before the synthesis tool's own effects.
- **Bitsliced software.** Constant-time AES on CPUs without AES instructions evaluates the circuit with one word-wide instruction per gate, across many blocks at once. Every gate is an instruction.
- **Masked implementations**, the standard defence against power and electromagnetic side channels. XOR is nearly free under masking; each AND costs randomness and a quadratic number of share products. Here the number that matters is the AND count, not the total.
- **MPC, garbled circuits, ZK proofs.** With free-XOR garbling and most secret-sharing schemes, XOR costs nothing and each AND costs communication or a constraint. Again, AND count.

Hold on to that split, because it decides who benefits. Jain's records are in total gates. The AND count of his S-box circuits is 32 to 34, the same as the 2010-era circuits, and in 2026 the AND record moved well below that. I come back to this at the end.

The gate model is the one the field has used since Boyar and Peralta: two-input AND, XOR and XNOR, each costing one, free fan-out, no separate NOT gate and no constants, so every negation has to be folded into an XNOR. Depth is the number of gates on the longest input-to-output path. The repository states it in one line (`sbox/README.md:44`): "Gate model: \{AND, XOR, XNOR\}, cost 1 each, no NOT." That is also the model of the circuit he compares against, which matters: some famous S-box results use NAND, NOR, MUX or free inverters, and you cannot compare across models.

## The shape every small S-box shares

Almost every small AES S-box circuit since 2010 has the same skeleton, which Jain calls the Boyar–Peralta layout. It rests on Canright's tower-field idea: write a byte $A$ as $a_0 b_0 + a_1 b_1$ over a basis of $\mathbb{F}_{2^8}$ over $\mathbb{F}_{2^4}$, and inverting in the big field reduces to inverting a single 4-bit element, the norm $X = A^{17}$.

The circuit then has three parts. A **top** layer of XORs computes 18 linear forms of the input bits. A nonlinear **middle** multiplies pairs of those forms (9 ANDs), sums them into the four bits of the norm, and inverts the norm in $\mathbb{F}_{2^4}$ (5 more ANDs). A **bottom** multiplies the inverse back against the same 18 forms (18 ANDs) and finishes with a linear layer that also absorbs the AES affine map. That gives the famous $9 + 5 + 18 = 32$ ANDs. Everything else is XOR, and almost all the fighting over the last fifteen years has been over how few XORs the top and bottom layers can share.

You can see the shape in the circuit Jain is beating. The Circuit Minimization Team (CMT) page publishes a rendering of its 113-gate S-box. Yellow nodes are XOR, red are AND, and each label gives the node's level and its distance to the output:

<Figure src="https://ai.thesatyajit.com/articles/aes-circuits-lean/fig1.png" alt="A tall node-link drawing of a Boolean circuit. Inputs x0 to x7 enter at the top. A band of yellow XOR nodes labelled y1 to y21 and t0 to t1 forms the top linear layer, and below it red AND nodes such as t2, t3, t5, t7, t8 and t10 to t15 start appearing among further yellow nodes as the drawing continues downward." caption="The top third of the 113-gate AES S-box on the CMT page: the linear top layer (yellow, XOR) and the first multiplications (red, AND). Each node is labelled name:level,distance-to-output (Circuit Minimization Team, AESBoxVerbose.pdf, cropped)." />

Jain's own dissection of where the gates sit makes the point sharply. In every circuit the AND budget is identical. The savings are all in the XOR plumbing around it:

<Figure src="https://ai.thesatyajit.com/articles/aes-circuits-lean/fig3.png" alt="A table with columns Circuit, Top, MUL1, Inverter, Bottom, Total. BP/Calik 113: 23, 9+16, 5+14, 18+28, 113. Our 110 (110/38): 20, 9+17, 5+13, 18+28, 110. 107 (rep. 206, 190, 224, 0): 17, 9+19, 5+13, 18+26, 107. 106 (rep. 85, 130, 12, 1): 19, 9+17, 5+13, 18+25, 106." caption="Gate allocation by block for the 113-gate baseline and three of Jain's circuits, with the nonlinear blocks given as AND+XOR. The 32 ANDs never move; the 7 gates come out of the top, inverter and bottom XORs (Jain, AES S-box paper, Table 2)." />

Below is one of the released circuits, running. Pick an input byte and drag the depth: each column is one level, squares are ANDs, circles XORs, dashed circles XNORs, and a filled shape is a 1. The explorer evaluates the gate list from `sbox/circuits/sbox106_d24.json` and compares the eight outputs with an S-box it computes on its own from field inversion and the affine map, so the last line is a real check. Click any gate to see its equation and its value.

<CircuitExplorer />

Two things stand out when you step through it, and both are in the numbers as well. The first AND does not fire until level 7. The top layer of the 106-gate circuit is 19 XORs stacked six levels deep, where the 113's first AND already sits at level 4, because the representation sweep found cheaper forms that happen to be built on each other. And the ANDs come in four waves by AND depth, 9, then 3, then 4, then 18. The first and last waves are the skeleton's 9 and 18; the middle carries 7 instead of 5. The paper's account is that the depth lane's moves can change a gate's type, which is how the 32 ANDs of the sweep circuit became 34 here. For input 0x53 the explorer lands on 0xED, the value FIPS-197 gives as its worked example.

## Which circuit from 2010?

Precision matters most at this point. These are the circuits involved, all in the same gate model, with the counts from my own parse of the files (each matches the paper and, for the NIST files, the counts in the file names):

| Circuit | Where | AND + XOR + XNOR | Gates | Depth | AND depth |
|---|---|---|---|---|---|
| Boyar–Peralta, improved by Calik | CMT page | 32 + 77 + 4 | 113 | 27 | 6 |
| Boyar–Find–Peralta, low depth | CMT page | 34 + 87 + 4 | 125 | 16 | 4 |
| Low depth | NIST repository | 34 + 87 + 4 | 125 | 15 | 4 |
| Smallest forward, 2026 | NIST repository | 32 + 75 + 3 | 110 | 22 | 5 |
| Smallest forward, 2026 | NIST repository | 34 + 73 + 3 | 110 | 22 | 4 |
| Inverse | CMT page | 34 + 83 + 4 | 121 | 21 | 4 |
| Smallest inverse, 2026 | NIST repository | 32 + 71 + 9 | 112 | 26 | 5 |
| **Jain forward** | sbox106_d24 | 34 + 69 + 3 | **106** | 24 | 4 |
| **Jain inverse** | invsbox109_d30 | 32 + 71 + 6 | **109** | 30 | 6 |

The post's 113 is the CMT page's S-box, which the page describes as "an improvement, by Cagdas Calik, of a previous circuit in this page": the Boyar–Peralta circuit, whose published form had 115 gates at depth 28. The method is from Boyar and Peralta's SEA 2010 paper, so "from 2010" is a fair description of its lineage, although the 113-gate file itself carries no date on the page. The post's 121 for the inverse is the CMT page's reverse-direction circuit, which the page introduces with "We haven't worked much on this." Neither is the smallest published circuit any more.

In September 2026 NIST's circuit-complexity repository added S-box circuits over \{AND, XOR, XNOR\}, among them two 110-gate forward circuits at depth 22 and a 112-gate inverse at depth 26. I cloned [usnistgov/Circuits](https://github.com/usnistgov/Circuits) at its 8 October commit and listed every AES S-box file: nothing in the forward directory is below 110 gates and nothing in the inverse directory is below 112. So the honest comparison for size alone is:

- Forward: 106 against 110, which is 4 gates or 3.6%, at depth 24 against 22.
- Inverse: 109 against 112, which is 3 gates or 2.7%, at depth 30 against 26.

Both are still the smallest circuits for these functions in this gate model that I could find, so "new record" holds in the narrow size sense. But they are not better in both measures than what they beat, and the post's −6.2% and −9.9% are against circuits that the 2026 ones had already passed.

None of this is hidden. Jain's paper says, in its abstract, that the 106 is compared "against 110 gates at depth 22 on the NIST page and 113 gates at depth 27 on the CMT page", that "Both size circuits are deeper than the circuits they beat in size", and that "We claim no improvement on the 110-gate depth-22 circuit in the sense of a tie or a dominated point." Table 1 of the paper carries both baselines on every row:

<Figure src="https://ai.thesatyajit.com/articles/aes-circuits-lean/fig2.png" alt="A results table. Forward S-box Pareto points: 121/16 (34+83+4, AND depth 4) against 125/15 and 125/16; 116/17, 112/18 and 111/21 against 125/15 and 110/22. Smallest size: 106/24 (34+69+3) against 110/22 (minus 4 gates, plus 2 depth, 'smaller, deeper') and 113/27. Inverse: 109/30 (32+71+6) against 112/26 ('smaller, deeper') and 121/21. Dominated: 113/18, 112/20, 106/34, 109/31." caption="Every claimed circuit against the smallest published circuit with depth at most its own, and against the newest neighbour. Note the 'smaller, deeper' verdicts on the 106 and the 109 (Jain, AES S-box paper, Table 1)." />

The paper also releases a set of depth-budget circuits: 121 gates at depth 16, 116 at 17, 112 at 18 and 111 at 21. These fill the gap between NIST's 125-gate depth-15 circuit and the 110-gate depth-22 ones. The 121 at depth 16 is 4 gates below the CMT's 125 at the same depth, but one level deeper than NIST's 125, so it is not a same-depth win either, and the paper says so. Jain's own overlap analysis says the 121/16 shares 104 of its 121 gate functions with the CMT 125/16 and is "most likely a −4-gate local improvement" of it.

Richer gate sets are a separate league. Maximov and Ekdahl (TCHES 2019) reach 102 gates at depth 24 for the forward S-box using NAND, NOR and MUX gates, and Reyhani-Masoleh, Taha and Ashmawy (TCHES 2018) give 119 gates at depth 20 and 129 at depth 16, each plus inverters, in a library with NOR gates (as Maximov and Ekdahl list them). Jain did not translate those into his model, and says the comparison only holds in \{AND, XOR, XNOR\}.

The chart puts every point on one plane. The dashed line is the comparison the post makes; the lowest open square is the comparison that decides whether something is a record.

<GateDepthChart />

## How the S-box circuits were found

The 106 did not come from a SAT solver or from a single clever identity. It came from noticing that a random walk had stopped improving for a structural reason.

Jain's walk moves through functionally equal circuits with two moves: re-express a gate over two other existing signals that are not its descendants, or re-associate $(a \oplus b) \oplus v \to (a \oplus v) \oplus b$ when the inner gate feeds nothing else. Both keep the value of every output and every shared gate. That means a walk can never change the top and bottom matrices, only how they are shared, and walks from the 113 all plateaued at 110 gates (at depth 38, which NIST's 110/22 dominates).

The way out is to change the matrices. The Boyar–Peralta layout fixes one representation of $\mathbb{F}_{2^8}$ over $\mathbb{F}_{2^4}$; a different representation computes the same S-box with different top and bottom matrices around a conjugated inverter. Jain parameterises it by a dual basis and by a scaling and a Frobenius power, for $17 \times 240 \times 60 = 244{,}800$ builds, rebuilds the whole layout in each, scores them with Paar, Boyar–Peralta and RNBP linear-layer heuristics, and then walks the promising ones. Of 288 builds walked, 38 reached 106 and none went lower. The scaling and Frobenius part of that sweep is Maximov and Ekdahl's (their 2040 variants), and the paper credits it; the added parts are the dual basis and rebuilding the layout rather than re-optimising matrices around one fixed inverter. The paper is careful to say it has "no evidence that the dual-basis part is what gains the gates."

That sweep gave 106 gates at depth 34. A separate "depth lane" then rebalanced XOR trees under depth caps, ran the walk with a depth penalty and allowed moves that change a gate's type, which took it to 106 at depth 24 with 34 ANDs. Window SAT, which cuts out 4 to 9 gates and asks a solver for a smaller replacement, found exactly one gate on the 113 and is not credited with the 106.

The inverse 109 is different in kind. It shares only 22 to 23% of its gate functions with either published inverse, against 64% between those two, so it is not a local edit of either; its parent is not recorded. Neither is the search code: the paper says plainly that "the search code is not released, so none of the circuits can be regenerated from the pack." What you can reproduce is the verification, which is what matters for a correctness claim and is the only part I can check. The acknowledgements say the search and drafting were "assisted by AI tools".

## The multiplier, which is the cleanest claim

$\mathbb{F}_{2^8}$ multiplication is not part of the S-box circuits above, but general multiplication in the AES field (MixColumns only ever multiplies by constants) is a building block for composite-field designs and for any constant-time code that multiplies two field elements, and it has a long-standing record: the CMT's 117-gate circuit at depth 6, 48 AND and 69 XOR. The file in the repository's copy of the CMT archive opens with "Multiplication circuit for GF(256) with irreducible polynomial X^8 + X^4 + X^3 + X + 1. Date: July 2010" (`multipliers/sources/circuits/cmt/slp_84310.txt:1-3`). This is the one baseline that really is from 2010, and it is in the same model (AND and XOR only; none of these circuits uses an XNOR).

A field multiplier is bilinear, so every small circuit for it has the form "linear forms of $a$ and of $b$, a layer of $K$ products, a linear map from the products to the 8 output bits". The cost is

$$
\text{gates} = K + L(\alpha) + L(\beta) + L(W),
$$

where $K$ is the number of ANDs and each $L$ is the XOR count of one linear layer. The interesting choice is the product set. Splitting the coefficient index bit by bit, each split can be schoolbook (4 products of the halves) or Karatsuba (3 products, at the price of extra sums on the inputs). The CMT 117 is Karatsuba then two schoolbook levels, $3 \cdot 16 = 48$ products. Jain flips the order and searches over product sets scored by total gates rather than by AND count, solving the output map exactly for each. For a fixed product set that map is forced (the paper reports kernel dimension 0), so the search is really over products.

I split both circuits into layers to see where the five gates went. The CMT 117 spends 8 XORs on the inputs, 48 ANDs and 61 XORs on the output. Jain's 112 spends 20 on the inputs, 36 ANDs and 56 on the output. It pays 12 extra input sums to save 12 products, and then the smaller product set needs 5 fewer output XORs. Karatsuba's trade, made at the right level.

<Figure src="https://ai.thesatyajit.com/articles/aes-circuits-lean/fig4.png" alt="A table of four multiplier circuits for polynomial 0x11B: 112 gates (36 AND, 76 XOR, depth 6, file aes112_d6.slp), 110 (36, 74, depth 7), 108 (34, 74, depth 12), 107 (35, 72, depth 13), each with a SHA-256 prefix and verification level L. Reference: CMT, 117 gates (48 AND, 69 XOR), depth 6." caption="The multiplier's gate–depth points. Only the 112 is at the old record's depth; the 107 is more than twice as deep (Jain, multiplier paper, Table 2)." />

So 117 to 112 at depth 6 is a like-for-like 4.3% (5/117 is 4.27%), and the paper is again explicit that the 107-gate circuit "is more than twice as deep as the 117, so the like-for-like gain is 117 → 112." One caveat the paper raises itself: the same CMT page lists a 106-gate depth-6 multiplier in an unpublished tower basis, which would beat the 112 if you could use it, but in the AES polynomial basis it needs conversion layers whose cost nobody has computed. Jain also notes that newer linear-layer heuristics (Tan–Peyrin, Maximov, Xiang et al.) were not applied to his layers, or to the 117's, so both may shrink further.

## What "Lean-verified" covers

This is the phrase I most wanted to pin down, because "verified in Lean" can mean anything from a full functional specification to a checked table. Here it is closer to the second, and that is fine, as long as you know it. I don't have a Lean toolchain on this machine, so I read the files and the saved outputs instead of re-running them.

For the S-boxes, each file defines the gate list, a literal 256-entry table and a tiny evaluator, and proves that they agree everywhere (`sbox/lean/Sbox106d24.lean:41-48`):

```lean
def allOk (gs : List (Nat × Nat × Nat)) (t : List Nat) : Bool :=
  (List.range 256).all fun x => evalPt gs x == t.getD x 0

theorem circuit_ok : allOk gates sbox = true := by decide +kernel
```

`decide +kernel` makes the Lean kernel evaluate the Boolean itself, so the trusted base is the kernel, not a compiled evaluator; there is no `native_decide` and no `sorry` in any of the 30 Lean files, and the saved `#print axioms` output lists only `propext` for `circuit_ok`. Each file also proves two controls false (one AND flipped to XOR, and a table with entry 0x53 changed), which shows the check can fail.

What this does not prove is that the table is the AES S-box. The table is a literal list of numbers, and the README says so outright (`sbox/README.md:74`): "Lean proves equality with a literal 256-entry table only; gate counts and depth come from tools/verify_sbox.py." So I closed that gap from the other side. I extracted the table from all eleven Lean files and compared each with an S-box and inverse I computed from field inversion and the affine map: all eleven are identical. I also ran each Lean file's own gate list under Lean's own encoding (input bit $i$ is signal $7-i$, output bit $k$ from `outs`), and all eleven compute their table with zero mismatches.

The multiplier proofs are stronger, because the specification is in Lean too. `gmul` is shift-and-add with reduction, written in the file, and the statement compares the circuit with it on every pair (`multipliers/lean/Aes112d6.lean:44-45`), split into 64 chunk theorems of 4 values of $a$ each because, per the README, the unchunked 65,536-point `decide` hit a kernel timeout. The file also proves that the circuit is not multiplication modulo the other common irreducible, 0x11D (`Aes112d6.lean:135`). The theorem of record is the conjunction of the chunks, `circuit_ok : allOkC = true` (line 128); the README states that it is equivalent to the for-all statement "by unfolding the definitions", and that equivalence is not itself a separate theorem.

In both cases gate counts and depths are outside Lean. They come from Python, and from my recount, which agrees.

One small inconsistency, of no consequence to correctness: the multiplier paper says the 112-gate proof took 17m41s, while `Aes112d6.out` records `real 14m47.080s`. The paper's figure may come from another run; I mention it only because everything else in these papers is so carefully reconciled.

## Who gets the gates

If you build AES in hardware or bitsliced software, 106 versus 110 is a few percent fewer gates per S-box, and the 112-gate multiplier is a strict improvement at the old depth. But nothing here has been synthesised. Jain says "we make no area or timing claim", the relative cost of XNOR and XOR depends on the cell library, and the smallest S-box circuits are two to four levels deeper than what they beat, which costs latency unless the design is pipelined. The depth-budget circuits (112 at depth 18, for instance) are the ones to look at if you are latency-bound.

If you mask AES, or evaluate it in MPC or a ZK circuit, the S-box results do nothing for you. Their AND count is 32 to 34, the same as the 113's, and the AND record has moved: a 29-AND forward S-box was published by umizame in July 2026, and NIST now lists 28-AND circuits for both directions, contributed by Milad Nasr in September 2026 (at 124 gates and more). Jain's paper is direct about it: "there is no improvement for masked implementations, where cost grows with ANDs and not with XORs." The multiplier is more interesting here, since it goes from 48 ANDs to 36, but if your MPC protocol already works over $\mathbb{F}_{2^8}$ natively you never multiply bit by bit, so check which of the two you have before reading anything into that.

What I take away is less about AES than about how these results are now produced. A representation sweep of a quarter of a million builds, random walks, SAT windows, an AI-assisted search, and on the other end a verification pack that anyone can run and a theorem prover that refuses to accept a wrong table. The search is closed; the evidence is open and checks out. And the paper is more careful than the post. Read the paper.

## How I checked

I shallow-cloned `Swapnil-jain/gf2m-circuits` at commit `c451bf1` and read both papers (PDFs in `papers/`), the READMEs, the Lean files and their `.out` logs. I did not run any of the repository's code. Instead I wrote my own checker in Python:

- An S-box and inverse built from GF(2^8) inversion modulo 0x11B and the FIPS-197 affine map, asserted against the published values S(0x00)=0x63, S(0x01)=0x7C, S(0x53)=0xED, S(0xFF)=0x16.
- My own parsers for each source format: Jain's JSON and `.txt` listings, the CMT `name = x op y` files (with `#` for XNOR and output aliasing), and NIST's NCFF files. For NIST I tried both bit orders; one matches on all 256 inputs and the other on none.
- Bitsliced simulation of every circuit over all 256 inputs (S-boxes) or all 65,536 pairs (multipliers), counting mismatches; gate counts by type; depth as the longest gate path; AND depth as the most ANDs on any path; and a dead-gate count.

Results: all 11 released S-box circuits (and their `.txt` listings), all 13 released $\mathbb{F}_{2^8}$ multipliers, the CMT 113, 125 and inverse 121, the CMT 117 multiplier and the four NIST files Jain quotes compute the right function with zero mismatches and no dead gates, and every gate count, AND/XOR/XNOR split, depth and AND depth equals the paper's. I extracted the literal tables and gate lists from the eleven S-box Lean files and checked them as described above. I cloned `usnistgov/Circuits` at `113aec8` (8 October 2026) to list every AES S-box file, and read the CMT page text from the copy in Jain's repository. I could not check the search statistics (the 244,800 builds, the walk counts, the provenance of the inverse), which depend on code that is not released.