Proof-carrying debugging

Most tools guess.
Buggy executes, then proves.

Buggy runs your function against the inputs most likely to break it. When one does, it verifies the failure three separate ways before calling it a bug — then writes candidate fixes and scores each one for overfitting. It never edits your code on its own.

Install it See the pipeline

Node 18+ · TypeScript & Python · runs fully offline · MIT

buggy investigate

Example session transcript:

$ buggy investigate splitExpense --file src/expenses.ts

Debugger initialized.
Parsed src/expenses.ts — 1,284 CST nodes, 0 syntax errors.
Proving: generating edge-case inputs.
Executed splitExpense(0, 0) in a child process.

Investigation Report
Status: confirmed_and_repaired

Proof-of-Failure Certificate
  Violated postcondition: isFinite(result)
  Input: [0, 0]
  Observed output: NaN
  Admissible: inputs satisfy all preconditions
  Sound: NaN genuinely violates the postcondition
  Reproducible: 3 of 3 re-executions failed identically

Approved patches: 1, with overfitting probability 12.4 percent.
  if (people === 0) { return 0; }

0pipeline phases

0proof pillars

0classifier dimensions

0MCP tools

0tests in the suite

The gap Buggy fills

Static analysis tells you where a bug might be. AI assistants write a fix that looks right. Neither one proves anything, and both hand you the triage work.

The usual loop

A warning fires on a line that execution may never reach.
You read the code to decide whether it is real. That is the expensive part.
A patch lands, the suite goes green, production finds the edge case.
Nothing checked whether the fix generalises past the example that caught it.

With Buggy

A concrete input is produced that actually breaks the function.
The failure is re-run and re-checked before it is reported at all.
Fixes are derived from the failing input, not from a generic template.
Every patch carries an overfitting score. High scorers are rejected outright.

Four phases, run in order

An orchestrator drives each phase and stamps a timeline entry as it completes. If anything throws, the run halts and keeps whatever it had already produced.

Parse — build a tree that survives broken code

Tree-sitter produces a concrete syntax tree that keeps every space and comment. Invalid regions become error nodes carrying a byte offset and length, so a file that does not compile still gets analysed.

Fault-tolerant CST
Incremental re-parse
LSP symbol resolution
Bundled TS + Python grammars

Prove — find a real failing input, then distrust it

The fuzzer tries the values that break arithmetic first — 0, NaN, ±Infinity, MAX_SAFE_INTEGER, empty arrays — before any random input. Each candidate runs in a child process, and a violation only becomes a certificate after admissibility, soundness and reproducibility all pass.

Edge cases before randoms
Real execution, not simulation
Timeout · crash · NaN · postcondition · determinism
2 of 3 re-runs must reproduce

Repair — guard the input the proof blames

The certificate says price(0, 0) raised a division error, so the guard tests quantity == 0 rather than a generic null check. Five strategies produce structurally distinct candidates, and a dialect layer renders them as valid TypeScript or valid Python.

Trigger-derived guards
Clamping for magnitude bugs
5 strategies
Never writes to your files

What a certificate has to survive

A crash alone is not evidence. Three checks have to pass, and failing any one of them means nothing is reported.

Admissibility

The triggering input is re-checked against every precondition. A bug reached through an input you promised would never arrive is not your bug.

Soundness

The function is executed again and the output is re-evaluated against the postcondition. The violation has to still be there on a clean run.

Reproducibility

Three further executions, of which at least two must fail identically. A flake that cannot be reproduced never becomes a certificate.

Why the evidence survives storage. The values that trigger numeric bugs are exactly the ones JSON.stringify destroys — NaN becomes null, undefined breaks the database bind. In a proof-carrying tool the observed output is the evidence, so every one of them is written with an explicit sentinel token instead.

66 numbers decide whether a patch ships

A patch that special-cases the input which caught it passes every test you have and fails in production. Buggy measures the shape of the edit rather than trusting the suite.

11: AST properties — statements, branches, loops, calls, declarations, assignments, returns, literals, operators, nesting depth, identifiers
×3: Edit states — generated, deleted, remaining
×2: Raw counts, then normalised
=66: Dimensions in, one overfitting probability out

Patches at or below 0.5 are approved. Above it they are rejected and the three properties that pushed the score up are reported, so the verdict is inspectable rather than a black box.

generated deleted remaining

approve0.12reject

What you get

Everything runs locally. No API key, no account, no network call.

⌘

A real CLI

init with a setup wizard, then analyze, investigate, status and halt. JSON output on every command for scripting.

⇄

MCP server

Seven tools over stdio for Kiro, Cursor, Windsurf, Claude Desktop or anything else that speaks the protocol.

{ }

Embeddable API

One ProofDebugger class for CI jobs, internal dashboards and custom tooling.

◇

Two languages, one pipeline

TypeScript and JavaScript run through a Node child process; Python through a real interpreter. Patches are emitted in the right syntax either way.

◉

Memory that carries over

Every investigation becomes an episode. Verified ones turn into lessons your editor reads back before it touches the same code again.

▣

Read-only by default

Patch generation runs through a no-op writer. Candidates are produced, scored and shown — applying one is always your call.

The Watchlist

