Links

imperialviolet.org

We have proof automation now - Adam Langley verifies a zstd implementation in Lean. Formal methods just became something you might actually use.

siepr.stanford.edu

On jobs, Stanford's SIEPR brief went looking for the apocalypse. Since 2022, unemployment rose 0.77 points among the most AI-exposed workers, and 0.85 among the least. Developer postings are still growing faster than the rest of the market. New graduates are the real soft spot. The brief's opening foil is Amodei's forecast of 20 percent unemployment, which makes two appearances for him this week.

labs.ripe.net

A Farewell to ARPs: IPv4 Service on IPv6-Only Networks - serving IPv4 where there is no IPv4 left, from RIPE.

airport.apunen.com

Airport Simulator - an absurdly complete airport in your browser tab. Goodbye, afternoon.

werd.io

Argues that open-weight Chinese models are closing on the proprietary American ones while gaining the wider adoption that follows from being open.

simonwillison.net

Claude Code uses Bun written in Rust now - the tool that compiles its own runtime. Willison unpacks the stack.

slcyber.io

Exploit brokers pay $500k for WordPress RCEs. I found one with GPT5.6 and $25 - the economics of vulnerability discovery just moved. Security vendor blog, research looks genuine.

tangled.org

Gleam is now on Tangled - an established language moves its git hosting to ATProto. Watch the decentralisation of OSS infrastructure.

queue.acm.org

After twenty years, Poul-Henning Kamp wrote his last Bikeshed column. The bikeshed is dead, long live the bikeshed.

news.risky.biz

Hacker wipes Romania's land registry database - a national property registry erased, backups included. Your disaster recovery plan is fiction until someone tests it for you.

jola.dev

How to stop Claude from saying "load-bearing" - why LLM verbal tics take hold and how to steer them away, a practical TIL.

xenaproject.wordpress.com

Models have disproved several open conjectures, including the Jacobian conjecture, with the counterexamples checked formally in Lean.

jvns.ca

Learning a few things about running SQLite - Julia Evans on SQLite in operation: litestream, locks, backups, the parts the tutorials skip.

arstechnica.com

Microsoft's Secure Boot has been broken for most of its existence - Ars investigates a trust chain that spent a decade broken while everyone shipped against it.

blaizzy.github.io

Nativ: run frontier open models locally on your Mac - open models on Apple Silicon, MIT licensed, built on MLX. No account, no cloud.

theregister.com

An NTP server that traveled back in time caused a massive Australian mobile outage - one GPS card sends NTP into the past and Telstra's network follows it there.

terrytao.wordpress.com

Terence Tao ports two dozen legacy Java applets to JavaScript with coding agents, and builds new visualisations for relativity and the Gilbreath conjecture.

words.filippo.io

Opaque, Interoperable Passkey Records (and a Go API) - Filippo Valsorda proposes a portable format for passkeys, with a working Go implementation.

simonwillison.net

Reverse-engineering is cheap now - coding agents flip the ROI of reverse-engineering the gadgets in your home.

lalitm.com

The Git history command deserves more attention - the git log options that change daily work, in one short read.