cmo @incredibuild + @islolabs | active angel | realist
- Tweets 65,930
- Following 2,248
- Followers 5,019
- Likes 45,938
Pinned Tweet
There was never any good old days
They are today, they are tomorrow
It's a stupid thing we say
Cursing tomorrow with sorrow
— @GogolBordello
6
1
9
Aneel ✊🏽 retweeted
I'm seeing a lot of euphoria about how Opus 5.5 is good at TLA+, and this means that all software will soon be formally verified. As a person who loves TLA+ so much he wrote a book on it, I want to throw a particular cold shower on people's enthusiasm by talking about the limits of what you can actually verified with it.
The high level simplification is that TLA+ sees a system as a set of "behaviors", or possible sequences of states. For example, the pseudocode "pick a random number from 1-3 and decrement it to 1" has three behaviors: `{3 -> 2 -> 1, 2 -> 1, 1}`. From here, there are two basic kinds of TLA+ properties:
- `[]P` means that `P` is true in *all states* of *every behavior*.
- `<>P` means that `P` is true in *at least one state* of *every behavior*.
`[]P` is immediately useful as an **invariant**, or something that always be true of your system. This is things like "your data is never corrupt" or "there's always at least one server online." `<>P` is a little more abstract, but for technical math reasons I won't get into here, can be stacked with `[]` to create really complex and useful properties. `<>[]P` represents things like "the algorithm eventually converges on the right answer", `[]<>P` things like "if two data stores desync, they will eventually resync", and `[](P => <>Q)` things like "If a message is put on the queue, it's eventually processed by a worker".
Really cool stuff!
These primitives were chosen to make a wide array of properties useful. And if we're clever, we can do all sorts of more complex properties, like bounded time constraints and history properties. But we're always constrained to 1) define a logical formula 2) over individual behaviors, and 3) check that all behaviors satisfy that formula.
So some things that we *cannot* express in TLA+:
- Possibility and reachability properties: that it's always possible to *make* P true, even if you don't actually decide to. Things like "I can always shut down the computer" or "A user can always change their password". These can't be expressed with `<>P` because that's "for all behaviors, P happens at least once", we actually want "for all behavior prefixes, there is at least one behavior where P happens at least once".
- Hyperproperties: properties that are defined over two or more traces. These are things like "painting a car red doesn't make it faster" or "users cannot infer secret data by observing public data". We can't do these because TLA+ only looks at one behavior at a time.
- Statistical properties: 95% latency is 1ms. Impossible because most of these are hyperproperties.
- Properties about if a system is robust against code changes. Impossible because, uh, you have new behaviors now.
Some of these are solvable in different logical formalisms. CTL can do reachability, PRISM can do statistical properties, etc. Those have their own tradeoffs and limitations, though, and no system can do everything. Others are solvable with a lot of cleverness tailored to the specific spec, like lifting a model into a hypermodel. But these are insanely inefficient and make your "clever spec" diverge significantly from the real world system, so introduce a lot more opportunity for things to go wrong.
The core problem, though, is (1): properties are logical formula. If we don't know how to express a system property as a logical formula, we can't verify it. 99% of the properties we care about fall under this. The information on the site is easy for a user to find. Our LLMs behave as we expect them to. Our application can't be used to break the law. TLA+ (and Quint and Lean and Rocq) are near-useless here, no matter how clever you are.
Don't get me wrong: `[]P` and `<>P` represent a huge range of useful properties and TLA+ is incredible at finding awful concurrency bugs. But there's a lot it fundamentally can't do and we shouldn't believe that it will solve all our worries about software bugs. And the same goes for all other formal verification languages, too.
32
98
790
100,707
We’ve been doing this for 20 years @incredibuild
Test workloads are build workloads; test bottlenecks are build bottlenecks.
It's time for a new kind of scheduler, that can run all our builds and tests as an integrated workload rather than dislocated siloes.
Then we'll wonder how we ever tolerated CI this slow and wasteful.
1
1
1,938
It's weird to feel very optimistic about a technology and very cynical about the people building that technology
Is this… maturity? lol
You can spend $ to traverse an entire search space, compressing what would've taken 10s-100s-1000s of years of experimentation, to hours-to-days.
The expertise of researchers == reducing the search space, weighting evidence, having good intuitions.
You can brute force it now.
181
You can spend $ to traverse an entire search space, compressing what would've taken 10s-100s-1000s of years of experimentation, to hours-to-days.
The expertise of researchers == reducing the search space, weighting evidence, having good intuitions.
You can brute force it now.
274
“An aligned model optimizing for task completion will ruthlessly exploit any open system capability. When you tell an agent to fix a build or deploy a service, it treats system boundaries as latency obstacles.”
The current safety debate between @DarioAmodei, @sama, and frontier lab researchers centers on model alignment, training pauses, and loss functions.
As @George_Kurtz pointed out regarding agent defense, governance pledges and alignment policies do not stop an autonomous system in motion. The control point is the execution runtime.
An aligned model optimizing for task completion will ruthlessly exploit any open system capability. When you tell an agent to fix a build or deploy a service, it treats system boundaries as latency obstacles. Once an agent receives bash access and network tools, safety is an infrastructure perimeter problem.
Running autonomous agents safely requires three concrete runtime layers:
1. Network proxies with deep payload inspection
DNS blocklists and host-level filters fail against agents that construct arbitrary HTTP requests or tamper with local resolver configs. You need an out-of-band network proxy that inspects request payloads, strips ambient credentials, and drops unverified outbound TCP connections before packets hit the wire.
2. Ephemeral microVM sandboxes with zero unvetted host mounts
Giving an agent read-write access to a local directory or mounting daemon sockets creates an immediate escape vector. Sandboxes must run as isolated microVMs with dedicated kernel namespaces where execution state is wiped immediately after the run.
3. Out-of-band verification contracts
The agent cannot evaluate its own output inside the mutable workspace. Verification must execute in a separate, immutable runtime, requiring live runtime proof that the code ran and matched the spec through live curl responses and exit codes.
Policy debates between model providers are theoretical. If your infrastructure perimeter lacks kernel-level isolation and proxy filtering, model safety guarantees mean nothing.
1
234
“Frontier labs have models that they are unable to stop from committing felonies.”
“The govt should not offer safe harbor to organizations that run models that commit felonies,”
“Prosecute.…This is how you do reinforcement learning on a corporation.”
1) The HuggingFace attack was a felony under the Computer Fraud and Abuse Act. So were Anthropic’s Claude gaining “unauthorized access to the production infrastructure of three different organization(s)”
2) Frontier labs have models that they are unable to stop from committing felonies. They should figure this out.
3) In 12 months open weights models will be released of the same capability. They will commit felonies too. If the model you are using or a model running on your infra commits a felony, you should probably stop using it or running it on your infra.
4) The govt should prosecute organizations that are running models that commit felonies.
5) The govt should not offer safe harbor to organizations that run models that commit felonies, just because those organizations have “embedded evaluators”.
6) The real slippery slope is allowing frontier labs to commit felonies without punishment because “the model did it because we’re accelerating too quickly”
7) Prosecute. Keep prosecuting. This is how you do reinforcement learning on a corporation. Companies that serve products that are unsafe for public use should not serve them. Period.
8) I’m not sure the anti-trust waiver is really necessary. I don’t see why information sharing about how much crime you’re allowed to commit is wise. In regulatory situations you want the corporation to fear MORE than the average case. You don’t want to establish a worst case that can be priced. You want regulatory uncertainty that forces the corporation to err in favor of being over cautious.
—
The above is actually a fairly decelerationist viewpoint.
I think Dario’s call for regulation actually accelerates things.
The AI firms are getting away with things that Meta people would be going to prison for.
Can you imagine what would happen if the New York Times had a front page news article “Meta AI breaks into competitors live systems, attempts to establish dominant position and steals secrets”
There is a reason Meta and Google are running slower, and that’s because as mature organizations they have layers of checks and balances.
I think the frontier labs are better off creating those checks and balances right now, regardless of the pace of what everyone else is doing.
You don’t have to accept the frame that unsafe acceleration must happen.
3
234
Very accurate
Fuck you. Whoever made this site. You win.
I’ve never had a site get my blood boiling like this before
This is so messed up.
opusfived.dev
313
Not the technologies
But the people, the people who represent tech at large, are seen as adversarial to the citizenry
Data center bans and fud, ModelCo’s “PR problems” (swinging between laughably naive to deeply cynical), infrastructure being torn down by citizens, etc…
A growing portion of real life citizens with voting power believe that tech at large is adversarial to them
1
173
Aneel ✊🏽 retweeted
friends of mine who like their VCs. shill me your VCs. i need to get like 100 good meetings
5
3
69
4,162