#formalmethods — Public Fediverse posts on home.social

Lobsters @[email protected] · 2026-08-15 · 11:20 UTC

Improving system safety with Temporal Logic of Actions (TLA+) https://lobste.rs/s/ues1ak #formalmethods #vibecoding
https://depot.dev/blog/tla-verification

#formalmethods #vibecoding

Lobsters @[email protected] · 2026-08-15 · 11:20 UTC

Improving system safety with Temporal Logic of Actions (TLA+) https://lobste.rs/s/ues1ak #formalmethods #vibecoding
https://depot.dev/blog/tla-verification

#formalmethods #vibecoding

Marin Ivezic @[email protected] · 2026-08-15 · 08:03 UTC

Cryptanalysts are using AI models now, openly and on live claims. So what does "independently confirmed" mean? Less than it meant two years ago, and two events this summer show why.

April 2024 is the baseline. Yilei Chen posted a claimed polynomial-time quantum algorithm for LWE on the first day of the NIST PQC Standardization Conference. Eight days later he withdrew it, with an acknowledgment thanking Hongxun Wu and, independently, Thomas Vidick for finding the bug in Step 9. That parenthetical is the whole quality control mechanism of the field. Two experts, reasoning separately, converged on the same defect. Neither had seen the other's reading.

July 23, 2026. Ananth and Sahai at UCSB and UCLA posted a proof of efficient unclonable encryption at 10:35 Pacific. Seyoon Ragavan at MIT posted the same result three hours and eighteen minutes later. Both credited GPT-5.6 Sol Ultra with the core ideas. Both traced to the same Simons Institute talk. Neither knew the other was working on it. Ragavan drove the model in supervised two-hour stretches; Ananth and Sahai used a self-critiquing UCLA harness. Two workflows about as different as two workflows get, one construction, one working day.

August 2026. Daniel Simon's claimed polynomial-time algorithm for the Dihedral Coset Problem is being adjudicated right now on ePrint and Discord, in days rather than months, with Bernstein and Kirshanova among the people reading it. Several of the substantive responses were produced by humans working with models. One lists two language models on its byline. Disclosure across the documents is uneven: some name the model and version, some say only "AI assistance."

The mechanism cryptanalysis depends on is not expertise. It is decorrelated failure. Two humans with similar training still make different mistakes, at different points, for different reasons, and their errors decorrelate even when their education does not. The risk with shared tooling is not sampling correlation. It is common-cause error, where shared weights, training data, post-training and retrieval reproduce the same blind spot across operators who have no way of noticing they share it.

I am not claiming three model-assisted reviews reduce to one. I am claiming we currently lack the provenance to know how much independent weight they deserve.

The fix is cheap. Every cryptanalysis note that circulates before peer review should end with two sections: who found what, and what was checked by whom, with what, and how hard. Ragavan's paper already does most of it, and ships a Lean 4 formalization that states which claims it does not cover. A kernel shares no weights with anything.

IACR has barred models from bylines since May 2025. That rule governs formal submission. It does not reach the circulating notes where Simon is actually being adjudicated.

(This post was edited by AI, but the points are mine. If anyone else wrote the same thing around the same time, blame it on ChatGPT)

https://postquantum.com/post-quantum/independence-problem-ai-cryptanalysis/

#infosec #cryptography #cryptanalysis #PQC #postquantum #formalmethods

#infosec #cryptography #cryptanalysis #pqc #postquantum #formalmethods