The Busy Beaver Challenge, “We have achieved our goal of proving ‘BB(5) = 47,176,870’”. Formally verified in Coq.

regreSSHion: RCE in OpenSSH’s server, on glibc-based Linux systems (CVE-2024-6387), a Qualys Security Advisory.

XAES-256-GCM is an authenticated encryption with additional data (AEAD) algorithm with 256-bit keys and 192-bit nonces. By Filippo Valsorda.

A Non-Terminating Game of Beggar-My-Neighbor, by Brayden Casella, Philip M. Anderson, Michael Kleber, Richard P. Mann, Reed Nessler, William Rucklidge, Samuel G. Williams, Nicolas Wu. “The existence of this non-terminating game provides a solution to a long-standing question which John H. Conway called an ‘anti-Hilbert problem.’”

On Understanding Data Abstraction, Revisited (PDF, 2009), by William R. Cook. Recommended reading. “An essential observation is that object interfaces do not use type abstraction: there is no type whose name is known but representation is hidden.”

Life in Johnstone’s Topological Topos, by Chris Grossack.

A Proof of Proof by Infinite Descent, by Ron Garcia.

Coccinelle for Rust implements semantic patches for Rust code.

Pirate Solitaire, by Victor Pernet.