Infer is an open-source static analyzer developed by Meta that detects null dereferences, memory leaks, resource leaks, and data races in Java, C, C++, and Objective-C code using separation logic. It is a SAST tool that performs inter-procedural analysis, also supporting Erlang and Hack.
What makes Infer different from pattern-matching analyzers is its foundation in separation logic — a mathematical framework for reasoning about programs that use shared mutable data structures. This lets it analyze each procedure independently and compose the results, scaling to codebases with millions of lines of code without sacrificing depth.
Meta deploys Infer internally across Facebook, Instagram, WhatsApp, and Messenger. Over 100,000 issues reported by Infer have been fixed by developers before code reached production. The project has 15,500+ GitHub stars and is licensed under MIT with no usage restrictions.
| Feature | Details |
|---|---|
| Developer | Meta (formerly Facebook) |
| License | MIT (fully open-source, no restrictions) |
| Languages | Java, C, C++, Objective-C, Erlang, Hack |
| Analysis type | Inter-procedural via separation logic and bi-abduction |
| Core engine | Pulse (null deref, memory/resource leaks, taint, use-after-free) |
| Concurrency | RacerD (thread safety and data race detection) |
| CI mode | Differential analysis — reports only new issues per diff |
| Build systems | Gradle, Maven, javac, clang, gcc, make, Buck, Xcode |
| Output formats | JSON, SARIF |
| GitHub stars | 15,500+ |
Overview
Infer works in two phases: capture and analyze. During capture, Infer intercepts your build system’s compilation commands and translates source files into its internal intermediate representation. During analysis, it examines each function and method individually using its Pulse engine.
The key innovation is bi-abduction — a logical inference technique that automatically discovers what each function expects (pre-conditions) and guarantees (post-conditions). This means Infer doesn’t need developers to write annotations or specifications. It figures out the contracts from the code itself, then checks whether callers respect those contracts.
This compositional approach is what makes Infer scale. Instead of analyzing the entire program at once, it breaks the analysis into independent pieces that can be cached and reused. When a developer submits a code change, only the modified files and their dependents need re-analysis.
Key Features
Pulse engine
Pulse is Infer’s default analysis engine, replacing the earlier Biabduction checker. It detects these issue types:
| Issue Type | Description |
|---|---|
| Null dereferences | Accessing a null pointer in Java, C, C++, or Objective-C |
| Memory leaks | Allocated memory that is never freed (C/C++/Objective-C) |
| Resource leaks | Unclosed file handles, database connections, streams |
| Use-after-free | Accessing memory after it has been deallocated |
| Uninitialized values | Reading variables before they are assigned |
| Taint flows | User-configurable tracking of tainted data from sources to sinks |
| Unnecessary copies | C++ objects copied when a reference would suffice |
Pulse’s taint tracking is configurable — you can define your own sources, sinks, and sanitizers to detect application-specific data flow vulnerabilities.
RacerD: concurrency analysis
RacerD is Infer’s dedicated checker for thread safety and data race detection. It identifies situations where multiple threads access shared data without proper synchronization.
For Java, RacerD detects:
- Unprotected field accesses across threads
- Inconsistent lock usage
- Race conditions on shared mutable state
For C++, RacerD extends these capabilities to detect inconsistent lock usage patterns in concurrent code.
Race conditions are notoriously difficult to catch through testing because they depend on thread scheduling, which is non-deterministic. Infer’s RacerD is one of the few free tools that detects data races through static analysis rather than runtime testing.
The table above, from Meta’s engineering blog, shows why inter-procedural analysis matters. For thread safety violations and memory allocation bugs, the vast majority of issues span multiple files — tools that only analyze within a single function or file would miss them entirely.
Build system integration
Infer hooks into your existing build system rather than requiring a separate build configuration:
| Build System | Capture Command |
|---|---|
| Gradle | infer run -- ./gradlew build |
| Maven | infer run -- mvn compile |
| javac | infer run -- javac *.java |
| clang/gcc | infer run -- clang -c file.c |
| make | infer run -- make |
| Xcode | infer run -- xcodebuild |
| Buck | infer run -- buck build //target |
The infer run command handles both capture and analysis in a single step. For more control, you can run infer capture and infer analyze separately.
Differential analysis for CI
Infer’s differential analysis mode is designed specifically for continuous integration. Rather than reporting every issue in the entire codebase, it compares results against a previous analysis and reports only regressions — new issues introduced by the current code change.
# Analyze the base branch
git checkout main
infer run -- ./gradlew build
# Switch to the feature branch and run differential analysis
git checkout feature-branch
infer run --reactive -- ./gradlew build
This workflow mirrors how Infer is deployed at Meta: every diff submitted for code review triggers an Infer run that reports only the issues introduced by that diff. Developers get focused, actionable feedback instead of a wall of pre-existing findings.
Separation logic foundation
Infer’s theoretical foundation sets it apart from pattern-matching tools. Separation logic provides a way to reason about heap-allocated data structures by partitioning memory into independent regions.
The separating conjunction (*) lets Infer prove that modifying one part of memory doesn’t affect another part. This is what enables compositional analysis — each function is analyzed independently, and the results compose correctly because separation logic guarantees non-interference between heap regions.
Use Cases
Mobile app development — Infer was built for Meta’s mobile apps. If you develop Android (Java) or iOS (Objective-C) applications, Infer catches the memory and null safety issues that are most common in mobile codebases.
Systems programming — For C and C++ projects, Infer’s memory leak and use-after-free detection addresses the most dangerous categories of bugs. Memory safety issues account for the majority of critical vulnerabilities in systems code.
Large-scale CI/CD — The differential analysis mode makes Infer practical for large teams. It doesn’t require fixing all existing issues before adoption — it catches new issues from day one.
Concurrency-heavy applications — RacerD fills a gap that most SAST tools leave open. If your application uses multithreading, Infer can find data races that are nearly impossible to reproduce through testing.
Strengths & Limitations
Strengths:
- Inter-procedural analysis that scales to massive codebases via compositional reasoning
- Differential analysis mode works well in CI — reports only new issues per diff
- RacerD catches concurrency bugs that most SAST tools miss entirely
- No annotations required — bi-abduction infers function contracts automatically
- Proven at Meta scale (millions of LOC across multiple apps)
- MIT license with no restrictions
Limitations:
- Limited language support compared to tools like Semgrep or CodeQL — no JavaScript, Python, Go, or Ruby
- Focused on memory safety and concurrency — not a general security vulnerability scanner (no SQL injection, XSS, etc. out of the box)
- Requires compilation — cannot analyze code without a working build (unlike pattern-matching tools)
- Setup complexity is higher than simpler SAST tools; depends on OCaml toolchain
- Documentation and community resources are thinner than more widely adopted tools
- No web dashboard or centralized management — CLI-only workflow
Getting Started
brew install infer. On Linux, download the binary release from the GitHub releases page. Building from source requires the OCaml toolchain via opam.infer run -- <build-command>. For a Java project with Gradle: infer run -- ./gradlew build. Infer captures the compilation and then analyzes the result.infer-out/report.json. Each finding includes the bug type, file, line number, and a trace showing how the issue was reached.infer run on the base branch first, then infer run --reactive on the feature branch. Only new issues appear in the report.How Infer compares to other SAST tools
The main difference between Infer and other SAST tools is the analysis approach. CodeQL treats code as a queryable database for finding security vulnerability patterns. Semgrep matches syntactic patterns in source code. Infer uses formal verification techniques to prove the absence (or presence) of specific bug classes, reasoning about program behavior across function boundaries.
The tradeoff is coverage versus depth. Semgrep and CodeQL support more languages and broader vulnerability categories. Infer goes deeper on fewer bug classes — memory safety, null safety, and concurrency — in fewer languages. Infer is better for catching null dereferences, memory leaks, and data races; CodeQL is better for catching SQL injection, XSS, and authentication flaws. For teams working primarily in Java, C/C++, or Objective-C, Infer addresses bug categories that pattern-matching tools struggle with.
For PHP projects, consider PHPStan or Psalm instead. For Python, Bandit is a more appropriate choice.
