Tag
ASMC 是一个将 Ghidra 的 p-code 汇编语义提升到 CBMC GOTO IR 的开源工具，用于对 x86-64 汇编进行有界模型检查，支持汇编验证、翻译验证与 C 级规格断言等多种用途。
Hillel Wayne explains what properties TLA+ can verify (safety invariants, action properties, liveness) and which limitations remain, tempering the hype around formal methods after Boris Cherny mentioned Claude's Opus finding race conditions with TLA+.
The article discusses the possibility of expressing reachability properties in TLA⁺, referencing Leslie Lamport's work and the limitations of the TLC model checker.
This survey paper reviews 38 studies on safe LLM agents, highlighting key challenges such as specification translation bottlenecks, incomplete safety guarantees from enforcement methods like runtime monitoring, and the verifier tax that impedes safe task completion.
TLA+ is a model checking tool that explores all state interleavings to find bugs in distributed systems; it helped improve safety in Depot Registry's garbage collector by identifying a missed bug through formal verification.
Specula is an agentic system that automatically derives TLA+ specifications from code, runs model checking to find concurrency bugs, and reproduces them via integration tests. It found 249 bugs across 48 open-source distributed and concurrent systems, demonstrating a significant scaling of formal verification.
Kani is an open-source model checker for Rust that uses bounded model checking on the MIR to verify safety properties and functional correctness, with a specification language for unbounded verification. The paper reports case studies on industrial Rust projects where Kani uncovered six previously unknown bugs and operates at scale in production CI.
An introduction to using TLA+ with LLMs like Claude to write formal specifications, showing how LLMs can help with syntax while focusing on correctness.
This paper presents a novel framework for synthesizing finite-state controllers for Partially Observable Markov Decision Processes (POMDPs) by integrating sampling, automata learning, and model-checking. The approach provides formal guarantees for threshold-safety problems that elude existing formal synthesis tools.
Researchers from the Specula team created SysMoBench, a benchmark evaluating whether LLMs can faithfully model real-world computing systems in TLA+ or merely recite textbook specifications. The benchmark tests 11 systems across four phases and reveals systematic gaps in current LLMs' ability to accurately model system implementations versus reference papers.
TLA+ semantics guarantee nonordered updates, but the TLC model checker breaks these guarantees by requiring ordered assignments and adding effectful operators like PrintT, causing confusion for beginners.
Explains the concept of possibility properties in formal methods, complementing safety and liveness, and discusses their use in specification and model checking.