Meta has shipped over 100,000 bug fixes that were caught by a static analyzer before the code ever reached a user. The tool is called Infer, it is open source, and it does not run your code. It reads it, builds a mathematical model of what the code could do, and proves that certain bad things cannot happen. Or it finds a path where they can.

The technique is abstract interpretation. It sounds academic because it is. Patrick Cousot and Radhia Cousot invented it in the 1970s as a way to reason about programs without executing them. Meta’s team, led by Peter O’Hearn, took the theory and made it fast enough to analyze millions of lines of mobile and server code in minutes. The result is a tool that finds null pointer dereferences, memory leaks, resource leaks, and race conditions at diff time.

The problem: dynamic testing cannot cover what you did not think to run

A unit test checks one path through your code. An integration test checks a few more. But a function with five conditionals and two loops has hundreds of paths, and most of them are never exercised in test suites.

Dynamic testing, running the code, can only find bugs on paths you actually execute. Static analysis finds bugs on paths you never thought of. It is the difference between checking your house for intruders by walking the rooms with a flashlight, and checking by proving that all doors and windows are locked.

The challenge is that proving things about real programs is hard. Real programs have loops, recursion, heap allocation, and concurrency. You cannot enumerate every state. Abstract interpretation solves this by approximating.

What abstract interpretation actually means

Abstract interpretation works by running your program on abstract values instead of concrete ones.

In a normal execution, a variable x might hold the integer 42. In an abstract interpretation, x might hold the abstract value “positive.” The analysis does not know that x is 42. It knows that x is greater than zero. That is enough to prove that x / y will not divide by zero if y is also positive. It is not enough to prove that x == 42. Abstract interpretation trades precision for computability.

The set of abstract values is called an abstract domain. The simplest domain is the sign domain: each variable is either negative, zero, positive, or unknown. More complex domains track ranges, pointers, or whether a memory location has been freed. The analysis iterates over the program, applying abstract versions of each operation, until the abstract state stops changing. At that point, it has found a fixed point, an approximation of every possible concrete state at each program point.

Loops are the hard part. A loop might run zero times, once, or a billion times. The analyzer cannot unroll it a billion times. Instead, it applies a widening operator that jumps to an over-approximation. If a variable increments by one each iteration, the analyzer might widen its abstract value from “positive” to “non-negative” and stop there. It loses the exact bound, but it keeps the property that matters for the proof.

How Infer uses bi-abduction to analyze procedures modularly

Traditional abstract interpretation analyzes an entire program as a whole. That does not scale to a mobile app with a million lines of code. Infer solves this with a technique called bi-abduction.

Bi-abduction lets Infer analyze one function at a time. When Infer analyzes a function, it discovers two things: the preconditions that must hold for the function to be safe, and the postconditions that the function guarantees. These are inferred automatically, not written by the programmer.

Here is a concrete example. Suppose Infer sees this C function:

void greet(struct Person* p) {
    printf("Hello, %s\n", p->name);
}

Infer infers that greet requires p to be non-null. That is the precondition. It also infers that greet does not free p or modify any visible state. That is the postcondition. When another function calls greet, Infer checks the caller against the inferred precondition. If the caller might pass null, Infer reports a bug.

The bi-abduction engine works by symbolic execution over separation logic. Separation logic lets Infer reason about heap ownership: which function owns which memory, and whether that memory has been freed. This is what makes Infer good at finding null dereferences and memory leaks in C, C++, Objective-C, and Java.

What Infer catches and what it misses

Infer is not a general-purpose linter. It targets specific bug classes that are expensive to find dynamically and dangerous in production.

Null pointer dereferences. Infer tracks whether each pointer is definitely null, definitely non-null, or maybe null. A dereference of a maybe-null pointer triggers a report. In Java and Objective-C, this catches the most common crash type.

Memory leaks. Infer uses separation logic to track heap ownership. If a function allocates memory and does not free it or return it to a caller, Infer reports a leak. This is particularly valuable in C and C++ codebases where leaks accumulate over weeks of uptime.

Resource leaks. File descriptors, sockets, and locks are tracked similarly. If a function opens a file and returns without closing it on every path, Infer reports the leak.

Race conditions. Infer’s RacerD module analyzes Java concurrency. It tracks which threads access which fields and whether those accesses are protected by locks. Two threads accessing the same field without synchronization is a race.

