Breaking Cryptography with LLMs

In July 2026, Anthropic published two results that read, at a glance, like the encryption apocalypse headlines have been warning about: Claude Mythos Preview found a real weakness in a NIST post-quantum candidate and sped up the best public attack on reduced-round AES by up to 800×, both without a human writing the mathematics by hand.

The frame worth holding onto: the hypothesis-generation step of cryptanalysis, the part that used to take a specialist a year of staring at an S-box, now takes an agentic model about a week of search — a billion tokens on the AES run alone. The headline number in that shift is a ratio, not a work-factor drop.

Whichever side you sit on, the practical stakes are the same: finding the next structural weakness — in a candidate scheme, a reduced-round variant, or an unreviewed protocol draft — now costs on the order of a hundred thousand dollars of API spend and a month of expert verification. The benchmark suites built to measure that capability double as an honest check on whether a defensive migration timeline is still realistic, and both sides of that ledger get equal treatment below.

01 The Entropy Barrier

Every wave of cryptanalysis has run into the same wall eventually: a well-designed cipher leaves nothing behind for a machine, or a person, to exploit. Claude Shannon poured that wall's foundation in 1949, when he formalized confusion and diffusion as the properties that make ciphertext statistically indistinguishable from noise; every cipher built since has been judged by how completely it achieves that goal. Each earlier wave hit that wall too, and every one had to route around it rather than through it.

From Friedrich to Claude

