FM-Agent:
Autonomously Reasoning About
Correctness of Large-Scale System Code
FM-Agent enables fully automated reasoning about large-scale system code, such as Claude's C Compiler with up to 143K LoC.
-
Lines Analyzed
-
Users
-
Bugs Found
Highlights
Top-Down Specification
FM-Agent autonomously understands developers' intent and generates correctness specifications for functions from top to bottom.
Natural-Language Hoare Logic
FM-Agent generalizes Hoare logic inference rules to reason about code against natural-language specifications without human effort.
Automated Bug Diagnosis
FM-Agent autonomously detects the root causes and locations of bugs from reasoning process, providing rich context to understand and fix them.