Each run is recorded with what triggered the bug, which patches were rejected and how they failed. Verified runs become lessons, promoted outward through three tiers.

local Private to you

Every episode lands in the SQLite file under .debugger/, which init adds to your .gitignore.

team Committed for the repo

Verified lessons are rewritten into a steering file your editor loads automatically, so the next person gets the same warning.

global Across your projects

Promoted only after the same lesson appears in two separate projects, and sanitised to patterns and type shapes — never source, paths or values.

Then it checks whether that helped

Recording lessons is easy. Knowing if they worked is the part that usually gets skipped.

retrospect Did the fix hold?

Each lesson is read as a timeline, separating fixes that held from ones that regressed — proven again after being repaired. That is the case where the memory existed and the defect still came back, which usually means the patch guarded the triggering input rather than the cause.

dead ends Stop retrying what failed

Rejection reasons are normalised and counted, so an approach that keeps getting rejected becomes a named dead end instead of something the agent rediscovers every session.

suggest Propose the missing guardrail

When a defect class keeps recurring, the answer is usually a new guardrail rather than another patch. Buggy proposes hooks, steering rules and skills built from its own evidence — each naming the episodes behind it, and each written only when you accept it.

Three ways to drive it

Same core underneath all of them.

# set up once — the wizard detects your language
buggy init

# parse a file and show what was found
buggy analyze src/expenses.ts

# run the full pipeline on one function
buggy investigate splitExpense --file src/expenses.ts --verbose

# machine-readable, for CI
buggy investigate splitExpense -f src/expenses.ts --json

{
  "mcpServers": {
    "buggy": {
      "command": "buggy-mcp",
      "autoApprove": [
        "buggy_analyze",
        "buggy_list_functions",
        "buggy_investigate",
        "buggy_recall"
      ]
    }
  }
}

Tools exposed: buggy_init, buggy_analyze, buggy_investigate, buggy_status, buggy_query_graph, buggy_list_functions, buggy_recall, buggy_retrospect, buggy_suggest_capabilities, buggy_apply_capability.

import { ProofDebugger } from 'buggy-debugger';

const dbg = new ProofDebugger({ projectRoot: '/path/to/project' });
await dbg.initialize();

const report = await dbg.investigate({
  functionId: 'splitExpense',
  filePath: 'src/expenses.ts',
  specification: {
    preconditions:  ['people >= 0'],
    postconditions: ['isFinite(result)', 'result >= 0'],
  },
});

// 'confirmed_and_repaired' | 'confirmed_no_repair' | 'unconfirmed' | 'halted'
console.log(report.status, report.proof, report.approved_patches);

await dbg.shutdown();

Install

Install straight from the repository. It compiles itself during install, so there is no separate build step.

Add it

# global — gives you `buggy` and `buggy-mcp`
npm install -g buggy-debugger

# or as a project dependency
npm install buggy-debugger

Published as buggy-debugger — the bare name buggy on npm is an unrelated issue tracker. The commands it installs are still buggy and buggy-mcp. Installing from github:himanshusaini-afk/buggy also works.

Set up your project

cd /path/to/your/project
buggy init             # interactive
buggy init --yes       # accept detected defaults

Writes .debugger.yaml, creates .debugger/ and offers to git-ignore it. Prompts are skipped automatically when stdin is not a terminal, so it is safe in CI.

Find a bug

buggy investigate splitExpense --file src/expenses.ts

Or build from source: git clone, npm install, then npm link to expose both binaries.

Requirements

Node 18 or newer.
Grammars are bundled. Nothing extra to install for TypeScript or Python parsing.
Python on PATH to prove Python code — python on Windows, python3 elsewhere. Override with BUGGY_PYTHON.
An LSP server is optional. Symbol resolution degrades quietly without one.

What runs today

The repository contains more than the live pipeline currently calls. Rather than let the diagram imply otherwise, here is the split.

Wired and running

Tree-sitter parsing with error recovery, incremental re-parse, LSP resolution
Execution-based fuzzing with edge-case-first input generation
Five oracles: timeout, crash, NaN/Infinity, postcondition, determinism
Three-pillar certification: admissibility, soundness, reproducibility
Trigger-derived repair with TypeScript and Python dialects
66-dimensional overfitting classification
Watchlist recording and recall across all three tiers
Retrospective analysis and the capability advisor
CLI, MCP server and programmatic API

Present, not yet in the pipeline

Firecracker microVM isolation — today the boundary is an OS child process
Compile and test filtering of patches before classification
PROBE adversarial property refinement
SpecTune alpha-consistency refinement
TrajSpec commit-history interpretation
SAFuzz region-biased mutation
Backward slicing for defect localisation
Differential test generation
OAP passports, circuit breaker and snapshot pool
Call-graph population, so graph queries return empty
The four plug-in extension points

Worth saying plainly. Untrusted code currently runs in a child process, not a hardware-isolated VM, and an approved patch has passed the overfitting check only — it has not been compiled or test-run for you. Read the diff before you apply it. The full module-by-module split lives in FEATURES.md.

Point it at your riskiest function.

If there is an input that breaks it, you will have the input — not a warning.

Open the repository Install

Most tools guess. Buggy executes, then proves.