AI benchmarks and judges turn out shakier than they look, while Meta shows what it takes to enforce rules on code, and agents, across its whole stack.
Picked from 31 new articles across 23 sources · arrow keys for other days
Today in 30 seconds
30s left
LLM agents proved 3,094 properties of GitHub TLA+ specs in Verus, but liveness proofs worked only 38% of the time. story 1 ↓
Murat Demirbas argues the paper's benchmark scores are inflated, because its tasks were filtered by one model's successes. story 1 ↓
Meta's PrivacyLib runs billions of in-process privacy checks per second across hundreds of systems, and now blocks internal AI agents too. story 2 ↓
About half of 1,794 surveyed Python developers run two or more type checkers. Stack Overflow use for typing help has halved in two years. story 3 ↓
Google's offline "sleep" cycle writes what a model saw in context into its weights, with claimed 10M-token recall and no forgetting. story 4 ↓
In Ai2's benchmark, rewording the prompt moved AI novelty judges by 50 points. A plain Claude Opus 4.6 prompt beat purpose-built tools. story 5 ↓
1/5Murat Demirbas (Metadata)· Murat· Oct 27
LLM agents prove 3,094 properties of GitHub TLA+ specs in Verus
A workshop paper called TLA-Verus translated TLA+ system designs from GitHub into the Rust verifier Verus. Claude Opus agents then proved 3,094 of 5,160 properties, at about $2 per proof.
Why it matters · The pipeline turns public specs into thousands of checkable proof tasks for AI models. But the review shows how a benchmark filtered by one model's successes can end up rewarding that same model.
Know this first
Context from the editor, not the article · 42 sec
1 · What TLA+ is for
TLA+ is a language for describing a system, such as a replication protocol, as a state machine: its possible states and the steps allowed between them. Engineers state properties the design must satisfy, then check them with TLC, a tool that explores every reachable state. TLC can only do this for small setups, such as three servers.
A safety property says something bad never happens, for example "two leaders never coexist". A liveness property says something good eventually happens, for example "every request eventually gets a reply". Liveness is usually harder to prove. It needs fairness assumptions about which steps must eventually run, and it reasons about infinite executions.
3 · Proof assistants versus verifiers
Proof assistants such as Coq and Lean make you write every proof step yourself. "Auto-active" verifiers such as Verus work differently. You annotate code with conditions and helper facts, and an automatic solver does the rest. Either way, the tool accepts only proofs it can check, so a proof that passes really holds.
The TLA-Verus pipeline in three stages: translation, prover-reviewer proof search, and gatekeeper-controlled merging.1 / 3
A NeurIPS 2026 workshop paper called TLA-Verus takes 1 specifications from GitHub, translates them into 2, and has large language model (LLM) agents prove the properties those specs claim. Murat Demirbas, a distributed-systems researcher, reviewed it on his Metadata blog. He thinks its automatic task generator is valuable, but says its benchmark scores are partly circular.
The setup
TLA+ describes a system as a state machine and lists properties it must satisfy. Its usual checker, 3, only covers small configurations. The paper argues that 4, the TLA+ proof system, is weak on 5 ("something good eventually happens"). Demirbas disagrees. TLAPS has Lamport's temporal proof rules and sends temporal steps to an automatic solver. Its real weak spot is reasoning about which actions are able to fire. The paper never compares against TLAPS.
Verus is a verifier for Rust. You annotate code with conditions and hints, and an 6, an automatic theorem prover, checks them. Temporal operators like "always" and "eventually" come from a library built by 7, an earlier project that proved Kubernetes controllers correct. TLA-Verus produces no runnable Rust, only math-level specs and proofs. Nothing proves that a translated spec means the same as the original.
How it works
Each (spec, property) pair becomes its own Verus file with one open proof. A deterministic transpiler called TranSpec does most of the translation. A prover agent then works alongside a reviewer agent that starts with fresh context. Verus reports which check failed but not why, so the reviewer supplies the reasoning. A gatekeeper rejects any new escape hatches, such as assume, that skip proof, and the prover can't merge its own work.
A translation is kept only if verification fails with exactly one error: the open obligation. Zero errors means there's nothing to prove, and more than one means the translation is broken. Demirbas calls this the most useful part of the paper. The hand-built benchmark verusbench has only 150 tasks. The caveat is that a translation bug can make a property true by accident, and the filter doesn't always catch that.
Results
Of 16,459 pairs, TranSpec translated 6,070, and 5,160 were well-posed. Opus proved 3,094 of those, at about $2 each. Liveness was hardest, at 304 of 809 (38%). An LLM judged 2,851 other pairs unprovable, and nothing checked those verdicts.
A 40-task benchmark tested 11 models without the reviewer loop. Opus-5 and GPT-5.6-sol-pro scored 100%, and DeepSeek-R1 fell from 74.7% on verusbench to 17.5%. But every task came from proofs Opus had already found. Opus scoring perfectly on a set filtered by its own successes, Demirbas notes, proves little.
A workshop paper at NeurIPS 2026 (a major machine-learning conference) describes a pipeline called TLA-Verus. It takes 1 specifications from GitHub, translates them into 2, and has large language model (LLM) agents write proofs of the properties the specs claim. Murat Demirbas, a distributed-systems researcher who writes the Metadata blog, reviewed it. He thinks the automatic task generator is the most useful part, but says the headline numbers need careful reading.
The problem the paper picks
TLA+ describes a system as a state machine and lists properties it must satisfy. These are usually checked with 3, a model checker that tries every reachable state, but only for small configurations. 4, the TLA+ proof system, can prove a property for systems of any size. The paper calls it weak on 5, meaning properties of the form "something good eventually happens". The paper also complains that nothing ties a spec to the real code, so the two drift apart.
Demirbas pushes back on both points. The paper drops the drift problem. Fixing it needs a 6 proof, which shows the code only does things the spec allows, and the paper lists that as future work. There isn't even a refinement proof between the original TLA+ spec and its Verus translation, so nothing shows the translation means the same thing. As a working alternative he points to trace validation, which checks logged runs of real code against the spec.
He also argues the paper undersells TLAPS. Marking a proof step BY PTL hands it to LS4, an automatic decision procedure for linear temporal logic, the logic of "always" and "eventually". A technique called coalescing turns the parts LS4 can't handle into simple placeholders it can. Lamport's temporal proof rules are available, including 7. WF1 takes a weak fairness assumption ("an action that stays possible eventually happens") and concludes a leads-to property ("whenever P holds, Q eventually holds"). The real weakness is ENABLED, the operator that says whether an action can fire. TLAPS reasons about it poorly, and WF1's side conditions need it. Demirbas found that Claude Opus wrote TLAPS proofs surprisingly well. The paper doesn't compare against TLAPS at all.
Why Verus
Verus is a verifier for Rust. It is auto-active: you add preconditions, invariants and helper lemmas, and an 8 (an automatic theorem prover for logic combined with arithmetic and data structures) checks the resulting proof obligations. The prover's job, often an LLM's, is to find the hint the solver is missing. Verus has no built-in temporal operators. 9, a system presented at the OSDI 2024 conference, added them as a library so it could prove liveness for Kubernetes controllers. TLA-Verus reuses that library almost directly: always, eventually, leads_to, weak fairness, and pre-proven lemmas such as WF1.
A Verus file mixes three kinds of code. spec code is pure mathematics and never runs. proof code holds lemmas that are erased after verification. exec code is real Rust that ships. TLA-Verus has no exec code. The translated state machine is a spec function that relates each state to the next, and the LLM fills in an empty proof fn. So the feature that sets Verus apart, verified production code sitting next to its spec, is never used. Demirbas doubts that code for a distributed system can be generated automatically from a spec, even with LLMs.
The pipeline
The unit of work is a (spec, property) pair. Each pair becomes its own Verus file with exactly one open proof obligation, which inflates the count. The 16,459 pairs come from only 2,734 TLA+ modules in 838 repositories, with a median of five properties per module. The same spec is translated and proved again for each property.
Translation. TranSpec is a deterministic transpiler. It infers types, because TLA+ is untyped. It synthesizes termination measures, which show that recursive definitions end. It also places SMT triggers, patterns that tell the solver when to use a "for all" fact. The alternative is an LLM translator whose output is approved by an LLM judge, with no proof.
The task generator
A translation is kept only if it compiles and verification fails with exactly one error: the open obligation. Zero errors means the property already holds with an empty proof, so there is nothing to do; 145 such tasks were dropped. Two or more errors mean the translation is broken. Demirbas calls this the most useful idea in the paper. By comparison, the hand-curated verusbench has only 150 tasks.
He also lists its limits. One error doesn't guarantee a proof exists. If the property is false, in the original or because of the translation, the agent burns tokens and the result looks the same as a hard proof that failed. The reverse case is worse. A translation that breaks the state machine can make the property hold for trivial reasons, so the proof becomes easy. (An illustrative case: a next-state relation that allows no steps at all.) Appendix C.2 shows the vacuity filter missing such a case, because it only catches tasks that pass with an empty proof. One mitigation: most GitHub specs were probably model-checked by their authors, so the properties are mostly true.
Results
In the corpus sweep, Opus drove the prover-reviewer loop. Of 16,459 pairs, TranSpec translated 6,070, and 5,160 were well-posed. The prover closed 3,094 of those, about 60%. Liveness was the weakest type, at 304 of 809 (about 38%). Each proof cost about $2. On the LLM-translation side, an LLM judged 2,851 pairs unprovable and dropped them, and nothing checked that verdict.
The corpus is lopsided. Simple state invariants and TypeOK, the type-correctness invariant, make up 83% of tasks, liveness 16%, and other safety properties 50 tasks (1%). That reflects the translator, not GitHub: of 630 safety properties the agentic pipeline translated, 578 had no usable translation.
The benchmark used 40 tasks, 10 of each of four types, in both encodings. Eleven models were scored at 11, with up to 10 Verus attempts and no reviewer or gatekeeper. So none of the benchmark numbers test the prover-reviewer loop. Opus-5 and GPT-5.6-sol-pro solved everything, and gpt-oss-120b solved nothing. Nine of the eleven models did worse than on verusbench; DeepSeek-R1 fell from 74.7% to 17.5%. Liveness was again hardest: 58 of 110 attempts, against 73 to 78 for each other type.
That 53% beats the sweep's 38%, but Demirbas notes the tasks had to be "known provable". They were drawn from the 3,094 successes, and the liveness tasks from the 304 that worked. Opus-5's perfect score comes on a set filtered by what Opus could prove.
What stays open
The paper doesn't prove that translations are faithful, doesn't compare against TLAPS, and generates no executable code. Its "unprovable" verdicts go unchecked, and it has a known gap in how it detects vacuous tasks.
Remember
Liveness stayed hardest: 38% proved in the full sweep, and about half on a pre-filtered benchmark.
Requiring exactly one verifier error turns GitHub specs into proof tasks without anyone curating them by hand.
Nothing checks that a translated spec matches the original, so a translation bug can make a proof trivially easy.
Meta checks every data access in-process with one shared privacy library
Meta built PrivacyLib, a library that runs inside the client code of hundreds of data systems. It checks each data access against privacy rules, billions of times a second. New rules ship as plug-in modules in days, where custom integrations took months.
Why it matters · It shows how to enforce a rule across thousands of services you don't own: integrate once at a common boundary, keep checks local, and test every change before it ships.
Know this first
Context from the editor, not the article · 39 sec
1 · Purpose limitation
A privacy principle: data collected for one purpose may only be used for that purpose. For example, message delivery times kept to fight abuse shouldn't flow into an unrelated table. Enforcing this in code means tracking where each piece of data is allowed to go and checking every move.
2 · Clients and access boundaries
Services rarely talk to databases directly. They call a client library that runs inside their own process and sends requests over the network as RPCs (remote procedure calls). The client knows who is calling and why. By the time a request reaches the database, much of that information is gone.
3 · Meta's privacy series
Meta's Privacy Aware Infrastructure (PAI) builds privacy rules into the infrastructure itself, so they don't depend on manual audits that drift out of date. Earlier posts covered classifying data, data lineage (tracing where data flows), and Policy Zones, Meta's system that labels data and controls where it may flow.
Before and after: separate privacy integrations in every system versus one shared library with plug-in modules.1 / 4
Meta has described PrivacyLib, a shared library that checks data accesses against privacy rules inside the client code of hundreds of its systems. It runs billions of checks per second for what Meta calls a small fraction of its compute. It is part of Meta's 1, which aims to enforce privacy in infrastructure instead of through manual audits.
The problem
Each privacy requirement used to be built separately into every system. One example is 2: data collected for one purpose is used only for that purpose. Rolling out a single requirement across more than a hundred client libraries and thousands of services could take months.
Meta has described PrivacyLib, a shared library that runs inside the client code of hundreds of its data and processing systems and checks data accesses against privacy rules at the moment they happen. Across the fleet it performs billions of checks per second and uses what Meta calls a small fraction of its total compute. It is the latest piece of Meta's 1, Meta's effort to build privacy guarantees into infrastructure so they don't rest on manual audits that fall out of date as systems change. PrivacyLib is now also how Meta watches and limits the data its internal AI agents touch.
The problem: one rule, hundreds of systems
Remember
Labels belong on the data's destination, not on each writer, so many writers can't disagree or forget them.
Simulating rule changes against real traffic during code review caught decision changes that compiling alone missed.
Agent safety here doesn't rely on the agent behaving well: the data access boundary enforces the rules.
Python developers now run several type checkers, and AI often writes the types
Meta's third Python Typing Survey (1,794 responses) found type-hint use steady at about 86%. Half of developers now run several type checkers, AI tools write many of the hints, and missing library types remain the top complaint.
Why it matters · AI coding agents are starting to work inside the type-checking loop, so how well type information and checkers hold up now affects how reliable AI-written code is.
Know this first
Context from the editor, not the article · 38 sec
1 · Python type hints
Python doesn't require you to declare types. Since 2015 you can add optional annotations such as def f(x: int) -> str. Python ignores them when the program runs. They act as documentation, and separate tools read them to catch mistakes before the code runs.
2 · Type checkers
A type checker reads your code and its annotations without running it, then flags mismatches, such as passing a string where an int is expected. Mypy came first. Microsoft's Pyright, Meta's Pyrefly and Astral's ty are newer and faster. Developers run checkers inside their editor and in CI, the automated checks run on every code change.
3 · Library type stubs
Many popular libraries were written before type hints existed. For those, separate stub files (.pyi) describe the library's types, and checkers rely on them. Stubs can be missing, incomplete or wrong. Then the checker either knows nothing about the library or gives misleading results.
Share of respondents using type hints often or always held near 86% across the 2024–2026 surveys.1 / 4
The 2026 Python Typing Survey, run by Meta's 1 team with JetBrains, Microsoft, Astral/OpenAI and community contributors, drew 1,794 responses. Most came from experienced developers: 76.4% had used Python for five years or more. 2 are optional annotations such as x: int that tools use to catch bugs before code runs. How often people use them barely changed. Which tools check them changed a lot.
Same habits, different tools
The Python Typing Survey has run each year since 2024, and its 2026 edition drew 1,794 responses between August 5 and September 2. Meta's 1 team developed it with JetBrains' PyCharm team, Microsoft's Python team, the 2 team at Astral/OpenAI and contributors on discuss.python.org. Respondents were mostly seasoned: 76.4% had used Python for at least five years. The results fall into three parts. How much people use type hints is flat. Which tools check those hints is changing fast. And AI coding tools now write the types and react to checker errors.
Steady use, unsettled tools
Remember
Using several checkers is now normal, and 42.7% of developers who do report that the checkers disagree.
AI agents that run checkers can satisfy them dishonestly, using `object` types or `# type: ignore` comments.
Dynamic libraries like Django and pandas still defeat static typing, and that's the top complaint at 65.1%.
Google's "sleep" cycle lets language models learn new facts without forgetting old ones
Google researchers give language models a wake/sleep cycle. While "asleep", a model copies what it learned in context into newly added weights, then trains on practice data it made itself. Reported results: little forgetting and better math scores.
Why it matters · Deployed models are frozen at their training cutoff. A working way to update their weights safely after deployment would change how AI systems are maintained and personalized.
Know this first
Context from the editor, not the article · 34 sec
1 · Frozen models, short memory
A large language model (LLM) learns during training and then its weights, the numbers that encode its knowledge, are frozen. After deployment it can only pick up new information through its context window, the text in the current prompt. When the session ends, that information is gone.
2 · Catastrophic forgetting
The obvious fix is to keep training the model on new data. But updating weights for a new task tends to overwrite what the model already knew, so old skills degrade badly. This is called catastrophic forgetting, and it is the main obstacle to continual learning.
3 · Mixture of Experts
A Mixture-of-Experts (MoE) model contains many sub-networks called experts. A small router network sends each token to only a few of them. This makes it possible to add new experts, and so new capacity, without touching the existing ones.
in-context learning (ICL)
A model using information or examples in its prompt without changing its weights. The effect lasts only for that session.
Image: Google Research
Google researchers have proposed a sleep framework for 1. The model alternates between a "wake" phase, where it serves users, and an offline "sleep" phase, where it updates its own weights. The goal is a model that keeps learning after deployment without forgetting what it already knew.
The problem
Once deployed, an LLM is frozen at its training cutoff. You can teach it new things in two ways, and both fall short:
Researchers at Google Research, Cornell and the University of Southern California (Ali Behrouz, Farnoosh Hashemi, Adel Javanmard and Vahab Mirrokni) have proposed a sleep framework for 1. Instead of training a model once and then freezing it, the model alternates between an active "wake" phase, where it serves users, and an offline "sleep" phase, where it updates its own weights. They report that this lets a model absorb new facts and languages without losing old skills, recall information across 10 million tokens, and score higher on competition math.
The problem: two bad options
A deployed LLM has a fixed knowledge cutoff. There are two standard ways to teach it something new, and each has a cost:
Remember
Knowledge goes into newly unlocked expert weights, not existing ones. That is how the design avoids overwriting old skills.
The model teaches itself: its with-context version acts as teacher for its without-context version.
No baseline numbers, base model or compute cost are given, so the size of the gains can't be judged.
Rewording the prompt swings AI judges of research novelty by 50 points
The Allen Institute for AI (Ai2) tested six AI models on judging whether research ideas are new. Small prompt changes flipped verdicts. Extra search and reasoning didn't help, and neither did specialized tools.
Why it matters · Using one model to grade another model's output is now routine, and this study measures how unstable that grading gets, especially on AI-generated work.
Know this first
Context from the editor, not the article · 36 sec
1 · LLM-as-judge
Teams often grade a model's output by asking another large language model (LLM) to rate it, because it is cheaper than human review. The judge's verdict depends on which model is used, the prompt wording, and any documents it is shown. Those choices are rarely checked for stability.
2 · AI research-idea generators
Labs are building systems that propose scientific hypotheses and experiments. To filter thousands of proposals, they need an automatic way to spot ideas that are genuinely new, not old work in new wording. A model that does this grading is what the authors call a "novelty judge".
3 · Pointwise vs pairwise judging
A judge can rate one item on its own (pointwise: "is this novel?"), or pick the better of two (pairwise: "which is more novel?"). In a pairwise test, guessing at random is right 50% of the time, so 50% is the chance level.
Each judge's accuracy on human-vs-AI idea pairs under the two prompt wordings; every model drops with the plainer prompt.
The Allen Institute for AI (1), a nonprofit research lab, has published a benchmark that tests how well 2 judge whether a research idea is new. Its main finding: the verdicts are unstable. Rewording one prompt moved a model's accuracy by more than 50 percentage points on the same pairs of ideas.
The problem
The Allen Institute for AI (1), a nonprofit research lab, has released Old Ideas, Novel Problems, a study of how reliably 2 can judge whether a research idea is novel. The release also includes a benchmark, data, code, and a pipeline for building new test sets. The headline finding: on the same pairs of ideas, changing a few words in the prompt moved one model's accuracy by more than 50 percentage points.
Remember
Test LLM judges on the kind of output they will actually grade. Results on human work didn't carry over to AI-generated ideas.
Instability can be measured without ground truth: count how often reasonable setups flip their verdicts on the same item.
More retrieval, reasoning, or pipeline engineering raised cost by 10× or more without improving accuracy over a plain prompt.
Proof search. A prover agent works alongside a reviewer agent that starts with fresh context. Verus reports which assertion failed but gives no counterexample, so the reviewer supplies the reasoning about why.
Merge control. A gatekeeper, a signed append-only ledger and a git hook guard what gets accepted. The checks reject any newly added assume, admit or external_body, escape hatches that tell Verus to trust a claim without proof. The prover can't merge its own work. This blocks 10, where an agent games the success check instead of doing the task.
Integrate once, add modules
Each system now integrates once by mapping its API onto five common operations: read, write, 3 (a call to another service), request entry, and inline execution (wrapping one computation inside a request). Rules are written as modules against those operations:
Enforcing modules can block an access. 4, Meta's system for controlling where labelled data may flow, is one.
Observing modules only record.
Adding a module to a system that is already integrated takes days. The check runs inside the client because the client still knows who is calling and why. Running it there also means a bad change breaks only the service running it, not a shared database.
A worked example
Messenger's backend writes message metadata, such as delivery times, to warehouse tables through 5, a logging library. The table itself carries a MESSAGING_TRAFFIC_METADATA label, so its many writers can't disagree about what's in it. Before each write, Policy Zones checks that the label is present and that the current context is an allowed use of the data. If either check fails, the write never leaves the process.
Speed and coverage
Rules are compiled at build time, and in-process caches answer most checks without a network call. An older design that fetched configuration remotely was thousands of times slower. For callers that skip the client and send raw RPCs, Meta's RPC layer checks a signed token from the client. Without a token, it applies a coarser, stricter check.
Safe changes
Changes to labels are simulated during code review. The system replays real data flows against both the old and new rules and flags any decision that would change. New modules roll out gradually behind a runtime percentage that can be lowered without a redeploy. Meta adopted these safeguards after early incidents, including an invalid config that crashed processes across the fleet.
AI agents
Internal agents decide at runtime what to access. A companion runtime, 6, tags each tool call with its agent session and passes that along to PrivacyLib. There, PrivacyLib can log the access or block it with the unchanged Policy Zones module, even for tools the agent's developers never expected it to use.
Every privacy requirement used to be built separately into the client of each storage or processing system. Two examples are 2 (data collected for one purpose is used only for that purpose) and data flow discovery (finding where data actually goes). Rolling out one requirement could take months. Each needed the same things: reach every system, ship in weeks, run on every access without adding noticeable delay, and change behaviour without taking the fleet down.
The scale makes this hard. More than a hundred client libraries are in scope, from key-value stores to AI features. Thousands of production services run some version of the library. Millions of data assets are accessed every day.
The design: integrate once, add modules
PrivacyLib separates "hook this system up" from "implement this rule." Each system integrates once by mapping its own API onto five common operations: read, write, 3 (calling another service), request entry (once, when a service starts handling a request) and inline execution (wrapping one computation, such as evaluating a feature, inside a larger request). Reads, writes and RPCs also have "after" hooks for modules that only record.
Rules are written as modules against those five operations. Enforcing modules can block an access; 4, which enforces purpose limitation, is one. Observing modules only record. Privacy Probes, for example, collects runtime signals used to discover data flows. Turning on another module in a system that is already integrated takes days.
The check runs in the client because the client still knows the caller's identity, endpoint and purpose, details that are often lost by the time a request reaches the datastore. Running it in the client also contains failures: a bad change breaks only the service running that build, not a shared database.
Worked example: messaging metadata
Messenger's backend processes metadata (for example, when messages were sent or delivered) to improve performance and detect abuse. Services write this metadata to data warehouse tables through 5, a client library that runs inside each service's process.
The label is attached to the destination table, not to each writer. Each table has a LoggerConfig. MetadataTraceLoggerConfig pulls in a trait that supplies the MESSAGING_TRAFFIC_METADATA label and attaches it with annotateWithTableLevelPolicy(). A table can have many writers, so if each declared the label separately, they could disagree or a new writer could forget it. Logger's code generator then turns the config into a PrivacyLib "artifact" for 6 (Meta's typed version of PHP). For C++ and Python, Logger publishes table identities and labels to a central catalog, and PrivacyLib generates artifacts from it.
Logger declares once, for all tables, that its write operation runs Policy Zones (enforcing) and Telemetry Logging (observing). In C++, a write builds a request with the table name, a hashed API identifier and the caller, then calls dispatch(). Policy Zones checks two conditions: the current processing context is an allowed use of messaging metadata, and the destination carries the MESSAGING_TRAFFIC_METADATA label. If either fails, the write is denied before the record leaves the process. Telemetry runs without affecting the decision.
Keeping it cheap
Rules are compiled at build time into their simplest form that can be evaluated. Per-request caches avoid repeating a check within one request, and per-host caches keep common configuration and results. An earlier design fetched configuration remotely, which alone was thousands of times slower than the in-process path. To keep telemetry from flooding downstream systems, each host uses a 7 (a compact structure for spotting repeats) to downsample high-volume repeated events at a fixed rate. Sampling rates also adjust as traffic changes, so rare events stay visible.
Callers that bypass the client
Some callers send raw RPCs. When a client-side check passes, PrivacyLib attaches a cryptographically signed token. 8, Meta's RPC layer, validates the token on supported traffic. Requests without a token get a coarser check based only on what's visible in the network payload, and that check applies the strictest reading, accepting false positives to avoid gaps. Paths outside Meta-managed clients and supported RPC routes are not covered and need their own integration.
Changing rules safely
A two-line edit that adds or removes a label can start blocking every writer to that table. During code review, the artifact is regenerated, and a simulation replays observed data flows against both the old and new versions, reporting any flow whose decision changes. Reviewers see the edit, the generated code and the simulation results together. Approved changes ship through each service's own deployment pipeline, which limits damage to services running that build. The cost is slower propagation, so owners track which services need the update and can use emergency deploys.
New modules start as rollingOut(), controlled at runtime under a key such as logger.input.write.zones. Meta raised Policy Zones on Logger from 0 to 100% in stages while watching denials, errors and latency. It could lower the percentage without rebuilding anything, then switched to enabled(). Meta learned this the hard way. Early on, an invalid config crashed processes across the fleet, and annotation changes that compiled cleanly still changed access decisions and broke products.
AI agents
Agents choose at runtime which tools to call, and one tool call may pass through several services before it reaches data. 9, a runtime built on PrivacyLib's design, tags each tool call with its agent session. That context travels downstream to the integrated system. There, the Agent Observability module records session and tool-call IDs, destination, client API and errors, so engineers can trace a tool call by session. Systems already integrated picked up the module without new work. Policy Zones is reused unchanged: where it's enabled, it can block an access even through a tool the agent's developer never anticipated, and the denial travels back to the agent.
What's left open
The post gives no latency figures for individual checks and doesn't say what share of access paths falls outside coverage. Meta names next steps: training data that arrives from many environments, evaluating agent behaviour as it happens, and accesses that are several agents removed from the person who asked.
Between 85.5% and 88.0% of respondents used type hints often or always in each of the three surveys. Choice of 3, the program that reads those hints and flags mismatches, was much less stable. Speed was the top reason for picking one (56.5%). Half of respondents (49.9%) now run two or more checkers, up from 46.0% last year. Of those using Pyrefly, Meta's own checker, 83.3% also used another. One team runs Pyrefly in 4 (the automated checks on every code change) and falls back to the slower 5 only on files where Pyrefly fails. There's a cost: 42.7% of multi-checker users reported that different checkers disagree on the same code.
AI joins the loop
AI tools wrote type hints for 42.5% of respondents. 24.4% said an AI coding agent runs their checker itself. Of those, 61.6% also had AI fix the errors, against 19.3% of everyone else. Respondents complained that agents choose overly broad types like object, which accepts anything, and scatter # type: ignore comments that silence the checker rather than fixing the problem. 29.8% weren't sure whether types even help AI-assisted coding, nearly four times the uncertainty for any other benefit. The authors say there's no hard evidence yet either way.
Libraries are still the bottleneck
The most common difficulty, at 65.1%, was missing type information in third-party libraries. Respondents named Django, SQLAlchemy, Pydantic, NumPy, pandas and Polars. These libraries create attributes and behavior at runtime in ways current type annotations can't describe, which 44.6% hit directly. Occasional users had a different main problem: 41.6% found the type system too complex or wordy, against 14.5% of frequent users. The most-wanted feature was a better way to write the types of functions passed as arguments, chosen by 45.7%.
Where people look for help
Between 2024 and 2026, use of Stack Overflow for typing help fell from 46.4% to 22.9%, while chats with AI language models rose from 26.0% to 41.7%. Use of the official typing documentation also rose. The authors suggest error messages link to short explanations with examples, which would help people and AI chat tools alike.
A caveat: respondents chose to take part, the survey was shared largely through checker projects' own channels, and Meta builds one of the checkers it asks about.
3 are optional annotations such as def total(items: list[float]) -> float. Python ignores them at runtime, and separate 4 read them to find mistakes before the code runs. Frequent hint use held between 85.5% and 88.0% across all three surveys (88.0% in 2024, 85.9% in 2025, 85.5% in 2026). A different group answered each year, but the rate barely moved.
Checker choice moved a lot more. 5, the original checker, was long the default. One 2024 respondent asked for "a faster Mypy" and blamed its slowness for splitting the ecosystem. By 2026 several newer open-source checkers were in use, including Microsoft's 6, Meta's Pyrefly and Astral's ty. Speed or performance was the top reason for choosing a checker, at 56.5%. Comparing the same list of checkers both years, 49.9% of respondents used two or more in 2026, up from 46.0%. The article includes a chart of each checker's share, but the text doesn't give the numbers.
Teams split checkers across tasks. Of 700 Mypy users, 297 also used its editor plugin, and 314 used a different checker's editor integration. Of 264 Pyrefly users, 220 (83.3%) also used another checker. One respondent described a setup in which Pyright runs locally because it understands their code's unusual typing patterns. In 7, the automated checks run on every code change, Pyrefly checks everything first and Pyright re-checks only the files where Pyrefly fails, to save time. In effect it's a fast first filter with a slower expert behind it.
The cost is disagreement. Checkers interpret parts of the typing rules differently, so the same code can pass one and fail another. A third (33.3%) of respondents to the difficulties question reported inconsistencies between checkers. Among multi-checker users the figure was 315 of 738, or 42.7%. The authors ask checker projects to document which of their differences are intentional.
AI in the type-checking loop
The share of respondents who said types make "AI-generated code more accurate/reliable" rose from 18.5% in 2025 to 38.4%. Among 1,517 respondents, AI tools wrote type hints for 42.5%, and 32.6% wrote types specifically to improve AI output. 61.0% used AI for at least one of four typing activities: writing hints, writing types to help AI, fixing type errors and explaining them.
A tighter loop is also appearing. For 24.4% (370 people), an AI coding agent ran the type checker itself. Of those, 61.6% also used AI to fix checker errors, against 19.3% of everyone else. So the agent writes code, runs the checker, reads the errors and edits again. Respondents reported shortcuts the agents take. One is annotating everything as object, a type so broad that almost any code passes and the check proves nothing. Another is adding # type: ignore comments, which tell the checker to skip a line. Both make the error go away without fixing the underlying problem.
Respondents were also unsure of the benefit. Asked how useful types are for AI-assisted coding, 29.8% of 1,551 said "I'm not sure." That's nearly four times the 7.7% uncertainty for runtime guarantees, the next most uncertain of six listed benefits. The authors say empirical evidence is still needed on which interactions between AI tools and checkers actually help. The Pyrefly team presented early work, "Type Checking in Agentic Workflows," at the 2026 Python Typing Summit.
Libraries remain the top problem
Missing type information in third-party libraries was the most common difficulty, at 65.1% of 1,486 respondents. A further 44.6% said the type system can't describe everything their code does. Shipping 8, which describe a library's types, doesn't settle it. Among 156 free-text answers, 22 mentioned dynamic constructs, decorators, metaprogramming or framework "magic". Ten mentioned arrays, dataframes or scientific types, and at least eight described annotations that were wrong, incomplete or too broad. Django, SQLAlchemy, Pydantic, NumPy, pandas and Polars came up repeatedly. These libraries tend to build behavior at runtime. For example, an object-relational mapper (a library that maps database tables to Python classes) creates query attributes from model definitions. A static checker can't easily see that. Meta's Pyrefly team works with Quansight, a consultancy in the scientific-Python world, on pandas-stubs and NumPy typing.
Who struggles with what
How often someone uses type hints shaped their complaints. Among rare or occasional users, 41.6% found the type system too complex or verbose, against 14.5% of frequent users. Frequent users were hit harder by library gaps (70.0% against 36.2%), probably because they type more of their code and run into gaps more often. Years of typing experience mattered little: complexity was reported by 18.2%, 16.0% and 21.0% across the 0–2, 3–6 and 7+ year groups. Newcomers to typing were often experienced Python developers. Of 396 people with 0–2 years of typing, 77.3% used hints often or always and 87.1% had at least three years of Python. The authors say beginner guidance should assume Python skill and show how to add types to an existing codebase.
The most-wanted feature was better Callable syntax, the notation for "a function that takes these arguments and returns this", chosen by 45.7%. Today it's written as Callable[[int, str], bool], and it can't easily express keyword arguments.
Editors and where help comes from
Readability or documentation was the top reason to use hints (93.6%). 84.8% rated editor support 4 or 5 out of 5. 82.9% ran a checker inside their editor, and VS Code led at 59.3%. Between 2024 and 2026, use of Stack Overflow for typing help fell from 46.4% to 22.9%, and chats with 9 rose from 26.0% to 41.7%. Typing documentation rose from 56.2% to 65.9% and checker-specific docs reached 60.5%, while general Python docs slipped from 66.7% to 62.2%. The authors want error messages to link to short explanations with examples, which would also give LLM chat tools better material to draw on.
Caveats
The sample is self-selected and was distributed partly through type-checker projects' own channels, so it likely overrepresents enthusiasts. Respondents differ year to year, many questions allowed multiple answers, and the number of people answering each question varies. Meta builds Pyrefly, one of the checkers being compared. The AI findings mostly raise questions rather than answer them. The raw data is published for anyone who wants to check the numbers.
Fine-tuning (further training on new data) causes 2: learning new things degrades old skills.
In-context learning (ICL), putting information in the prompt, is safe but temporary. The knowledge vanishes when the session ends.
The sleep framework takes in knowledge through context while awake, then moves it into weights during sleep. "Sleep" is an analogy; underneath it is an automated post-training loop.
Sleep stage 1: consolidation
The model uses a 3 design, where a router sends each token to a few of many sub-networks called experts. It is combined with 4, an earlier Google architecture that separates fast short-term memory from slow long-term memory. During sleep:
Expansion: small, pre-allocated experts are unlocked so new knowledge has fresh space and older weights stay untouched.
Knowledge seeding: the model with the information in its context acts as a teacher. The expanded model learns to reproduce its behavior without that context. It gets token-by-token feedback on its own outputs, plus a reward for completing teacher text closely, scored by meaning and by edit distance.
Pruning: the short-term memory is wiped for the next session.
As an analogy, think of copying a day's whiteboard notes into a new notebook chapter, then erasing the board.
Sleep stage 2: dreaming
The model generates synthetic practice data while its router deliberately activates experts it wouldn't normally use, which mixes unrelated knowledge. It keeps only the samples whose training updates look most useful, fine-tunes on them, and checks that downstream performance actually improved.
Reported results
Learning Manchu and Kalamang in sequence: "near-zero" forgetting, while ICL and standard fine-tuning forgot badly.
5, a benchmark that hides facts in huge texts: near-perfect recall up to 10M tokens, beating GPT-4 and Titans.
New facts on SQuAD (a question-answering dataset): 48.9% single-task and 46.2% under continued pre-training, ahead of fine-tuning and SEAL.
Competition math: 79.2% on AIME 24, 69.0% on AIME 25, 46.1% on HMMT 25, beating common reinforcement-learning methods.
Caveats
The post gives no baseline numbers and doesn't name the base model. It also says nothing about how much compute a sleep cycle costs or what happens once the reserved expert slots are used up. For production teams, a model whose weights change every night also raises open questions about testing and rollback.
Fine-tuning, meaning further training on new data, changes the weights. But training on task B tends to wreck performance on task A. This is 2.
In-context learning (ICL) means putting the new information into the prompt. This leaves the weights alone, but the knowledge lasts only as long as the context window. Close the session and it is gone.
The sleep framework aims to keep ICL's safety while getting the permanence of fine-tuning. Knowledge enters through context during the day and is moved into weights at night, in a way built to avoid overwriting what is already there. The authors stress that "sleep" and "dreaming" are only analogies to neuroscience. The process is an automated post-training loop with a fixed architecture and rules set by people.
Stage 1: memory consolidation
The authors compare this stage to non-REM slow-wave sleep, when the brain is thought to stabilize recent memories. It has three parts.
Parameter expansion. The model is built on a 3 design, where a router sends each token to a few of many sub-networks ("experts"). It is combined with 4, an earlier Google architecture that arranges memory as a hierarchy. Fast, high-frequency components hold short-term information. Slower, low-frequency blocks hold stable knowledge. During sleep, pre-allocated "low-rank" experts (small, cheap add-on weight matrices) are unlocked and attached to the slow blocks. New knowledge goes into this fresh capacity, so old parameters are not disturbed.
Knowledge seeding (upward distillation). Next, the short-term memories are moved into the new experts. The version of the model that has the information in context acts as a teacher. The expanded model, which must hold it in weights, is the student. Two training signals are used:
On-policy distillation (a form of Generalized Knowledge Distillation, GKD). The student generates its own text, and the teacher gives token-by-token feedback on it. Training on the student's own outputs, rather than only on teacher text, matches what the model will actually produce at inference time.
Learning to imitate (LTI), a reinforcement learning (RL) objective. The student is given the start of a teacher-written passage and rewarded for how closely its completion matches. Closeness is measured both by meaning and by 5, the number of character edits needed to turn one string into another.
Synaptic pruning. Once consolidation is done, the fast temporary memory is reset, which frees room for the next wake session.
A rough analogy (ours, not the article's): you take notes on a whiteboard all day. At night you copy what matters into a new chapter of a notebook without editing earlier chapters, then wipe the whiteboard.
Stage 2: dreaming
This stage is modeled on REM sleep, and it aims to improve the model rather than store memories:
Random expert selection. While the model generates synthetic training data, the router deliberately activates experts it would not normally pick. This mixes unrelated areas of knowledge.
Curated rehearsal. The resulting samples ("dreams") are filtered with gradient-based data selection. That means keeping the samples whose training updates look most likely to improve overall capability.
RL refinement. The model is fine-tuned on the best dreams and then checked to see whether downstream task performance actually improved.
The theory, briefly
The authors frame consolidation as a low-rank compression problem. The model does not copy every detail. It finds a small set of weight directions that preserve both its own behavior and the meaning that the reward values. Their account of dreaming is that random experts widen the range of gradient directions the model explores, and filtering keeps the informative ones. The result, they say, is a "better conditioned" optimization in which a few directions do not dominate the updates. On this view, dreaming is more than data augmentation.
Results
Continual translation into languages the model had never seen, Manchu and Kalamang: "near-zero" performance drop across several sequential learning stages. ICL, Cartridges (pre-trained compressed caches of a document's context), and plain supervised fine-tuning (SFT) all showed severe forgetting.
Long context on 6, a benchmark that hides facts in very long text and asks questions about them: "near-perfect scaling" up to 10M tokens, beating GPT-4 and Titans (an earlier memory architecture from the same lead author).
New factual knowledge on SQuAD (a reading-comprehension question-answering dataset): 48.9% in the single-task setting and 46.2% under continued pre-training. That beats the base model, SFT, and SEAL (Self-Adapting Language Models, which write their own fine-tuning data).
Math reasoning: 79.2% on AIME 24, 69.0% on AIME 25 and 46.1% on HMMT 25. These are high-school competition exams. The scores beat SFT, 7 (Group Relative Policy Optimization, a popular RL method for reasoning) and on-policy self-distillation.
What the post leaves open
The blog post gives no baseline numbers, so the size of each gain can't be checked. It does not name the base model behind the math scores or say how large it is. It gives no cost for a sleep cycle: compute, wall-clock time, or how often sleep must happen. Nor does it say what happens after many cycles, when the pre-allocated expert slots run out. GPT-4 is an old reference point for long-context work. "Near-zero" forgetting is not quantified. Dreaming relies on gradient-based filtering and downstream evaluation, which assumes you have a reliable task signal to check against. For engineers, the most practical question is also unanswered: how a model whose weights change nightly would be versioned, tested and rolled back in production.
Labs are building AI systems that generate research ideas in bulk. Someone has to filter out ideas that just repackage existing work, and that job usually goes to another LLM, which the authors call a "3." Teams build these judges with their own choice of model, prompt, 4, and literature search. They usually validate them on human-written papers, even though the judges end up grading AI-generated ideas.
Building ground truth
The team used peer reviews from 5 2026, a major machine-learning conference. Acceptance alone doesn't measure novelty, so they pulled out the passages where reviewers explicitly discussed originality. That gave them two pools:
154 high-novelty ideas: top-10% accepted papers where reviewers praised the novelty and no reviewer disputed it.
A second test set paired the 154 strong ideas with 154 ideas from a bare-bones LLM generator that had no search or tools. An expert checked 30 of these pairs and preferred the human idea in every one.
What they found
Six judges were tested, from GPT-5.1 to Claude Opus 4.6. Prompt wording mattered most. When told that exactly one idea in each pair was novel, GPT-5.4 picked the human idea 93.5% of the time. When simply asked which was novel, it scored 40.9%, worse than a coin flip, and it changed its answer on more than half the pairs. On the human-only pairs, the same change moved it by only about 7 points. Judges look steadier on human work than on AI output.
No prompt worked best for every model. When the team compared two idea generators against each other, a quarter to a third of verdicts flipped between prompt variants.
Extra effort didn't help. An agent with heavy reasoning and live search of 6, the preprint server, scored 0.78 7, a score that balances accuracy on novel and non-novel ideas. A simpler Claude Opus 4.6 setup scored 0.89, and the agent cost about 10× more per decision. A plain Opus 4.6 prompt with three-vote majority scored 0.854 for $2.59 in total. Two dedicated tools, Idea Novelty Checker and Sakana AI's AI Scientist, scored 0.642 ($30.66) and 0.772 ($82.05).
Caveats
Labeling the generated ideas as less novel is an assumption. The authors stress, though, that a judge flipping its verdict on the same pair shows instability whichever answer is right.
Why 3 exist
Ai2 builds tools for automating parts of science. DataVoyager explores datasets, AutoDiscovery generates and tests hypotheses, Theorizer synthesizes literature into candidate theories, and Asta ties these efforts together. Systems like these can produce research directions in bulk. The hard part is telling which ones add something new and which repackage existing work.
That check usually goes to another LLM, which the authors call a novelty judge. It rates an idea on its own (4) or picks the more novel of two (pairwise). Nobody has standardized how to build one. Each team picks a model, a prompt, an output format, a 5 (how much hidden "thinking" the model is allowed), and sometimes a retrieval system that fetches related papers. The authors also note that these judges are usually validated on human-written papers, while in practice they grade AI-generated ideas.
Building ground truth from peer reviews
To test a judge, you need ideas whose novelty is already known. The team mined reviews from 6 2026 (the International Conference on Learning Representations, a major machine-learning venue). They did not use acceptance as a stand-in for novelty, because a paper can be accepted for being solid without being new, and a rejected paper can be original but flawed. Instead they pulled out the passages where reviewers explicitly discussed originality.
High-novelty pool (154 ideas): accepted papers in the top 10% of their research area by rating, where reviewers praised the novelty and no reviewer disputed it.
Lower-novelty pool (145 ideas): rejected papers in the bottom 10%, where reviewers raised originality concerns and none praised novelty.
A human annotator checked 50 of the extracted signals and agreed on whether each was praise or criticism in 47. None of the three disagreements would have changed how a reviewer was counted.
These two pools form the Human-Only setting. The Human+Generated setting pairs the same 154 strong human ideas with 154 ideas from a deliberately simple generator, an LLM given only a research area and told to propose something novel, with no search, tools, or iteration. Labeling every generated idea as less novel is a weak assumption, and the authors say so. They backed it up two ways. An expert reviewed 30 pairs, chosen mostly from cases the best judge got wrong, preferred the human idea in all 30, and found none of the generated ideas novel. They also rewrote both kinds of idea into a common structure, to test whether judges were reacting to writing style rather than content.
The authors point out that many findings don't depend on the labels at all. If two reasonable setups give opposite verdicts on the same pair, the judge is unstable whichever answer is correct.
Prompt wording had the biggest effect
Six judges were tested: GPT-5.1, GPT-5.2, GPT-5.4, Claude Sonnet 4.5, Claude Opus 4.5, and Claude Opus 4.6. The team varied one factor at a time: prompt, reasoning budget, access to related papers, idea formatting, how many judgments were combined, and which model generated the AI ideas.
The prompt mattered most. On Human+Generated, one prompt told the judge that reviewers had found exactly one idea in each pair novel and asked which one. The other simply asked which idea was novel. GPT-5.4 dropped from 93.5% to 40.9%, which is below the 50% a coin flip would get, and it changed its verdict on more than half the pairs. Every model fell under the plainer prompt:
Judge
"Exactly one is novel"
Plain prompt
Claude Opus 4.6
100.0%
72.7%
Claude Opus 4.5
92.2%
58.4%
GPT-5.4
93.5%
40.9%
GPT-5.2
81.8%
76.0%
GPT-5.1
79.2%
56.5%
Claude Sonnet 4.5
60.4%
36.4%
On Human-Only, the same change moved GPT-5.4 by only about 7 points. So a judge can look stable on human research and fall apart on AI output. Human ideas were not immune, though: Claude Opus 4.6 moved 21 points on Human-Only.
No prompt was best across models. In pointwise judging, removing a warning not to count trivial or incremental work as novel helped some judges and hurt others.
The team also ran a common real-world comparison: ideas from two generators, Claude Opus 4.5 against Sonnet 4.5 and GPT-5.4 against GPT-5.1. Across prompt variants, roughly a quarter to a third of verdicts flipped on average. That number needs no ground truth, and it means a leaderboard of ideation systems can change depending on the judge's prompt.
More search, reasoning, and engineering didn't help
An agentic judge (GPT-5.6 Sol, as the article names it) got an extra-high reasoning budget and live, iterative search of 7, the preprint server. It scored 0.78 8. Macro-F1 averages the judge's accuracy-like F1 score on the "novel" class and the "not novel" class, so doing well on only one class doesn't help. The agentic judge trailed Claude Opus 4.6, which saw five pre-retrieved abstracts and scored 0.89, and it cost about 10× more per decision.
Dedicated tools did worse, all running on Claude Opus 4.6:
Plain prompt, low reasoning, majority vote over three calls: 0.854 macro-F1, $2.59 total
Idea Novelty Checker (retrieve and rerank related literature): 0.642, $30.66
The authors conclude that LLM novelty evaluation is unsolved. They recommend testing judges on the kind of ideas they will actually grade, reporting sensitivity across prompts and models, finding better ways to bring in prior literature, and building benchmarks that update as the field changes. The article does not explain why the "exactly one is novel" framing helps so much. One plausible reading is that it hands the judge the answer's structure, and real deployments can't do that. The Human+Generated labels also rest partly on the assumption that the simple generator produces less novel ideas, even though the expert check supports it.
