LLMs are making formal software verification feasible at a much larger scale
Claude formally proved security properties in the compiled code of 123 open-source libraries. Along the way, it found bugs that had eluded detection for years.
Topic
#formal-verification
7 篇笔记
形式化验证 LLM 生成的代码（FATTW 2026, Lucas Cordeiro）
FATTW 2026 会议演讲（与 ASE 2026 联合举办）：LLM 负责猜测（不变量、契约、harness），证明引擎负责裁决（ESBMC/k-induction/Vampire）。以 310,531 个 C 程序基准、Test-Comp/SV-COMP 竞赛成绩和 AWS/NVIDIA/vLLM 生产代码漏洞为证据，论证『模型建议 + 证明引擎确认』的设计原则。
The Harness Playbook
Model the agentic harness like a game engine and most of its hard problems — durable state, tools, configuration, the TUI, inference — collapse into ones other people already solved.
wal3: A Write-Ahead Log for Chroma, Build on Object Storage
wal3, Chroma's write-ahead log, combining a 30-year-old lock-free algorithm with S3's newest conditional writes feature.
Formally verified distributed locks for sandboxes
I’m wrapping up my internship at Modal, where I worked on our new, massively scalable sandbox architecture.
protocols for transactional usage of object storage
building correct applications w/o external coordination
Building and operating a pretty big storage system called S3
Three distinct perspectives on scale that come along with building and operating a storage system the size of S3.