Open source · TypeScript · Next.js
Give Brody a folder, a ZIP, or a GitHub repository. It parses with real parsers, builds a symbol and dependency graph, reviews with deterministic analyzers and optional AI, and proves what it can with Lean 4. A claim that does not cite lines that exist is dropped. The code it analyzes is never executed.
An AI finding survives only if its file exists, the quoted evidence is in that file, and a suggested patch applies to the real source. Otherwise it is dropped or marked Needs verification.
A theorem counts only when Lean accepts it with nothing beyond its standard axioms. A separate audit checks that the model matches the source, and replays every counterexample on the original code.
It reasons over symbols, the call graph, routes, models, and retrieved excerpts. Repository text is wrapped as untrusted content, and detected secrets are redacted before a request is sent.
Features
Every view below is a real Brody screen, generated from the same stored analysis. There is no separate “quality score.”
Each finding has an ID, severity, confidence, the exact lines, what happens, why it matters, the business impact, a fix, and, where possible, a patch that has been applied to the real file to prove it fits. Filter by severity, category, source, status, confidence, and functional area.
An AI fix prompt condenses the open issues, with their fixes, validated patches, and evidence, into one Markdown prompt for Claude Code, Cursor, Copilot, or ChatGPT.
The functions that most need it — open AI claims first, then high complexity, dense arithmetic, and names that decide amounts, limits, state, or access — are modelled in Lean 4 and checked by Lean’s kernel.
Brody can prove a guarantee, prove a concrete counterexample (the input that breaks the code, ready to become a regression test), confirm an AI claim, or remove a false positive by proving the claimed failure cannot happen. Unchanged functions reuse their proofs.
The code map goes from functional areas to files to a single symbol, marks risk, exports Mermaid, and answers “if I change this, what could I affect?” System explanation has four zoom levels — the whole system, groups of files, one file, and a symbol — and every statement links to its source.
A gauge on every project page shows the tokens and estimated cost of the latest analysis, updating while it runs, with the model that answered, a per-step breakdown, and the prices used. Local or unpriced models show tokens and “cost n/a” rather than a guess.
Without an API key, every deterministic stage still runs. AI stages say plainly that they were skipped.
Security and privacy
A security assessment covers overall risk and its reasons, the attack surface, OWASP Top 10 (2021) coverage, CWE-mapped findings, the controls found in the code, and a Now / Next / Later plan. A privacy review inventories personal-data fields, subjects, likely third parties, and regulatory indicators. Both are built from the same verified findings as the code review.
Ask and search
Structural questions — who depends on this, what writes to orders, what happens after POST /checkout — are answered from the graph. Open questions go to the model with retrieved excerpts. Every answer cites lines and says when the evidence is not enough. Search covers files, symbols, code, findings, and generated documentation.
Reports
Every view downloads as PDF, Word, Markdown, a web page, or JSON. The executive deck is a 14-slide briefing in business language, as PowerPoint with speaker notes, PDF, or a page you can present from. Each slide names the report section behind it.
Explainers
An Ask answer, a file, an area, a finding, or the whole system can become a clear explanation, a diagram, an interactive explainer, or a narrated video. All four come from one grounded explanation. Animation is cut to measured word timings, not a guessed speaking rate. Narration stays on the machine unless you allow a cloud voice.
Architecture
The architecture view maps layers, entry points, the API, an entity-relationship diagram, external services and what fails if they are down, environment variable names, ports, feature flags, CI, infrastructure, and tests.
Handoff
Export a project as one zip: the analysis, source with detected secrets redacted, reports, and one-click launchers. Open it in any Brody with the full interface and no re-analysis, or read the HTML report without Brody at all.
How it works
Brody does not turn a repository into one giant prompt. The pipeline below is the persisted job in src/lib/jobs/stages.ts.
Files are classified, hashed, and language-detected. Tree-sitter grammars cover TypeScript and TSX, JavaScript, Python, Go, Java, C#, Ruby, Rust, PHP, CSS, HTML, JSON, and Shell. SQL, Prisma, GraphQL, Markdown, and YAML have their own parsers. Other languages use text inspection and are marked as such, never as an AST.
Imports resolve to files, including tsconfig path aliases. Calls resolve to symbols with a confidence score. ORM and query calls become reads and writes. Routes, models, entry points, external services, environment names, tests, and infrastructure are detected from those facts. Retrieval ranks excerpts with BM25, graph neighbours, and a PageRank importance prior.
Static checks come first: built-in rules, TypeScript syntax diagnostics, ESLint with a fixed embedded config, Python ast, Ruff in isolated mode, gofmt -e, plus structural and privacy checks. Six AI passes then run over retrieved excerpts: security; privacy; reliability and correctness; performance and data; architecture and API; testing and operations. Lean 4 follows, then a verifier that re-anchors quotes and rejects patches that do not apply.
Documentation is built symbol, then file, then functional area, then architecture, then an executive summary. A deterministic baseline always exists. AI may enrich it, and statements whose evidence does not resolve to real lines are dropped. Re-analysing a changed repository reprocesses only what changed.
A refresh or a restart does not lose the job. Each stage ends done, skipped with a reason, warning, or failed.
Quick start
Node 24 is the version CI and the Docker image use (.nvmrc). AI keys are optional. Then upload fixtures/sample-shop, a small shop backend with deliberate flaws. Then open http://brody.localhost (Docker) or http://brody.localhost:3003 (npm run dev); it needs no setup.
The image includes Ruff and a Lean 4 toolchain, runs as non-root with all capabilities dropped, and keeps SQLite in the brody-data volume.
cp .env.example .env
docker compose up --buildDependencies install without running their install scripts. Optional: ruff and python3 for Python analysis, and Lean 4 for proofs. If Lean is missing, the home page can install it.
npm install
cp .env.example .env
npm run devWrites Markdown, PDF, Word, HTML, and JSON. The same npm scripts run on Windows. start brody is the macOS and Linux background helper.
npm run analyze -- ./path/to/project --out ./reportBrody answers on loopback, including any .localhost name, and on the names in ALLOWED_HOSTS (default brody), and refuses other host names. The README quick start covers that check, Windows, and start brody.
Architecture
The UI, the JSON API, and an in-process job worker share a SQLite database. Parsing uses tree-sitter WebAssembly, so install does not need a compiler. The worker can be split out with EMBEDDED_WORKER=off and npm run worker. Design notes live in docs/ARCHITECTURE.md.
Upload, ZIP, and GitHub import. Classification and secret redaction.
Tree-sitter extractors, text fallbacks, and parse worker threads.
Imports, calls, data access, and importance.
AI review passes, verification, patch checks, and dedupe.
Lean 4 targets, models, repair, the axiom check, and the fidelity audit.
Explanation IR, narration, measured timing, and video jobs.
Trees, graphs, change impact, and diagrams.
The 14-slide executive deck, from the same analysis as the report.
Security model
ZIPs are read in memory with entry, size, and compression-ratio limits. Paths that escape the archive are rejected, and symlinks are skipped. Analyzers only parse. Repository ESLint configs are ignored because they are JavaScript. mypy and go vet are not run, because they load plugins or resolve modules.
Lean source is written by a model that read untrusted code, so constructs that can execute code or fake a proof are refused before Lean runs. Lean itself gets no inherited environment, a private temporary directory, a memory cap, a heartbeat limit, and a hard kill.
To report a vulnerability in Brody itself, use private vulnerability reporting. See SECURITY.md.