Infer does not catch everything. It misses bugs that require reasoning about numerical precision, string contents, or complex aliasing patterns. It is also unsound by design: it may miss bugs in order to keep false positives low. A static analyzer that cries wolf on every diff gets disabled. Meta’s internal deployment kept Infer’s false positive rate under 10%, which is why developers actually act on its reports.

Running Infer on your own code

Infer is open source and supports C, C++, Objective-C, Java, and (experimentally) Rust and Swift. The easiest way to try it is on a Java or C project.

Install Infer via Homebrew or Docker:

# macOS
brew install infer

# Or via Docker
docker run --rm -v $(pwd):/repo infer/infer infer run -- make -C /repo

For a Java project using Maven:

infer run -- mvn compile

For a C project using Make:

infer run -- make

Infer compiles your code, builds a control-flow graph, and runs the analysis. The output is a set of bug reports with file names, line numbers, and the inferred precondition that was violated.

Here is a minimal C example that Infer will flag:

// leak.c
#include <stdlib.h>

int* allocate_but_leak(void) {
    int* p = malloc(sizeof(int));
    *p = 42;
    // forgot to return p or free it
    return NULL;
}

Running infer run -- cc leak.c produces:

leak.c:5: error: MEMORY_LEAK
  memory dynamically allocated by call to `malloc()` at line 5 is not reachable after line 7

Infer also catches the null dereference in this example:

// null.c
#include <stdio.h>

void print_length(const char* s) {
    if (s != NULL) {
        printf("%zu\n", strlen(s));
    }
}

void unsafe_call(void) {
    print_length(NULL);  // Infer reports this
}

Wait, actually Infer will not report the above. The print_length function safely handles a null argument. Infer only reports when a dereference happens on a possibly-null pointer without a check. Here is one that will trigger:

// null_bad.c
#include <stdio.h>

void unsafe_print(const char* s) {
    // No null check before dereference
    printf("first char: %c\n", s[0]);
}

void call_unsafe(void) {
    unsafe_print(NULL);  // Infer reports this
}

Infer traces the path from call_unsafe through unsafe_print and reports that s is null when s[0] is evaluated.

The trade-off: speed versus precision

Infer’s modular design makes it fast enough to run on every pull request at Meta. But modularity introduces approximation. When Infer analyzes a function, it does not know the exact calling context. It infers preconditions that are conservative, meaning they may be stronger than necessary. A stronger precondition means fewer bugs reported at the call site, but also fewer false positives.

This is the central tension in static analysis. A sound analyzer reports every bug, but drowns you in false positives. An unsound analyzer like Infer keeps developers happy by only reporting bugs it is confident about. The bugs it misses are the cost of adoption.

Infer’s bi-abduction engine also struggles with global state and complex callbacks. If your Java code passes an anonymous inner class to an executor, Infer may lose track of which thread runs which method. RacerD handles common patterns but misses subtle races involving condition variables or atomic fields.

When to adopt static analysis and when to skip it

You should consider Infer if you ship native code, mobile apps, or server code in C-family or Java languages. The bugs it finds, null dereferences, leaks, races, are exactly the ones that cause production crashes and security vulnerabilities.

You should not expect Infer to replace your test suite. Static analysis and dynamic testing are complementary. Tests verify that your code does what you intend on the inputs you chose. Static analysis verifies that your code does not do what you forbid on any input.

If your codebase is in Python, Ruby, or JavaScript, Infer is not the right tool. These languages lack the static type information that Infer uses to build its abstract model. For dynamic languages, type checkers like mypy or pyright catch a different class of errors.

The takeaway

Meta’s 100,000 bug fixes are not a marketing number. They are the output of a tool that runs on every diff, analyzes code without executing it, and reports bugs that no test would have caught. The underlying technique, abstract interpretation, is decades old. The engineering achievement is making it fast and precise enough that developers do not turn it off.

You do not need Meta’s infrastructure to benefit. Install Infer, point it at your build system, and run it on a module that scares you. The memory management module, the concurrency layer, the C interop boundary. Fix the leaks and null dereferences it finds. Then add it to CI and keep the bug count from growing.

Abstract interpretation is not magic. It is math applied to code, with all the approximations and trade-offs that entails. But it is math that finds real bugs in real codebases, and that makes it worth knowing.