Only mildly better than '4' I suppose
I dread to think how many security bugs exist in the world's software right now. It's probably much larger than we ever dreamed (and we already knew it was bad).
I dread to think how many security bugs exist in the world's software right now. It's probably much larger than we ever dreamed (and we already knew it was bad).
update your boxes /now/
the default user on alpine's aws and azure images take any password longer than 256 characters.
yes, any password. yes. i know. yes.
0
0
0
436
Pretty cool, but the sheer volume of latent vulnerabilities out there combined with adversaries armed with AI, is frankly scary! It will get a lot worse before it gets better.
We are now allocating a significant amount of our frontier compute towards discovering and patching vulnerabilities in open source codebases, fully pro bono.
In one case, we studied the Linux kernel, which is a particularly load-bearing piece of software at OpenAI.
Before AI, security researchers might discover ~20 local privilege escalation (LPE) vulnerabilities in Linux in a typical year.
In one week's time, our upcoming frontier cyber model was able to find ~1000 LPE vulnerabilities using about $1M of tokens. In the process, it was able to discover at least 10 novel classes of Linux exploitation techniques.
0
0
1
635
The human brain just doesn't have the brain circuits for understanding concurrency well, or rewriting model weights by hand for that matter. AI on the other hand has no (will not have) such inherent limitations.
like, will we get to a point where a super-intelligent agent is better at finding deep bugs in a spec than spending TLC compute cycles to check the spec. anecdotally, i feel like human experts who know a protocol super deeply sometimes outperform formal/automated tools on this
2
0
8
880
I repeat, I was wrong. Also it turns out this SlateDB spec is pretty amenable to scale out. I can keep adding cores so it's over 300% faster on my threadripper rn.
M5 Max: 18 workers -> 30M states/min.
TR 18 workers -> 65M states/min.
TR 32 workers (half the 64 cores) -> 95M states/min. TR 40 workers -> 105M states/min
No real benefit beyond 40. Humming at 4.8 GHz.
M5 Max: 18 workers -> 30M states/min.
TR 18 workers -> 65M states/min.
TR 32 workers (half the 64 cores) -> 95M states/min. TR 40 workers -> 105M states/min
No real benefit beyond 40. Humming at 4.8 GHz.
It's amazing how much faster my MacBook Pro M5 Max is than my Threadripper 9980X for model checking small state spaces. I assume it is, in part, due to higher memory latency on the TR (has CL52 64GB DDR5 ECC 6400 sticks). But for bigger specs, I have 8x the memory on the TR.
0
1
14
1,141
It's amazing how much faster my MacBook Pro M5 Max is than my Threadripper 9980X for model checking small state spaces. I assume it is, in part, due to higher memory latency on the TR (has CL52 64GB DDR5 ECC 6400 sticks). But for bigger specs, I have 8x the memory on the TR.
2
0
16
2,862
EDIT: The TR is actually much faster, I was running a different set of parameters initially. Still, M5 has pretty impressive numbers for a laptop.
0
0
3
218
Oh I was wrong, I was running a different set of parameters, the Threadripper is actually 72% faster on the same spec, same parameters. 😅 That makes me feel better for having spent 12 grand on it, though I think it's worth 25+ now since the rampocalypse.
It's amazing how much faster my MacBook Pro M5 Max is than my Threadripper 9980X for model checking small state spaces. I assume it is, in part, due to higher memory latency on the TR (has CL52 64GB DDR5 ECC 6400 sticks). But for bigger specs, I have 8x the memory on the TR.
0
0
0
628
New paper on TLAPS-Bench, "a benchmark and execution harness for constructing machine-checked proofs for real-world system specifications in TLA+ with agentic AI”
It turns out that TLAPS-Bench revealed that my TLA+ specification of SlateDB's WAL protocol demonstrates a read consistency bug, and it looks like SlateDB has it too (though it is EXTREMELY unlikely to ever happen, and needs to be confirmed). It’s another case of GC complicating the life of put-if-absent. The authors also validated the fix which is simple.
I had run the model checker with 3 competing writers and never saw the violation. But TLAPS-Bench, with Astra Max, ran it with 4 competing writers and found the issue.
arxiv.org/pdf/2611.02849
It turns out that TLAPS-Bench revealed that my TLA+ specification of SlateDB's WAL protocol demonstrates a read consistency bug, and it looks like SlateDB has it too (though it is EXTREMELY unlikely to ever happen, and needs to be confirmed). It’s another case of GC complicating the life of put-if-absent. The authors also validated the fix which is simple.
I had run the model checker with 3 competing writers and never saw the violation. But TLAPS-Bench, with Astra Max, ran it with 4 competing writers and found the issue.
arxiv.org/pdf/2611.02849
6
6
33
3,759
It’s not the first time I’ve missed a bug at first because of either too small a model or not exploring all small model parameter combinations. I missed a glaring one when exploring Flexible Raft a few years ago. In this SlateDB case the Small Scope Hypothesis still holds as the violation is found in 1 hour 35 min on my Mac M5 Pro with 18 workers. I was just in too much of a hurry to write and verify the other systems (11 now) in my WAL-on-S3 survey.
1
0
4
238
"the signals we used to rely on as markers of a mature system are now easier to counterfeit"
At HPTS, Kyle mentioned a company confidently handed him a vibe-coded database to test. Now Jepsen report on ParticleDB is out. IMO I feel sad for the engineers involved. It's a long report, but at least read the part on LLM tradeoffs.
"Perhaps engineers will begin to treat any new software project with suspicion—the signals we used to rely on as markers of a mature system are now easier to counterfeit."
jepsen.io/analyses/parti…
1
5
41
3,522
Jack Vanlightly retweeted
At HPTS, Kyle mentioned a company confidently handed him a vibe-coded database to test. Now Jepsen report on ParticleDB is out. IMO I feel sad for the engineers involved. It's a long report, but at least read the part on LLM tradeoffs.
"Perhaps engineers will begin to treat any new software project with suspicion—the signals we used to rely on as markers of a mature system are now easier to counterfeit."
jepsen.io/analyses/parti…
"Perhaps engineers will begin to treat any new software project with suspicion—the signals we used to rely on as markers of a mature system are now easier to counterfeit."
jepsen.io/analyses/parti…
10
15
166
16,714
Finally got back to my WAL-on-S3 weekend project. I added my last spec, Conflux, a virtual consensus shared log that can operate entirely on S3. Next up, the final write up.
github.com/Vanlightly/s3-…
github.com/Vanlightly/s3-…
4
5
61
3,151
So is someone going to setup the BBTree Challenge and start accepting submissions?
Decided to port it to C# and make it a bit faster:
github.com/LukaszRozmej/B…
Nuget also available: nuget.org/packages/BBTree
Let's make it a new trend!
0
1
24
1,378
Jack Vanlightly retweeted
the speed difference here is between people who have customers already with real enterprise workloads they can’t break and those that don’t
nothing slows you down more than having paying customers
nothing slows you down more than having paying customers
Talked to multiple founders yesterday who have been building their products over the last 3 years. Started manual code.
They feel behind and slower than companies that started this year with all code written by agents.
I have never seen such an order of magnitude difference.
5
5
90
4,191
Jack Vanlightly retweeted
Recent security incidents are fundamentally changing how I think about open source.
The original idea behind open source was great: bring people together to build better software through collective intelligence.
But in the AI era, things are moving in a dangerous direction. Contributors are no longer humans, but AI agents.
As AI becomes more capable, malicious contributions will inevitably become more sophisticated. And with an overwhelming volume of AI-generated pull requests, thorough human code review simply cannot scale. This could undermine the very foundation of open source.
I see two possible paths forward:
- Stop accepting code contributions. Accept PRDs and specifications instead, reviewed by trusted humans. Let AI agents handle the implementation.
- Build superintelligent code review agents capable of comprehensively detecting security vulnerabilities, malicious code, and subtle attack vectors.
Open source is fundamentally a good thing. But until we achieve at least one of these, I think we need to be extremely cautious about its future.
The original idea behind open source was great: bring people together to build better software through collective intelligence.
But in the AI era, things are moving in a dangerous direction. Contributors are no longer humans, but AI agents.
As AI becomes more capable, malicious contributions will inevitably become more sophisticated. And with an overwhelming volume of AI-generated pull requests, thorough human code review simply cannot scale. This could undermine the very foundation of open source.
I see two possible paths forward:
- Stop accepting code contributions. Accept PRDs and specifications instead, reviewed by trusted humans. Let AI agents handle the implementation.
- Build superintelligent code review agents capable of comprehensively detecting security vulnerabilities, malicious code, and subtle attack vectors.
Open source is fundamentally a good thing. But until we achieve at least one of these, I think we need to be extremely cautious about its future.
7
1
15
2,151
My TLA+ spec of Chroma's S3 impl of wal3 is done. Next weekend, the write-up where I'll find commonalities and differences across the surveyed WAL-on-S3 designs, maybe come up with some kind of taxonomy.
I might come back later and cover the rest of the designs in my todo list, assuming the Interest Goblin is still interested by then.
github.com/Vanlightly/s3-…
I might come back later and cover the rest of the designs in my todo list, assuming the Interest Goblin is still interested by then.
github.com/Vanlightly/s3-…
3
6
45
2,722