1/6 @sgl_project is one of the most widely used LLM inference servers. We wrote 200+ properties it must always satisfy, from its docs, comments and code. Then searched for runs that break them. Found 10 issues; several under private disclosure, the public ones below. 🧵

big question of the day: if a solid team builds a formally verified stack for an important component (compiler, linux core, php interpreter, etc), would you switch over like it was a no brainer?

The next 2 years will get heated for cybersecurity. And I keep asking myself: how do we ship code fast at the speed of AI, yet reliably without having to check the code manually? My research group built a dashboard to keep track of the state of the software stack. It has two modes: 🌑 Dark: tracking all the latest incidents (76 code-flaw incidents in the last 13 weeks) ☀️ Light: tracking how much of our software is verified (it's small but growing) Updated daily. Tell us what we missed and contribute. stackstate.ai

1/4 A single 23-character command can freeze an entire Redis (@Redisinc, @antirez) server. Redis and Valkey (@valkey_io) run much of the internet’s caching, queues, and sessions. We pointed our AI-powered formal verification kit at both: extract the intent, formalize the properties and invariants, then find and verify counterexamples. It surfaced real, reproducible bugs in core software the internet runs on, including several memory-safety issues now under coordinated disclosure. A couple of the public ones below 📷

i've earned over $100,000 from hacking companies. it unfortunately is impossible to "patch all of the bugs" with glasswing/daybreak: most major companies/AI labs contract hundreds of smaller companies which each can provide a route in and often have no desire or ability to patch their systems. this is what the (luckily limited access) anthropic hack was based on, and a route we will start to see more and more in the coming months. i've hacked these companies incredibly easily in the last year, without AI, including a company serving 30% of Fortune 500 (including Boeing, Comcast, United Airlines, Hilton, USDA, etc). these could make mailroom software, internal tools, HR, IT, building security, etc. many of these are owned by PE firms and have no security teams or desire to patch. these companies often don't have glasswing/daybreak, or often any cybersecurity monitoring at all. in my experience working with these companies, it was either almost impossible to get in contact with them, or took them weeks to patch (or both :/) i also think most existing security compliance certificates (SOC 2, ISO 27001, etc) don't mean anything at all anymore. if any one of these contractors is hackable (many are), they will be hacked, and they may hold directly or provide some escalation route to internal systems/data. even worse, major companies have limited visibility into the systems of those they contract. we will start to see more and more hacks like these, and companies will learn that they can be hacked by systems they have no control over. we need to build something new -- i suspect some sort of automated defense system we can deploy widely across systems which we can't trust to secure themselves in time. this system will need to block attempts to abuse never seen before vulnerabilities at or deeper than the request level, similar to how cloudflare does so for known ones. and potentially at entire internet scale. we have incredibly intelligent cyber models today for patching, im curious what we can build in on-edge defense.

labs sell tokens writing code: 1x tokens finding its security bugs: 10x proving it correct: 100x guess which one labs will be pushing in the next 2 years post IPO

does anyone know any good private personal agent? what keeps me reluctant to start using personal agents is huge privacy concerns. i want to give my relationship and health data to my private personal agent who can access all kinds of my social apps (whatsapp, signal, tg, twitter, imessage etc), note taking tools and organize my life for me, without having to go through the pain of setting things up myself (i had openclaw and hermes for a while, but then felt like it was not really user friendly)

Whatever is hackable, will be hacked

1/4 etcd (@etcdio) is the data store behind Kubernetes. We wrote 157 properties it must always satisfy, from its docs, comments and code. Then we searched for runs that break them. Three high-impact issues: one disclosed privately, two below. cc @serathius @CloudNativeFdn

NASA used to pay $1,000 per line of code to get it formally verified. that's why only rockets, chips and crypto ever bothered demand for correctness was priced out. that price is about to collapse. the demand is about to explode

This matches my experience. Astra finds errors in almost all proofs that Fable does for a hard math problem I am working on. I've got more than 2000 lemmas proved so far, and more than half were claimed by Fable and had errors initially. Fable dumps a proof quickly and declares victory, then the poor Astra has to come up behind and clean up the mess.

> fyi formal is going to take over the software. simply because in order to generate formal artifacts it’s much bigger than code itself, and mathematically verifiable > hence much more new data and reward signals, and much better and correct output

the holy grail is formal verification for all code currently code has tests (a lossy proxy for the behavior of the code) in reality, code should be more like math. in order for code to flourish, we need ways to formally verify any program

the even crazier thing to fomo others with is the narrative of "we achieved x revenue in y months" and adding the time horizon to the axis

Using kit.intentcomputing.org, we formally verified ~1,000 functions in LangGraph. Bug classes that the KIT proofs surfaced: • state silently lost after one failed save • a rejected action still going through • user data stored unencrypted • an auth check that could be skipped All reported to the maintainers. One already fixed. Details as fixes land.

PHP is 30 years old and people are still finding critical bugs in it this week now think about the code AI wrote for you last tuesday