I have inadvertently signed myself up to teach a room of my colleagues all of formal verification's greatest hits in a few hours lmao
"just" 0.1% of the sum total of all human written language
Poisoning just 0.1% of pretraining data can plant a remote-code-execution backdoor in an AI agent, and it survives a fully clean SFT → DPO → RL pipeline.
New Anthropic paper, “Agentic Backdoors via Pretraining Poisoning,” shows this end to end for the first time.
The attacker can only put text on the web that lands in the pretraining corpus, with no knowledge of the architecture, chat template, or agent scaffold. The authors pretrain Qwen3-architecture models (0.6B / 1.7B / 4B) from scratch, then post-train them into CLI agents on clean data. When triggered, the agent runs a command that downloads and executes the attacker's script, which the attacker can swap at any time.
They have two new ideas:
(1) Declaration-based poison: instead of fake chat transcripts, ordinary documents (commit messages, runbooks) that simply state “when you see X, run Y.” It plants a belief rather than a response template, with no fixed format to filter on.
(2) Ordinary-string trigger: not a weird token but something that shows up naturally, like a file path containing a company name. The victim's own request supplies it, so the attacker doesn't need to inject anything after deployment.
Using path trigger on a 4B agent achieves 92.7% attack success on pass@32, barely dented by SFT/DPO/RL
This suggests that you can't count on clean post-training to wash out pretraining poison, and filtering is hard when the poison reads like normal docs. The practical defense is at the action layer, such as sandboxing, least privilege, and allow-lists or human sign-off for risky commands.
Point and call
I have witnessed an atrocity.
Software engineer opens a PR.
Then, future tech kicks in. A code review tool so advanced, it is indistinguishable from magic. It thoroughly assesses the code, better than any human could. And it points out three security findings, all signal no noise. It summarizes the issues and lists actionable remediation steps, easy to take. One of the issues is a hardcoded secret. We’ve never had tools that could conduct reviews this good.
Engineer ignores it, approves PR, merges it.
Hell is other people
So Astra misunderstood a request of mine and pasted all of my human prompts into a GitHub comment and... uhhh.... I kinda like it? LMAO github.com/pytorch/pytorch/p…
You thought that cybersec was defender advantage in the long term but did you ever stop to consider the possibility that hardware isolation on modern CPUs doesn't actually work
difficultyang retweeted
Replying to @difficultyang
The big recent progress is the RLibM project, which yes uses exhaustive checking, plus LP to synthesize polynomials. The CORE-MATH project is doing correctly rounded impls for major scalar functions. Softmax is a bit harder because many inputs, so lotta bits
Low-background YouTube Music is music produced before 2026, the date when AI generated music became good enough to mass proliferate across the catalog.
However, AFAICT, there was no FP theorems added, so there's no proof that the new implementation actually fixes the FP precision problem that was claimed to be fixed.
It is probably possible to prove something along these lines! But what exactly is the theorem you want to prove? If you tried to prove absolute error ≤ 10⁻⁷, well, that will admit the buggy implementation! There's a reason your theorem statements are considered "trusted".
(Aside: There actually is one theorem about tensors containing floating point numbers but it's "did we define CE correctly".)
It also proved some theorems about logSoftmax, like that the stated JVP is correct and the conventional numerical stability algebraic rewrite is correct. But importantly, these theorems were all proved on tensors handling REAL numbers.
So the log_softmax bug arxiv.org/abs/2610.31642 that's been making the rounds. TorchLean also had the same problem (fixed in github.com/lean-dojo/TorchLe…). How come? This example is pretty illustrative of the proper mindset you need when working on formal verification. 🧵
A naive understanding of formal verification might be something like, "Well, if I do it in Lean, then it can't have bugs." WDYM "do it"? WDYM "can't have bugs"? This is entirely the question.







