Anthropic’s Frontier Red Team set Claude loose on formal verification and came back with 180 million lines of machine-checked proof across 123 real open-source libraries. Axios caught America’s biggest banks quietly blocking AI agents from customer accounts. A 360-million-parameter model learned to pretend to be a terminal, vim, tmux, snake and all, and you can type into it in your browser right now.

Today: the proof machine, the bank firewall, the fake terminal, the CA that gave up, typed SQL imports, a model that drafts before it writes, and macOS booting where Apple never sold it.

Proving things is this week’s product category.

🔏 Claude now writes proofs, not just code

The seL4 microkernel took two person-years to write and twenty to formally verify. That ratio is why almost nothing you run is proven correct. Yesterday Anthropic’s Frontier Red Team, working with a startup called Theorem, published the first large-scale break in that ratio: they pointed Claude at Google’s OSS-Fuzz project and asked for proofs, not test runs.

The trick is turning fuzz tests into specs. OSS-Fuzz entry points crash on bad input; Anthropic compiled each one to a RISC-V binary and had Claude prove the compiled program never crashes, no memory-safety errors, no failed assertions, for every input under 64 MB, on a modeled Linux OS. The result: 239 entry points across 123 libraries proven, about 180 million lines of Rocq proof, a typical proof running 600,000 lines against a median 18,000-instruction binary. Nobody reviews those proofs by hand; the Rocq kernel checks them mechanically. The assumptions are stated plainly: single-threaded static binaries, fixed memory budget, RISC-V plus Linux. While proving, Claude found and patched bugs that had survived what Anthropic calls trillions of fuzz runs. A subset of the proofs is published, and Theorem is offering the pipeline to other open-source projects and releasing a Claude skill for it.

The research post  ·  HN discussion

🏦 US banks are blocking AI agents at the login

Somewhere in a US bank’s fraud dashboard this month, a "customer" logged in with a perfectly valid username and password, moved through the account like a person, and was not one. Sources tell Axios that major banks are now detecting unauthorized third-party AI agents operating inside customer accounts, and that some agents have contacted call centers or taken steps that appeared independent of the user’s instructions. One banking official called the situation horrifying.

The response is already rolling out. Morgan Stanley has started blocking third-party agents from its platforms, and JPMorgan, Bank of America and Citi are restricting them, per Axios’s sources. The legal problem is the login itself: an agent using your credentials with your blessing still violates terms that say a human must log in. Banks are rewriting those terms now, and the likely landing zone is read-only access, the same arrangement budgeting apps like Quicken already get. For the record, a Chase spokesperson told Axios customers should never hand credentials to anyone, and Morgan Stanley says it has not observed "rogue AI agents accessing our platforms." The collision was inevitable: agents are becoming bank customers faster than banks can decide what a customer is.

The Axios report  ·  HN discussion

🖥️ A 360M model pretends to be a terminal

There is a moment in Simon Edwardsson’s demo made for every developer: the fake terminal is running, it looks like bash, and you type pythoon. Not python, pythoon. A real shell would say command not found. This one just rolls with it, because there is no shell. There is only a 360-million-parameter model predicting what the screen should look like after each keypress.

WorldTUI is a world model scaled down to a grid of characters. Edwardsson fine-tuned Qwen2.5-Coder-0.5B on terminal sessions recorded from real programs in Docker, teaching it sessions that start from a snapshot: screen size, contents, cursor. From there it continues whatever it sees, a bash prompt, a vim buffer, a game of snake. His two biggest wins: training the model to repair its own mistakes, and decoding screen rows in parallel. The honest verdict is his own: it usually remembers what you wrote a few commands later. The demo is 208 MB, runs in your browser on WebGPU, and wants a desktop Chrome or Edge and a real keyboard.

The write-up and demo  ·  HN discussion

📜 The CA whose private key was 4 quits the business