Cryptanalysis has always moved in waves defined by whatever computational tool showed up next. Nineteenth-century cryptanalysts like Friedrich Kasiski (this section's namesake) and, later, William Friedman broke polyalphabetic ciphers by hand: counting letter frequencies and coincidences over months of tedious tabulation. Bletchley Park's Bombe machines mechanized that same statistical intuition against Enigma, turning weeks of manual work into hours. The worked example below is a standard textbook illustration of Kasiski's method, not his original 1863 case.

Decades later, Biham and Shamir's differential cryptanalysis and Matsui's linear cryptanalysis turned round-by-round cipher analysis into a precise mathematical discipline, letting a human reason exactly about how many rounds a cipher needed before its structure disappeared into noise.

Each wave of cryptanalysis, hand tabulation, mechanized search, differential and linear analysis, didn't eliminate a human's judgment; it just moved the frontier of what a machine could search versus what a person had to reason through by hand. Agentic LLM cryptanalysis is the next wave in that same lineage, and understanding why it's different starts with the same question every previous wave had to answer first: what, exactly, is left for a machine to find once a cipher is doing its job?

The interesting question about language models and cryptography, the one Maskey, Zhu, and Naseem set out to test directly in "Benchmarking Large Language Models for Cryptanalysis and Side-Channel Vulnerabilities," has been whether a transformer could learn to invert a block cipher: read ciphertext, guess plaintext, the same way it guesses the next word in a sentence. The honest answer has always been no, and reduced-round toy ciphers aside, it still is. That isn't a limitation anyone is racing to fix, either. Confusion and diffusion exist specifically to make direct inversion impossible: with no structure left in the ciphertext to condition on, a model's prediction is just another guess at random noise.

What's new is agentic scaffolding: a model that can't invert ciphertext directly can still drive a Python interpreter, a computer algebra system, or a theorem prover toward an attack a human would otherwise need months to construct by hand, and that combination is increasingly finding things nobody engineered it to find.

The clearest recent instance comes from a research post titled "Discovering cryptographic weaknesses with Claude": given a sandboxed Python and SageMath environment and pointed at open problems in lattice cryptography and block-cipher structure, a frontier model independently found a weakness in a NIST post-quantum signature candidate and materially sped up the best public attack on reduced-round AES.

Nobody's key is more exposed this morning than it was yesterday (the target scheme isn't deployed anywhere, and the AES result tops out at 7 of the cipher's 10 rounds), but the mechanism behind both results is worth taking apart, because it doesn't generalize the way "AI breaks encryption" headlines imply, and it isn't unique to one lab's model, as the benchmark literature further down makes clear.

No Statistical Regularity to Exploit

Start with why the direct approach fails, because it's the reason everything downstream had to be built the way it was. A block cipher's entire design goal, formalized by Claude Shannon as confusion and diffusion, is to make ciphertext computationally indistinguishable from a uniform random string. Flip one bit of an AES-256 plaintext or key and, by design, roughly half the output bits flip along with it. There is no statistical regularity left for a model to key on.

Self-attention has nothing to grab onto in that setting. A transformer's next-token head works by isolating sparse statistical regularities across a sequence: exactly what natural language provides in abundance, and exactly what a properly diffused ciphertext, by Shannon's own design goal, denies it. Maskey et al. ran the direct experiment across nine ciphers, from Caesar shifts to AES, against nine LLMs.

Claude 3.5 Sonnet, the strongest model in their study, decrypts Caesar-shifted text with 0.99 exact-match accuracy; point the identical model at AES-128 ciphertext and exact match drops to 0.00: not approximately zero, exactly zero, and unmoved by giving it nine worked encryption-decryption pairs as few-shot examples first. In-weight inference doesn't approximately fail here; it fails utterly, because there's no statistical regularity left in the target to approximate.

From Models to Agents

Classical ciphers (Vigenère, substitution, Playfair) stay breakable by LLM-guided attacks precisely because they don't satisfy Shannon's criteria. The model isn't doing anything a well-tuned Index of Coincidence calculation couldn't do in principle; it's just better than a frequency table at scoring partial, noisy candidate plaintexts, which lets it work on shorter and messier ciphertexts than classical cryptanalysis ever could.

A second exception makes the same point more sharply. Meta AI's SALSA (Wenger et al.) trained a transformer to learn Learning With Errors (LWE) encryption directly, turning the model's weights into a practical key-recovery attack on lattice-based cryptography: fully recovering sparse binary secrets up to dimension 128, with a follow-on line (SALSA VERDE, SALSA FRESCA) that has since widened the margin to dimension 1,024 for the same sparse-secret setting. It's real, and it's the strongest evidence anywhere that a model can attack a real primitive family from its weights alone. But like the classical ciphers above, it doesn't cross the entropy barrier; it confirms the barrier by specificity.

Those targets are engineered to be mostly-zero and low-error, a strong prior a transformer can latch onto, and they are homomorphic-encryption-style parameters, not the random-secret schemes NIST actually standardized, which still sit out of reach. The reason SALSA works and AES does not is the reason the barrier holds in the first place: the lattice setting carried exploitable structure that confusion and diffusion exist precisely to erase.

So if raw autoregressive inference is a dead end against anything designed since the 1970s, where did Claude Mythos's two results, the post-quantum weakness and the AES speedup described above, come from?

The results didn't come from the model's weights doing cryptanalysis; they came from the model driving tools that can. Each run followed the same loop: form a hypothesis about a structural weakness, emit it as code in the target's own formal language, let a solver return a verdict — an attack, a proof, or a counterexample — and feed that verdict back into the next hypothesis.

Concretely, "emits code" can be as plain as unrolling a round-reduced cipher's state transition into a bit-vector SMT problem and handing the search to Z3 instead of guessing keys directly. In the sketch below, the key bits become free boolean variables (K), the state at each round gets its own array (S, S_next), and the round loop XORs in the same nonlinear term and round key the cipher itself would apply.

The two boundary conditions, the plaintext constraint before the loop and the ciphertext constraint after it, are what pin those free variables down to one specific key. solver.check() then either returns sat with a concrete model to read the key bits out of, or comes back UNSAT, which here means the attack's round or bit bounds were too tight, not that no key exists. This is an illustrative sketch of the pattern, not a specific published exploit:

from z3 import *

def solve_round_reduced_cipher(known_plaintext, target_ciphertext, rounds=4):
    # the controller emits this; Z3 does the actual search
    solver = Solver()
    K = [Bool(f'k_{i}') for i in range(32)]
    S = [Bool(f's0_{i}') for i in range(32)]

    for i in range(32):
        solver.add(S[i] == (BoolVal(known_plaintext[i]) ^ K[i]))

    for r in range(1, rounds + 1):
        S_next = [Bool(f's{r}_{i}') for i in range(32)]
        for i in range(32):
            nonlinear = And(S[(i + 1) % 32], S[(i + 2) % 32])
            solver.add(S_next[i] == (S[i] ^ nonlinear ^ K[(i + r) % 32]))
        S = S_next

    for i in range(32):
        solver.add(S[i] == BoolVal(target_ciphertext[i]))

    if solver.check() == sat:
        model = solver.model()
        return [1 if is_true(model[K[i]]) else 0 for i in range(32)]
    return None  # UNSAT: attack bounds insufficient

02 Two Worked Examples

These results come from a small internal team at Anthropic running Claude Mythos Preview inside a multi-agent harness with Python and SageMath. Both were reviewed by outside cryptographers before publication, and both come with the same caveat stapled to the front: neither one touches a system you rely on today.

The HAWK Key Recovery

HAWK is a lattice-based signature scheme still under evaluation in NIST's post-quantum standardization process: one candidate among several, not deployed. Its security rests on the difficulty of recovering a short secret basis from a published Gram matrix, over a lattice built from power-of-two cyclotomic rings.

The vulnerable symmetry itself wasn't news: van Gent and Pulles had already shown, in independent academic work, that a nontrivial automorphism of HAWK's key lattice would weaken it. Mythos's contribution, formalized in Straznickas and Weis's follow-up technical report, was finding that automorphism explicitly (the Galois involution τ: ζ ↦ −ζ) and using it to build a public "cocycle lattice" whose shortest vector reveals a functional equivalent of the secret key, via a Shortest Vector Problem instance in roughly half the original dimension.

Half the dimension sounds abstract until you see the resulting work-factor drop: HAWK-512 falls from 2¹⁵⁰ to 2¹⁰⁸, HAWK-1024 from 2²⁸⁸ to 2¹⁸², and the small HAWK-256 parameter set (where the attack is practical) from 2⁶⁴ down to 2³⁸, low enough to run end-to-end on a single machine in a few hours.

This is exactly the kind of result NIST's evaluation process exists to surface before standardization, not after.

Anthropic's own write-up doesn't say, though, whether HAWK's designers accept the analysis, or who the unnamed outside cryptographers who reviewed it were. One independent check did happen in public: cryptographer Daniel Apon verified the mathematical reduction on NIST's pqc-forum within an hour of the post going up, replying "it checks out independently for me." That's the reduction, not a reproduction of the full end-to-end key recovery, and it happened after publication, not as part of Anthropic's own pre-publication review.

What Anthropic did make public for HAWK is a runnable demo repository, not just a paper. That's unusually concrete for a disclosure like this. The AES side doesn't get the same treatment: no exploit code, just the technical report and Claude's reasoning trace.

The AES Möbius Bridge

The second result targets 7-round AES-128 in the single-key setting, where the standing best attack is Derbez et al.'s 2013 meet-in-the-middle construction, which needs nine subkey-byte guesses to build its offline matching tables: u₁[0..3], u₅[0], and u₆[0..3].

Mythos found what Nasr and Carlini's companion technical report calls the Möbius Bridge: the AES S-box is an inversion over GF(2⁸) followed by a fixed affine transform, S(x) = A(x⁻¹) + b, and there is an affine-invariant fingerprint of the round-5 transition difference that stays fixed regardless of one specific subkey byte, u₅[0]. Project the matching condition into that invariant coordinate frame and the dependency on that byte disappears: one fewer guess, a 256× reduction in the search space for that half of the attack.

Removing a byte guess doesn't help if computing the invariant costs more than the guess it replaces, so the harder engineering problem was building a fingerprint kernel cheap enough to keep the net win. The result: attack time complexity for 7-round AES-128 drops from 2⁹⁹ to somewhere between 2^89.3 and 2^91.4 operations (a 200–800× speedup in the computation needed to run the key-recovery attack, not in how fast anyone found it) at the same 2¹⁰⁵ chosen-plaintext data complexity as before.

The same post credits the model with two further reduced-round breaks, and one useful failure. A practical 13-round LEA key recovery using under 2³⁰ plaintexts, finished in under an hour; a full key recovery on 6-round Serpent-128, extending past the previous best bound of 2⁷⁰; and, on the other side of the ledger, attempts against Salsa20, Poseidon, and SHA-1 that yielded less than a 10× improvement over existing attacks: exactly the kind of negative result a hype-driven summary tends to leave out.

A Week to Find, a Month to Check

The numbers above are the least interesting part of the story. What matters is the process.

For HAWK:

• One researcher without a lattice-cryptography background ran the model inside the multi-agent harness for roughly 60 hours, mostly doing project management rather than mathematics.
• Two agent instances working the same problem disagreed with each other along the way (one dismissed the automorphism angle as infeasible before the other found a way to exploit it), and the disagreement itself proved productive.
• Total cost: on the order of $100,000 in API spend.

The AES result is stranger. Early on, the model concluded the improvement the researchers were asking for was impossible, and said so directly:

"If you want a different outcome, the target has to change."

For AES:

• Getting past that took three minimal prompts: reassurance that the model was allowed to struggle with a hard problem, redirection back to the original target instead of a substitute, and encouragement to keep looking.
• From there, it worked largely unsupervised for three days, producing several hundred million tokens before converging on the Möbius Bridge construction.
• It then spent a few more days refining that result, reaching roughly a billion tokens in total. Call it a week, start to finish.
• Cost, again, was on the order of $100,000.

Simon Willison called the shared prompts, spelling mistakes included, "the best part of this article," and quoted them straight rather than summarizing them. One researcher's prompt, unedited: "the models tend to think it is impossible to solve so they don't try they need a good amount of prompting." A later one in the same thread is blunter: "no we don't want to change the targets [...] agian we need to find something that worth publishing."

Then came the part that took longer than the discovery. The researchers' own account of the work makes the comparison directly:

"Compared to the one week that Mythos spent conceiving the idea, the vast majority of human researchers' time was spent validating the correctness of its claims."

03 From Anecdote to Pattern

Two results from one lab would be an anecdote. What makes it a trend is that dedicated benchmarks built specifically to measure this capability now exist.

The LWE Line, First

None of that benchmark-suite pattern is new either. Meta's 2022 SALSA attack on lattice LWE came paired with its own LWE Benchmarking effort (Wenger et al., IEEE S&P 2025): a dedicated comparison that measured the whole SALSA family against the classical state of the art (BKZ lattice reduction, uSVP) instance by instance, rather than against an LLM's word or an inflated headline. The attack never reached NIST-standardized random-secret parameters, and the benchmark said so plainly. CryptanalysisBench, four years on, explicitly lists the SALSA papers as related work: the lineage running from a direct neural attack, to the first benchmark built to measure it, to today's frontier-model suite is about as direct as it gets.

CryptanalysisBench

CryptanalysisBench (Fluri et al.) runs 191 tasks across six primitive families drawn from four NIST standardization efforts, split into known practical breaks, scaled-down variants, and full-strength production primitives. Frontier reasoning models solve 65–86% of the known-break tier (table stakes, arguably), but the benchmark also produced two results nobody engineered it to find: a key-recovery attack on the full SpoC AEAD scheme, and a gap in KINDI's published CCA-security proof that had survived peer review.

Bruce Schneier's own read on the benchmark keeps the caveats intact. The paper's own abstract is blunt about where things stand, and he quotes it directly: "we ask whether LLMs can do cryptanalysis, and find that the answer is increasingly yes," calling its early attacks "an early snapshot of a fast-moving frontier that may soon match, and in places exceed, the published state of the art." Schneier's own verdict is more measured: "Anthropic's frontier model actually found new attacks... Still early results, but this is definitely something to watch."

AICrypto's Three Tiers

AICrypto (Wang et al.) casts a wider net: 135 concept questions, 150 capture-the-flag exploitation challenges, 18 proof problems, across 17 models. On the concept questions, o3 misses only 3 of 135 for 97.8% accuracy, edging out the best human expert's 94.1%: memorization is saturated, full stop.

Formal proof-writing sits in between: the best models, gemini-2.5-pro and o3-high, score 84.5% and 84.2% against a human expert average of 88.1%. Close, but not saturated, and not yet matched.

The capture-the-flag results tell a third story. Human experts solve 81.2% of the practical exploitation challenges; the same top models solve 55.3% and 54.0%. That's the entropy-barrier prediction showing up again, quantified: models are excellent at recognizing a vulnerability class and bad at the multi-step dynamic analysis needed to exploit it.

Why Scaffolding Wins

CryptanalysisBench and AICrypto were built independently, by different teams, and they degrade in the same place: solid on the known-break and memorization tiers, then falling off exactly where a task stops being well-posed math and starts requiring multi-step, dynamic reasoning. That convergence, not any single number, is what makes this a pattern rather than an anecdote.

That gap raises an obvious question: if a standalone model solves barely half of AICrypto's CTF challenges, how did the same model family produce two cryptographic discoveries? The answer is scaffolding. AICrypto measures a model working alone, one shot, against a fixed budget. HAWK and the Möbius Bridge instead came from Claude Mythos wired into a multi-agent harness, given 60 hours and about a week respectively, with a human nudging it past its own premature conclusion that success was impossible. The benchmark measures the model; the breakthroughs measured the whole system built around it.

Each bar falls apart for a different reason. CryptanalysisBench drops off on novel algebraic structure and full-strength production primitives; AICrypto's proof tier falls apart on nothing catastrophic, just not quite matching human accuracy yet; its exploitation tier falls apart on multi-step dynamic analysis; and Maskey et al.'s decryption benchmark falls apart on any cipher that meets Shannon's criteria. Only the concepts tier has nothing left to fall apart on: it's saturated.

Verifying Protocols with Tamarin

Primitives are the cleanest target because they reduce to well-posed math problems. Protocols and hardware are messier, and the literature there tells a more mixed story.

CryptoFormalEval (Curaba et al.) pairs an LLM agent with the Tamarin Prover: the agent proposes an attack trace against a novel protocol, Tamarin either verifies it or hands back a counterexample, and the agent iterates.

Modesti et al. ran a more sobering comparison: unassisted chat models and reasoning models against ProVerif and OFMC, across 130 obfuscated protocols and 388 security goals. Chat models over-flag: 69–81% recall at under 31% precision, which in practice means drowning a human reviewer in false positives. Reasoning models invert the trade-off, up to 66.5% precision, but they catch barely half the true attacks, and they're specifically weak on injective authentication and multi-session replay: exactly the class of bug that depends on tracking state across an entire execution rather than reasoning locally about one message.

Extremal Testing from RFCs

CornerCase (Singha et al.) sidesteps the reasoning problem by scoping the LLM to something it's good at: reading an RFC and extracting explicit validity constraints, section by section, then generating test inputs at the boundary of each one. Across HTTP, DNS, BGP, QUIC, and SMTP implementations it surfaced 42 anomalies, 26 acknowledged as real bugs and 18 already fixed.

The individual cases are more illustrative than the count. A percent-encoded null byte in an h2o request path triggered a 301 redirect back to a path h2o considered semantically identical to the original, an infinite loop with real denial-of-service potential, patched after disclosure.

GoBGP accepted routes whose AS_PATH looped back through the router's own confederation identifier, precisely the isolation boundary confederations exist to enforce, and separately accepted EBGP sessions from non-member peers claiming that same confederation ID. On the DNS side, a single KEY record (RR type 25) was enough to fail an entire zone load in two independent nameserver implementations, Yadifa and Technitium: one malformed record, and every other record in the zone goes down with it.

Side-Channel Analysis, End to End

And Wałigóra (2025) showed GPT-4, driving Python against real oscilloscope traces off an embedded AES implementation, can run an entire Correlation Power Analysis campaign end-to-end and recover a 128-bit key without a human writing the analysis code.

The core of that campaign is a small, standard CPA loop: hypothesize a Hamming-weight leakage model per key byte, correlate it against the real power trace, keep whichever byte guess produces the sharpest correlation peak. It's a well-known technique; what's new is that the agent writes and runs it unattended:

import numpy as np

def correlation_power_analysis(traces, plaintexts, sbox):
    # hypothesize Hamming weight per key-byte guess, correlate, keep the peak
    hw = np.array([bin(n).count('1') for n in range(256)])
    recovered_key = []

    for byte_idx in range(16):
        best_guess, best_corr = 0, 0.0
        for k in range(256):
            hyp = hw[sbox[plaintexts[:, byte_idx] ^ k]]
            corr = np.corrcoef(hyp, traces.T)[0, 1:]
            peak = np.max(np.abs(corr))
            if peak > best_corr:
                best_guess, best_corr = k, peak
        recovered_key.append(best_guess)

    return recovered_key

04 LLMs+X: Comparing Boosts Side-by-Side

The same shape holds whichever deterministic backend sits behind the model:

• Pair it with an SMT solver and it learns to propose reductions that shrink the search space before the solver ever runs: a Galois automorphism, an affine-invariant fingerprint.
• Pair it with a symbolic protocol checker like Tamarin and it learns to propose attack traces that the checker either confirms or falsifies with a concrete counterexample.
• Pair it with a classical symbolic execution engine and the shape holds again: SAILOR wires an LLM's vulnerability hypotheses into exactly that backend and confirms 379 memory-safety bugs across ten C/C++ projects, against 12 for the strongest LLM-only baseline tested.
• Pair it with a fuzzer instead, as CODE-AUGUR does, and it learns to propose runtime invariants that the fuzzer either violates (a real bug) or fails to violate (a wrong assumption sent back for refinement).

In every case the model's job stops at picking a hypothesis in the target's native formal language; the tool's job is to return a verdict, not a suggestion.

The choice of backend tracks the target, not the model.

A cipher or a protocol goal is a closed, well-specified mathematical object; a real codebase is an open-ended surface with no fixed boundary, five million lines of pointer arithmetic and external libraries deep. That difference, not anything about which model is doing the proposing, is what decides whether Z3 and Tamarin do the work or a fuzzer does.

SMT and theorem provers reward a problem that's already clean and bounded, like a round-reduced cipher or a well-scoped protocol goal, while fuzzing earns its keep on the muddy exterior of a real production codebase, where full formalization would drown in pointer arithmetic and external libraries long before it found the bug.

Line the actual boost numbers up across both regimes and that same clean-versus-muddy split is exactly what explains the gap between them.

The cryptanalysis multipliers run into the millions; the fuzzing multipliers top out around 5×. That's not a smaller result, it's a different unit.

A cipher's complexity is a known number you can shrink toward zero; a codebase's true bug count isn't known at all, so "boost" there can only mean searching an unbounded space better, never collapsing a bounded one.

05 The Verification Bottleneck

By the paper's own count, it took two researchers nearly a month (several hundred hours) to gain that confidence, against the one week Mythos took to reach a refined result. That's the number that should have been the headline, and it runs backwards from most of cryptanalysis's history, where having the idea was the hard part and checking a claimed break, once written down, was comparatively quick.

The Asymmetry, Confirmed Independently

This is the same asymmetry this blog keeps running into from different directions: an agent that can generate a plausible answer faster than a human can independently confirm it is not obviously progress until someone builds the verification layer to match.

Independent commentary on the release landed on almost the same number without coordinating with Anthropic at all: as PostQuantum.com put it, "what changed is the economics of finding these flaws. A publishable cryptanalytic result now costs about USD 100,000 and a week of model time." That's the discovery half of the ratio, independently confirmed; the verification half is the part nobody outside Anthropic has had to reckon with yet.

Does It Take a Frontier Model?

There's a further question this post hasn't asked: did any of this need a frontier model specifically? A recent post on this blog, about small language models in cybersecurity, found that Claude Mythos's other headline results (a 27-year-old OpenBSD bug, a 17-year-old FreeBSD root exploit) were mostly reproduced within days by open-weight models three orders of magnitude smaller, at two to three orders of magnitude lower cost per token.

AISLE's own conclusion from that replication, in co-founder Stanislav Fort's own words: "the moat in AI cybersecurity is the system, not the model." Nobody has run the same experiment against HAWK or the Möbius Bridge yet, but nothing in this post's numbers rules it out.

The Lean Backstop

That's exactly why the credible results above route through a symbolic backstop rather than trusting the model's say-so: Tamarin for protocols, SMT and lattice-reduction tooling for round-reduced primitives, out-of-band test vectors for recovered keys. The neural half proposes; the symbolic half disposes. Nothing in this post's numbers came from an LLM's assertion that it was right. They came from someone else checking.

Every backstop named above still bottoms out in a human reading a solver's output and deciding it's trustworthy. A Tamarin trace or a Z3 UNSAT core is inspectable, but nobody outside the original toolchain re-derives it from first principles. That's exactly the gap that turned a week of search into a month of checking. A proof checked by Lean is a different kind of artifact: the kernel that verifies it is a few hundred lines long, and a third party can re-run the whole thing in minutes instead of re-deriving it by hand.

Cryptography professor Matthew Green, reading these exact results, lands on the same fix this post has been circling from the diagnosis side: with human review now the bottleneck rather than discovery, he argues the field needs machine-checkable proofs, not just a solver's word that it looked correct.

That's already underway, in pieces. Dziembowski et al.'s Lean 4 framework formally translates symbolic security proofs (the same Dolev–Yao-style reasoning Tamarin does) into computationally-sound ones, closing the gap between "the symbolic checker said yes" and "a cryptographer would sign off on the underlying reduction." Zhang et al. go a step further and put an agent in that loop directly: it drives Lean to formalize Shor's algorithm and produce machine-checked resource estimates for breaking RSA-2048 and P-256, with a human reviewing the scientific claims instead of re-deriving the proof by hand.

Not Unique to Cryptanalysis

Neither paper points at HAWK or the Möbius Bridge specifically, and neither closes the verification bottleneck on its own, but it's the same neurosymbolic loop this whole post describes, aimed one layer downstream: an agent proposing a proof, and Lean's kernel disposing of it in a way anyone can re-check, not just the lab that ran the original search.

It's the same loop under a different backend everywhere else in this post, too (SAILOR proposing to Z3, CryptoFormalEval proposing to Tamarin, CODE-AUGUR proposing to a fuzzer), and it shows up well outside cryptography and security altogether. DeepMind's AlphaProof pairs a language model with Lean itself and AlphaZero-style search over proof steps; paired with AlphaGeometry 2, it reached silver-medal standard at the 2024 International Mathematical Olympiad, solving 3 of the 6 problems, including the competition's hardest.

De Smet and De Raedt's recent attempt to give the field a single formal definition (neurosymbolic inference as an integral over a product of a logical and a belief function) is itself a sign the pattern has outgrown any one instance of it, cryptanalysis included.

Playing Defense

Every capability above runs in the other direction just as well, and in most organizations, more usefully. The asymmetry that matters is who runs the same scan first, not which side has better tooling. SAILOR's 379 memory-safety bugs, CODE-AUGUR's 34–370% bug-finding lift, VulnSage's +34.6% on exploit generation: every one of those is a defensive audit pass, measured on the offensive side of the ledger and turned into defense simply by pointing the same harness at your own codebase before anyone else does.

The classic worked example is timing side channels, where the vulnerability and the fix are both one line:

// vulnerable: early return leaks the mismatching byte offset via timing
int crypto_verify_vulnerable(const uint8_t *a, const uint8_t *b, size_t len) {
    for (size_t i = 0; i < len; i++) {
        if (a[i] != b[i]) return -1;
    }
    return 0;
}

// constant-time: bitwise OR accumulates every byte before branching once
int crypto_verify_secure(const uint8_t *a, const uint8_t *b, size_t len) {
    uint8_t result = 0;
    for (size_t i = 0; i < len; i++) {
        result |= (a[i] ^ b[i]);
    }
    return (int)result;
}

An agent wired into CI catches exactly this pattern (non-constant-time comparisons, static IVs, weak PRNG seeding) by scanning compiled assembly or LLVM IR on every merge, not as a red-team exercise run once a quarter. The same cheap-then-strong pipeline that gives Revelio its 3.2–5.6× bug-finding edge is what makes the defensive scan cheaper than the breach it prevents; the only real variable is whose repo the harness is pointed at.

Defense isn't only about catching bugs in CI, though; it's structural.

What changed is the cost of finding the next structural weakness before the other side does, now on the order of a hundred thousand dollars of API spend against a month of expert verification. The defender runs the same neurosymbolic loop as the attacker; the deficit is only in how often they run it first.

06 Open Questions

Everything above describes what happened recently. What happens next turns on a handful of questions this post can't settle, and each one changes how much the numbers above end up mattering.

RQ-1: Does it take a frontier model at all? The small-model replications discussed under the verification bottleneck stopped short of cryptanalysis: nobody has yet swapped an open-weight model three orders of magnitude smaller into the HAWK or Möbius Bridge harness. The per-token gap alone is stark: gpt-oss-20b runs at $0.11 per million tokens against Mythos's reported $25–125 for the same unit, and a comparable open-weight scaffold sweep in that same post turned up several dozen additional findings for under $20,000 total. If that swap works, neither result required a frontier lab's weights: just the right agentic scaffolding pointed at Z3 and SageMath, a far cheaper thing for anyone to replicate.

RQ-2: Was the model doing mathematics, or fast search? The vulnerable HAWK symmetry wasn't news: van Gent and Pulles had already shown an automorphism would weaken the scheme; Mythos found the specific one. So the open question underneath the whole neural-proposes, symbolic-disposes story is how much of the win is genuine mathematical insight and how much is efficient enumeration over a space a scripted search could also have swept. The answer changes what "an LLM found it" is worth.

RQ-3: Is any of this reproducible, or path-dependent on one researcher's nudges? The AES result turned on a human pushing the model past its own premature "impossible," and two agent instances on the same problem disagreed with each other along the way. Whether that's repeatable science or a lucky prompt is not something a single write-up can answer. It takes independent teams re-running the harness and reporting when it doesn't work, too.

RQ-4: Can the same agentic loop that compressed discovery also compress verification? The month of expert checking, not the week of search, is the actual bottleneck. The Lean backstop discussed above is a first answer, not a settled one. Nobody has pointed an agent-plus-Lean pipeline at a result like HAWK or the Möbius Bridge yet, so it's still open whether that compresses a month of expert checking the way agentic search compressed discovery, or whether confirming a claimed break needs a kind of judgment that resists automation precisely because a wrong "verified" stamp does more damage than an unverified claim.

RQ-5: Does this reach production ciphers, even in the limit? Every result here tops out at reduced rounds or an undeployed candidate, and the clean, bounded search space that SMT and lattice tooling depend on blows up fast as round count and key size grow toward their deployed values. Nothing in this post suggests confusion and diffusion stop working for full AES, RSA, or TLS as the harness improves (the entropy barrier is a property of the cipher, not of how hard anyone is trying), but whether reduced-round progress is a temporary frontier or a structural ceiling is precisely what the next few cycles of results will show.

RQ-6: How long does the grace period last? AICrypto's 25–30 percentage-point gap between human and model performance on practical exploitation is the one number in this post with no established lower bound. Nothing here supports a specific timeline for closing it, only that the theoretical-reasoning half of the gap closed first, and defenders are currently spending whatever time the practical half buys.

RQ-7: What do disclosure norms look like at $100,000 a break? This disclosure held together because a well-resourced lab chose to run it that way: Anthropic warned the HAWK authors first, and shipped a demo repo for HAWK while withholding exploit code for AES. None of that holds once the finder isn't a norms-following lab. When a publishable break costs six figures, the open question is who is obligated to tell whom, and what stops the first mover from simply publishing or selling.

07 Conclusions

Set the open questions aside for a moment and look at what this post established. The entropy barrier held. Nothing in this post inverts a properly diffused cipher from ciphertext alone, and nothing here is a reason to lose sleep over AES-128 or your TLS session today. Confusion and diffusion are doing exactly what Shannon designed them to do; no transformer read a ciphertext and guessed its way to a key.

The entropy-cliff data earlier in this post makes the point precisely: Claude 3.5 Sonnet's exact-match accuracy on AES-128 sat at 0.00, not approximately zero, even with nine worked examples to learn from. SALSA is the apparent exception, and it proves the rule rather than breaking it: it works because its lattice targets carry the mostly-zero, low-error structure that confusion and diffusion exist specifically to erase, not because a model learned to invert a properly diffused cipher.

What moved sits one layer up, at the same layer every previous wave of cryptanalysis moved, only this time the frontier shifted to hypothesis generation itself: the part that used to require a specialist staring at an S-box for a year now takes a model about a week of search — roughly a billion tokens on the AES run alone.

That's what makes the headline number the discovery-to-verification ratio, not the work-factor drop. About a week of largely unsupervised search against a month of two researchers checking the answer is a new shape for a field where, historically, having the idea was the hard part and confirming it was comparatively quick. Every credible result in this post routes through a symbolic backstop (Tamarin, an SMT solver, an out-of-band test vector) precisely because that ratio has flipped, and none of the underlying literature treats it as a solved problem yet.

Closing the verification gap is where the neurosymbolic loop points next: an agent proposing a proof for Lean's kernel to check in a way any third party can re-run, not just an attack for a solver to check once. Nobody has pointed it at a result of HAWK's or the Möbius Bridge's caliber yet. But it's the same shape of fix Matthew Green reached for independently after reading these exact results: verification has to become machine-checkable too, not just discovery.

The dual-use math cuts the same way for defenders. The same loop that found the Möbius Bridge finds non-constant-time comparisons in your own codebase; the same benchmark suites that measure offensive capability are the honest way to measure whether a PQC migration timeline is still realistic. The deficit, as the defense argument above laid out, is only in who runs the scan first.

Push this post's central ratio to its logical endpoint and the real question stops being which scheme falls next. It becomes whether anyone can tell a genuine result from a plausible-looking one fast enough to matter.

That instability is why verification, not discovery, is the harder problem from here. Green's own framing of who that leaves exposed doesn't carve out an exception for specialists: "we're all in that same pond, scientists, lawyers, salespeople, even plumbers. Whatever happens next, it's probably going to happen to us all."

References

• Anthropic. (2026). Discovering cryptographic weaknesses with Claude. link
• Straznickas, Z., & Weis, S. A. (2026). HAWK-n Key Recovery Reduces to SVP in Dimension n/2 + 1. Anthropic Technical Report. paper · demo code
• Nasr, M., & Carlini, N. (2026). Cryptanalysis of 7-Round AES via the Algebraic Structure of its S-box. Anthropic Technical Report. link
• van Gent, D. M. H., & Pulles, L. N. (2025). HAWK: Having Automorphisms Weakens Key. IACR Communications in Cryptology, 2(2). link
• Derbez, P., Fouque, P.-A., & Jean, J. (2013). Improved key recovery attacks on reduced-round AES in the single-key setting. EUROCRYPT 2013, 641–660. link
• The Hacker News. (2026). Claude AI Just Cracked a Post-Quantum Encryption Candidate — Here's What It Means. link
• Implicator.ai. (2026). Anthropic Posts AI-Found HAWK Attack to NIST Forum, Cryptographer Confirms the Math. link

• Fluri, L., Shafran, A., Carlini, N., Jagielski, M., Nasr, M., Dunkelman, O., Ronen, E., & Tramèr, F. (2026). CryptanalysisBench: Can LLMs do Cryptanalysis? arXiv preprint arXiv:2607.18538. paper · code
• Wang, Y., et al. (2025). AICrypto: A Comprehensive Benchmark for Evaluating Cryptography Capabilities of Large Language Models. arXiv preprint arXiv:2507.09580. paper · code
• Maskey, U., Zhu, C., & Naseem, U. (2025). Benchmarking Large Language Models for Cryptanalysis and Side-Channel Vulnerabilities. Findings of the Association for Computational Linguistics: EMNLP 2025. arXiv preprint arXiv:2505.24621. link
• Wenger, E., Chen, M., Charton, F., & Lauter, K. (2022). SALSA: Attacking Lattice Cryptography with Transformers. NeurIPS 2022. arXiv preprint arXiv:2207.04785. paper · Meta blog
• Wenger, E., Saxena, E., Malhou, M., Thieu, E., & Lauter, K. (2025). Benchmarking Attacks on Learning with Errors. IEEE S&P 2025. link

• Curaba, C., D'Ambrosi, D., Minisini, A., & Pérez-Campanero Antolín, N. (2024). CryptoFormalEval: Integrating Large Language Models and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection. arXiv preprint arXiv:2411.13627. paper · code
• Modesti, P., et al. (2026). Evaluating Large Language Models for Symbolic Security Protocol Analysis. arXiv preprint arXiv:2607.20712. link
• Singha, R., et al. (2026). CornerCase: Automated Extremal Testing of Protocol Implementations using LLMs. arXiv preprint arXiv:2606.29124. link
• Wałigóra, W. (2025). Large Language Models in side-channel cryptanalysis. International Journal of Electronics and Telecommunications, 71(2), 437–442. link

• Shafiuzzaman, M., Desai, A., Guo, W., & Bultan, T. (2026). Guiding Symbolic Execution with Static Analysis and LLMs for Vulnerability Discovery (SAILOR). arXiv preprint arXiv:2604.06506. paper
• Zhang, H., Rong, Y., He, Y., & Chen, H. (2024). LLAMAFUZZ: Large Language Model Enhanced Greybox Fuzzing. arXiv preprint arXiv:2406.07714. paper
• Chen, S., Luo, T., Wu, S., Liu, X., Zhou, Y., Li, Q., & Xu, W. (2026). Vulnsage: A Multi-Agent Framework for Automated Exploit Generation with Constraint-Guided Comprehension and Reflection. arXiv preprint arXiv:2604.05130. paper
• Hou, Y., Wang, H., Lyu, M., Momeu, M., Nguyen, E., Yang, T., Sen, K., Song, D., & Wagner, D. (2026). Revelio: Cost-Efficient Agentic Memory Safety Vulnerability Detection for Repository-Scale Codebases. arXiv preprint arXiv:2606.22263. paper

• Schneier, B. (2026). Measuring LLMs' Ability to Perform Cryptanalysis. Schneier on Security. link
• PostQuantum.com. (2026). AI Broke a NIST Candidate. Not Your Encryption. link
• Willison, S. (2026). Discovering cryptographic weaknesses with Claude. Simon Willison's Weblog. link
• CyberScoop. (2026). Anthropic's Claude Mythos finds weaknesses in encryption algorithms. link
• Fort, S. (2026). AI Cybersecurity After Mythos: The Jagged Frontier. AISLE, April 7, 2026. link
• Green, M. (2026). Some notes about Anthropic's new results. A Few Thoughts on Cryptographic Engineering. link

• Dziembowski, S., Fabiański, G., Micciancio, D., & Stefański, R. (2025). Computationally-Sound Symbolic Cryptography in Lean. IACR ePrint 2025/1700. link
• Zhang, L., Zhao, Y., Yao, H., & Wang, X. (2026). Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256. arXiv preprint arXiv:2607.14082. link
• De Smet, L., & De Raedt, L. (2025). Defining Neurosymbolic AI. arXiv preprint arXiv:2507.11127. link
• DeepMind. (2024). AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems. link

• Z3 SMT Solver — theorem prover used for bit-vector constraint solving. link
• SageMath — open-source computer algebra system used for lattice reduction and Galois field arithmetic. link
• Tamarin Prover — symbolic model checker for security protocols under the Dolev-Yao model. link