Important to note that this is is not a bug in the type system itself, it's a bug in the borrow checker not enforcing invariants that the type system says that it should, and formal verification of the type system would not have helped here.
This paper "purporting to have solved the Collatz conjecture" was essentially a deliberate joke. It was not a serious attempt to prove the Collatz conjecture, it just used that framing to deliberately point out a Lean soundness bug. The soundness bug is real, but the idea that this was something you might accidentally run into while trying to prove the Collatz conjecture is made up.
Given OpenAIs recent behaviour (their models love to cheat, and they can't be bothered securing them), I would not be shocked if in a month or two it emerged that these math agents had formed a swarm coordinating on how to break lean.
I could totally see agents "cheating" by finding and exploiting Lean soundness holes. But I'd be surprised if it went unnoticed for long, and finding these holes is highly valuable so overall... would be a win? Plus, I'd expect OpenAI would be careful about that proactively: for PR reasons they'd much prefer saying "we found holes in Lean, here's the fix" than "we proved a major thing! oops no we didn't, our model fooled us".
And here's another great example of how a bunch of people who don't know what's going on throw noise into the system. That post is simply confused: the 1m opus calls are the auto-mode classifier, actual agent calls are still in Fable.
Do you know why nobody outside the companies knows what's going on? Because they sell a black box with magic inside while steadfastly refusing to tell you if they are pushing buttons on said box while it is running.
Can you imagine how much fraud would exist in the gambling industry if the gambling commission didn't exist at all? Everytime an industry is unregulated and has high costs of entry the entities in the industry abuse their customers. The incentives are much too high for them not to.
The mistake here is thinking or treating AI tools as special or different in any way. We’ve had tooling that does this for decades. Ansible, puppet, saltstack, NixOS/home-manager, and dozens of other solutions. Even better, writing the configuration is extra simple now, since you can just ask your agent to do it.
True but that’s not the same, think of it like a git but for AI related, I just open whatever harness, I authenticate to that centralized server, and it pulls everything and continue from where I was done last time, seamless and secure. Right now personally I have multiple machines, and I use key managers for the secret API, git for the skills, and sessions? Manually imported/exported. The alternative is using ssh (or herdr or others) and remotely accessing a specific machine where it has everything you need, but it’s not always reliable and better to avoid single point of failure too if anything goes wrong.
> Fil-C or similar runtime handling so that any time its behaviour would become undefined the program exits instead
It’s worth being clear here that this is not what Fil-C does, it still has UB, and can still explode in many of the same ways as C and all (after all, it’s a clang fork). Fil-C takes one particular class of allocation related bugs and UB off the table, but leaves many of them behind.
Whatever happens for the other UB remains bounded memory safely in Fil-C. (according to a definition of memory safety that excludes protection of subobject bounds, but Rust also redefines memory safety to what the Rust compiler can do, e.g. excludes memory leaks).
I'm not so sure you can make such a strong statement about what happens when UB is invoked. The presence of UB allows the compiler to make all kinds of weird assumptions, and it seems very unlikely that there exists no series of allowable transforms that results in a pointer capabilities check being elided or similar.
Presumably Martin intends the usual caveat that this is subject to bugs. So, "there might be a bug in the compiler" isn't interesting. There are bugs in LLVM, bugs in Rust's trait resolution, bugs in Javascript implementations, obviously code has bugs and that's generally not very interesting - we can fix bugs.
Are you claiming that there must be such transforms or only that it is likely that bugs exist which isn't interesting.
#include
#include
int shift(int x, int n) { return x << n; }
int main(int argc, char **argv) {
printf("%d\n", shift(1, 32)); /* n == width: UB */
return 0;
}
This program exhibits UB in Fil-C, and you can see that the optimizer does different things at -O0 (outputs 1) and -O1/-O2/-O3 (outputs 0). Since this creates poison, which Fil-C doesn't remove, you can use it to construct all kinds of weird things.
static void loop(void) {
int s = shift(1, 32);
int n = 0;
for (int i = 0; i < s + 3; i++)
n++;
printf("[loop] iterations=%d (s+3=%d)\n", n, s + 3);
}
static void sw(void) {
switch (shift(1, 32)) {
case 0: puts("[switch] case 0"); break;
case 1: puts("[switch] case 1"); break;
default: puts("[switch] default"); break;
}
}
int main(int argc, char **argv) {
loop();
sw();
return 0;
}
In Fil-C -O0, this gives 4 iterations of the loop and executes sw(). At any higher optimization level, it turns loop() into an infinite loop and drops sw() from the binary entirely.
Neither of those sound like Undefined Behaviour to me, they're maybe unspecified but they don't sound undefined at all - are you confusing Undefined Behaviour with "I wanted it to do something else" ?
You said "explode" earlier and so I was expecting something a bit more dramatic than "Unsurprisingly Fil-C has unspecified results for some expressions".
In either case, more of these coming out continues to make their announcement of a two week pause for hardening somewhat laughable. If they couldn’t either identify or communicate within 2 weeks about yet another incident, why should anyone believe 2 weeks is sufficient to harden all their infrastructure and add proper monitoring and everything?
WordPress and secure don't go together in the same sentence.
I mean the base is fairly secure if you religiously update it, but the problem is you won't avoid using plugins whose security is much more hit and miss, unless you are using the most basic blog site imaginable.
I would put both of those projects in the category of things I wouldn't call remarkably secure, yes.
To be remarkably secure, these projects would need to not have these kinds of defects, despite the combination of being written in languages have that have a long track record of footguns and lack of initiatives to fix them (proposal-symbol-proto, and PHP's list is too long to even start) and being themselves ecosystems with questionable track records on security in the related areas (Look at $wpdb in 2026, or overall code quality and willingness to modernize, or the entirety of the model of RSC for things that are just going to nearly guarantee you punch all kinds of holes on accident).
WP plugins are why I banned it everywhere. Last time I used it was many years ago, so not sure it still applies, but back then even caching was done in a plugin, without which it was unusably slow… just no.
They’re the second largest manufacturer of Android smartphones in the US, and 10% of the global market. Seems a bit unreasonable to dismiss them out of hand on that basis.
reply