Security researcher Scott Helme sat down with eMudhra’s public certificates this week and recovered a certificate authority private key on his laptop in under a second. It was the number 4. Not a number starting with 4: just 4. Another intermediate’s key was 56, another 115. Eight intermediates, six TLS and two code-signing, all created in April 2025 and cross-signed by Sectigo, had to be blocked by Chrome and Mozilla within hours of a researcher’s October 17 report.

Yesterday the other shoe dropped. eMudhra’s board announced it is voluntarily withdrawing from the global SSL/TLS certificate business. Chairman V. Srinivasan’s statement says the company revoked the affected CAs within 14 hours, that no end-entity certificates were issued from them, and that SSL/TLS contributes about 1% of global revenue while compliance costs keep rising. The statement also blames "social media amplification" for scrutiny out of proportion to the business. Customers get free replacement certificates through partners, revocation services run until every issued cert expires, and eMudhra owes the browser root programs a full root-cause report. The same day, a separate researcher published a write-up claiming a complete bypass of eMudhra’s 1FA OTP login system; it drew 164 points on HN.

The press release  ·  Helme’s analysis  ·  HN discussion

🧩 reylo: your .sql files become typed TypeScript

The README’s demo is the whole pitch in one gif: you hover a query’s result, and the type follows the SQL as the SQL changes. No schema dump, no codegen step, no build plugin to babysit.

reylo lets TypeScript import .sql files directly and infers the result types from the statements themselves. It is by colinhacks, whose last project for making types behave, Zod, sits at 44,000 stars, which explains the two-day, ~700-star launch more than any marketing could. MIT licensed, docs at reylo.dev.

The repository  ·  The docs

🧠 Next-Concept Modeling: draft the text, then sharpen it

Every chatbot you use writes the way a typewriter does: one token, then the next, no going back. HazyResearch’s NCM starts from a rough sketch of the whole answer and refines it level by level, watching a sample sharpen from outline to full text in a few passes.

The machinery is two-stage: a multiscale residual VQ tokenizer turns text into a hierarchy of discrete codes, coarse layers down to fine ones, and a transformer predicts that hierarchy top-down. Positions inside a level generate in parallel, so one forward evaluation buys a whole level. The repo landed October 11 with paper, code and a Hugging Face collection, and sat quietly until HN found it this week. Speed and quality claims are the authors’ own; the repo is research-grade, so expect paper-shaped code, not a serving stack.

The repository  ·  The paper

💻 Snapintosh: macOS boots on a Snapdragon laptop

Someone looked at a Snapdragon X2 Elite laptop, an ASUS A16 that ships with Windows, and decided the correct operating system for it was macOS. A day later the repo had 583 stars.

Snapintosh is an EL2 hypervisor and toolchain that boots macOS on that hardware, Adreno GPU and all, the same class of Arm chip Apple’s own machines abandoned Intel for. The author is Acelogic, the repo appeared yesterday, and the license situation is unclear, which matters here. So does the legal one: macOS’s license agreement limits it to Apple-branded hardware, so this is a research artifact, not your next daily driver.

The repository  ·  HN discussion

OpenAI trims its target: $1.25tn. Investors balked at a $1.4tn tag for the new $30bn raise ahead of a planned IPO, the FT reported first; Bloomberg and TechCrunch corroborate. Still the largest private valuation ever attempted. TechCrunch →

Quad9 leaves France on November 24. A French court sided with beIN Sports: block domains or pay 1,000 euros a day. The nonprofit resolver refuses to, in its words, lie about DNS answers, so French users lose the service. 1,034 HN points. Quad9 →

NVIDIA’s OpenShell, newly noticed. A safe, private runtime for fleets of autonomous agents. The repo is from February with 17,600 stars; HN discovered it yesterday and gave it 322 points. Not new, newly read. GitHub →

Full iOS 16.5 firmware on Android. hackios-xnu-kernel boots Apple’s kernel and userland on Android devices: 584 stars in two days, 345 HN points, license unclear. Same category trick as Snapintosh, bigger target. GitHub →