Polyglot program analysis platform built on verified foundations.

go-brrr translates source code from multiple languages into a universal intermediate representation, then applies formally verified static analyses to find bugs, security vulnerabilities, and correctness violations that single-language tools cannot detect. The analysis framework, the translation correctness proofs, and the abstract interpretation foundations are written in FX and machine-checked.

The core thesis is that programming languages are parameterized instantiations of a universal computational substrate. Languages differ in their configuration — memory model, type discipline, null handling, effect tracking, concurrency model — not in their essential semantics. This makes it possible to specify analyses once at the IR level and apply them uniformly to any source language.

Source languages            brrr-ir                    Analysis
(Python, Rust, Go,    →     (universal IR,        →    (IFDS, abstract
 TS, C/C++, Java)           51 expression forms,       interpretation,
                            graded types)              CPG, taint, symbolic
                                                       execution)

brrr-ir is the universal intermediate representation. It carries graded type information — usage modes, effect rows, security labels, session types, ownership — derived from the FX type system's fifteen dimensions. Source languages that lack these dimensions (most of them) get grade information inferred during translation.

brrr-translate maps each source language to brrr-ir through a verified translation functor. Type preservation and semantic preservation are proved via simulation relations in FX, following the CompCert approach to compiler correctness. Properties that cannot be precisely translated are conservatively over-approximated.

brrr-machine is the analysis engine. It provides:

• A concrete interpreter for differential testing against source language semantics.
• A symbolic execution engine parameterized by abstract domains via Galois connections.
• An IFDS framework for context-sensitive interprocedural dataflow analysis.
• Taint tracking across function, module, and language boundaries.
• A unified code property graph (CPG) combining AST, CFG, and PDG for graph-reachability queries.

brrr-cli is the practical tool. It parses source code via tree-sitter, builds call graphs, computes code metrics, runs security scans, and supports semantic search over codebases. Output formats include JSON, Mermaid diagrams, and SARIF for CI integration.

FX is the language go-brrr is written in. The type theory, effect system, ownership model, security labels, session types, separation logic, and algebraic structure library that go-brrr depends on are native FX features. The analysis foundations — Galois connections, lattice theory, IFDS correctness proofs — are FX standard library modules.

The brrr-ir type system is a projection of FX's graded type system onto a language-neutral IR. For FX source code, the translation to brrr-ir is nearly identity. For other languages, the translation infers grade information the source language does not track:

Python source:                  brrr-ir (with inferred grades):

def process(data, key):         fn process(
    result = encrypt(data, key)   data :_(taint={UserInput}) bytes,
    log(result)                   key :_(security=secret) crypto_key,
    return result                 ) : bytes with IO
                                    // WARNING: secret data flowing to log()

The analysis then applies FX's grade checker to find violations — taint flows, information leaks, protocol mismatches, ownership errors — that the source language's own type system cannot express.

At the single-language level: SQL injection, command injection, XSS, path traversal, hardcoded secrets, weak cryptography, unsafe deserialization, ReDoS, use-after-free, null dereferences, resource leaks, dead code, circular dependencies, god classes.

At the cross-language level: type mismatches at FFI boundaries, ownership violations across language transitions, taint propagation through serialization, protocol violations in RPC, effect leakage through foreign calls.

At the semantic level: noninterference violations (secret data reaching public outputs), session type protocol deviations, refinement type violations inferred from runtime behavior, termination concerns from recursive call patterns.

Static analysis tools for individual languages are limited to what those languages can express. Python has no ownership model, so no Python tool checks for resource leaks through ownership. Go has channels but no session types, so no Go tool verifies protocol compliance. C has no taint tracking, so cross-boundary data flow between C and its FFI callers goes unchecked.

For each language, go-brrr encodes the relevant language standard — runtime semantics, memory model, type coercion rules, concurrency primitives — as explicit axioms in brrr-lang. A translated JavaScript program carries ECMAScript's coercion and prototype chain rules. A translated Go program carries goroutine scheduling and channel semantics. The encoding makes implicit language behavior available for analysis in a type system expressive enough to reason about it.

Additional structure extraction available for Ruby, PHP, Kotlin, Swift, C#, Scala, Lua, and Elixir via tree-sitter grammars.

The analysis framework synthesizes results from abstract interpretation (Cousot & Cousot 1977), interprocedural dataflow via graph reachability (Reps, Horwitz & Sagiv 1995), code property graphs (Yamaguchi et al. 2014), separation logic (Reynolds 2002), algebraic effects (Plotkin & Power 2003), session types (Honda 1993), information flow control (Denning 1976, Volpano & Smith 1996), and graded type theory (Atkey 2018). Proofs are mechanized in FX.

The CLI and IR library are Rust. The analysis engine and translation proofs are FX.

# Rust components
cargo build --release
cargo install --path brrr-cli

# FX components
cd brrr-lang && make verify
cd brrr-machine/src && make verify

Prerequisites: Rust nightly, FX compiler, Z3 4.13+.

brrr tree ./src --ext .rs              # file tree
brrr structure . --lang python         # functions, classes, methods
brrr calls ./src                       # cross-file call graph
brrr cfg src/main.rs main              # control flow graph
brrr security scan ./src               # vulnerability scan
brrr metrics report ./src              # code quality metrics
brrr semantic search "auth handler" .  # natural language search

Apache 2.0.