# Claude formal proofs, ThinkingBox rewards, Kling 4.0, TTR-Compressor > Anthropic proves security properties in 123 libraries, Microsoft turns database checks into RL rewards, Luma adds Kling 4.0, a new sequence compressor. Published 23 Oct 2026. Coverage: 22 Oct 2026 to 23 Oct 2026. By Ali Asif. ## Items 1. **LLMs are making formal software verification feasible at a much larger scale** (Anthropic, Frontier): With Theorem, Claude proved security properties at the RISC-V assembly level across 123 open-source libraries and found bugs that years of testing had missed. [Primary source](https://www.anthropic.com/research/formal-verification) 2. **Turning Database Grading into RL Rewards: Post-Training Agents with ThinkingBox** (Microsoft, Agents and coding): Executable database checks used as GRPO rewards lifted Qwen3.8-27B pass@1 from 51.70% to 60.78% and fully repeatable tasks from 38 to 107 of 507. [Primary source](https://huggingface.co/blog/microsoft/thinkingbox-training) 3. **Kling 4.0 in Luma: Fast Action and Big Camera Moves** (Luma, Image, video, world): Kling 4.0 is now selectable on Luma boards for tracking shots, orbits and push-ins, in text-to-video and image-to-video, across four aspect ratios. [Primary source](https://lumalabs.ai/news/kling-4-in-luma-ai-video) 4. **Rethinking Sequence Compression with Test-time Regression** (Academic, Science): TTR-Compressor treats input tokens as a regression problem and uses the fitted coefficients as the compressed representation, aimed at sparse attention and vision-language projectors. [Primary source](https://huggingface.co/papers/2610.31574) Today's log is led by a proof story from Anthropic, followed by a training recipe, a video model landing in a creative tool, and a paper on compressing sequences. I read the primary pages and ran none of the code, so the figures are what each publisher reports. ## Claude writes proofs for 123 libraries Anthropic, working with Theorem, asked Claude to prove security properties across 123 open-source libraries. The proofs sit at the assembly level, on RISC-V binaries with a median length of 18,000 instructions. Claude showed that some executable artifacts always exit normally, with no memory-safety errors or failing assertions, for every input under 64 MB and every modeled Linux response and memory layout. The part I find clever is where the specification comes from. Most programs have no formal spec, so the team encodes the rule "this test suite always passes" using a general model of executing a RISC-V binary on Linux, which turns an existing test suite into something provable. Anthropic says Claude also found bugs that had survived years of use and trillions of test runs while writing the proofs. The limits are stated plainly. The proofs assume a single-threaded static binary with a fixed memory budget on a RISC-V CPU running Linux, and the post says "formally verified" does not mean bug-free. Anthropic is publishing a subset of the proofs along with the RISC-V and OS semantics, and Theorem is offering to run the same pipeline for other open-source projects and is publishing a Claude skill for developers who want to try it on their own code. ## ThinkingBox turns database state into rewards Microsoft and Hugging Face followed their ThinkingBox benchmark post with a training one. Each of the 507 benchmark tasks gives an agent a real backend and tools, then checks what changed in the database. Since a check can return 1 or 0 from the final state, the team used it as a reward on training tasks outside the benchmark. The selection step is the interesting bit. Tasks that are already solved or hopeless teach nothing, so they estimated each task's success probability once with the base policy and kept a fixed pool. After 50 GRPO steps on Qwen3.8-27B, pass@1 rose from 51.70% to 60.78%, and tasks passed on all twenty attempts rose from 38 to 107. The cost is that pass@20 slipped from 453 tasks to 446, so repeatable success improved while at-least-once coverage dipped slightly. ## Kling 4.0 arrives in Luma Luma added Kling 4.0 to its boards for shots where action, camera and environment all have to hold together. The listed strengths are fast action, directed camera work such as tracking shots, orbits, push-ins and pans, characters closer to the brief, and on-screen text that stays put while the camera moves. It supports text-to-video and image-to-video in 16:9, 9:16, 1:1 and 21:9. Luma frames it as a lens you pick for the hard shots, keeping other tools for the rest. The page gives no benchmarks, so treat the claims as the vendor's description. ## Compression as regression A new paper proposes TTR-Compressor, which defines a regression problem from the input tokens and uses the fitted coefficients as the compressed representation. The regression is learned end to end by backpropagation. The authors report gains as a compressor for block-wise sparse attention in efficient language models and as a projector in multimodal models, and they point to video and audio compression as next steps. ## What I'd watch next Whether Theorem's offer to verify other projects produces proofs for libraries people actually ship, whether the ThinkingBox pool recipe holds on tasks from other domains, and whether the TTR results hold up in independent runs. ## My take The formal verification work is the one I would read in full, because proofs that scale change what a security claim can mean for a library I depend on. The ThinkingBox result matters to me for a plainer reason: a checkable outcome is a better reward than a judge's opinion. I read each primary page and ran none of it, so every number is the publisher's own. ## Sources - https://www.anthropic.com/research/formal-verification - https://huggingface.co/blog/microsoft/thinkingbox-training - https://lumalabs.ai/news/kling-4-in-luma-ai-video - https://huggingface.co/papers/2610.31574 Canonical: https://heyaliasif.com/ai/2026-10-23-claude-formal-verification-thinkingbox-kling-4-ttr