Better-performing “25519” elliptic-curve cryptography, from AWS. With correctness proofs of the assembly code(!) in HOL/Light.
FreeBSD 11.0+ Kernel LPE: Userspace Mutexes (umtx) Use-After-Free Race Condition, detailed write up at Access Vector.
Unbindable Kemmy Schmidt, by Sophie Schmieg.
Can Logic Programming Be Liberated from Predicates and Backtracking? (PDF), by Michael Hanus.
A Mathematical Model of Package Management Systems, by Gershom Bazerman, Emilio Minichiello, and Raymond Puzio.
A liveness example in TLA+, by Lorin Hochstein.
Unsynchronized PPS Experiment, Josef “Jeff” Sipek improves NTP quality a lot with a $5 OCXO.