ProofLadder

Debuggers fix code. ProofLadder debugs the programmer.

ProofLadder is an evidence-first diagnostic instrument for people learning to code. Given failing Python code and its problem statement, it forms a hypothesis about the learner's reasoning, asks an adversarial verifier to try to falsify that hypothesis, executes the experiments in a sandbox, and acts only on evidence that survives.

It is not a chat tutor and it does not reveal a corrected solution to the original problem. Its visible product loop is:

Theory -> Experiments -> Verdict -> Drill

Raw machine evidence is available behind a toggle; the default experience stays in plain language.

Track: Education. Built with Codex and GPT-5.6 for OpenAI Build Week.

Requirements and supported platforms

• Python 3.11 or newer.
• A modern browser.
• Windows, macOS, or Linux for the local demo. Process resource controls differ by operating system; this is not a multi-tenant public-execution service.
• An OPENAI_API_KEY for live diagnosis, verification, and drill generation.

The application intentionally has no third-party Python dependency. It uses the standard library plus the OpenAI Responses API over HTTPS when live model access is configured.

Run locally

Start the local server from the repository root:

python server.py

Then open http://127.0.0.1:8000.

To enable the live GPT-5.6 runtime, use one of these approaches before starting the server. For a local demo, the most convenient approach is a repository-root .env file (copy .env.example and replace only the placeholder):

OPENAI_API_KEY=sk-...

The application loads this file automatically, never logs its contents, and the repository's .gitignore excludes .env. Do not put a real key in source code, a tracked file, or Git history.

Alternatively, set an API key in the shell that launches the server:

$env:OPENAI_API_KEY = "sk-..."
python server.py

export OPENAI_API_KEY="sk-..."
python server.py

PROOFLADDER_MODEL defaults to gpt-5.6 and may be set explicitly when needed.

If the live model is unavailable

The server still starts, but it does not substitute a canned diagnosis, fixed test inputs, reference solution, or drill for live GPT-5.6 reasoning. The investigation ends in an explicit unavailable or unverified state with its provenance shown in the UI. That is intentional: an honest non-confirmation is better than a fabricated result.

If diagnosis and verification have already completed but only the optional drill generator becomes unavailable, the evidence-backed verdict remains visible and the drill is withheld rather than replaced with a template.

Sample data and judge path

fixtures/corpus.json contains seed cases used to exercise the normal input path. They are demo data with human-reviewed labels, not proof of a live diagnosis. Load one from the browser, or paste your own valid Python and problem statement. The repository bundles fixtures/golden/recorded-run.json: a provenance-checked GPT-5.6 recording that makes Replay available from a clean checkout without requiring the judge to spend API credits. The recorder refuses to write that file unless a live auto-mode investigation confirms the seed's human-reviewed pointer_aliasing label, so a mislabeled take can never ship as the flagship recording.

For a judge run:

1. Start the server and open the local URL. No API key is needed to run the static interface.
2. If a verified recording is bundled, select Replay verified live record to see the captured GPT-5.6 evidence. Otherwise Replay honestly remains disabled.
3. For a new live investigation, configure OPENAI_API_KEY, load a seed case, and select Begin investigation.
4. Confirm that the UI identifies the provider, displays the experiment evidence, and either produces a defensible verdict or explicitly says unverified.

The Golden control is an input convenience only. It must use the same automatic analysis path as any other submission. Replay, when available, is clearly labeled as a recording of a provider-backed run; no canned replay is bundled as live model evidence.

To make Replay available after a fresh clone, run the live recorder with a configured key:

python scripts/record_golden.py

It writes fixtures/golden/recorded-run.json only after a confirmed live gpt-5.6 investigation produces a validated drill and passes its provenance checks. Inspect and commit that generated recording; never create a substitute fixture by hand.

Tests and developer checks

Run the complete Python suite and the frontend syntax check:

python -B -m unittest discover -s tests
node --check web/app.js
node --check web/learning.js

To validate a clean checkout before sharing it with judges, run the same commands from the repository root, then start python server.py and confirm:

• http://127.0.0.1:8000/ serves the interface;
• http://127.0.0.1:8000/api/health returns JSON with ok: true;
• http://127.0.0.1:8000/api/corpus returns the bundled seed cases; and
• the Replay control is enabled and labeled as a recorded live session.

Without OPENAI_API_KEY, a new analysis is expected to close as unverified. That is a successful fail-closed setup check, not an installation failure.

Optional developer measurement scripts live in scripts/. Their reports are artifacts of the runtime and configuration used when they were run; they are not a substitute for a fresh live-model rehearsal.

How it works

1. AST fingerprint: extracts limited structural signals from submitted Python.
2. Diagnostician (GPT-5.6): emits a strict-JSON hypothesis from a fixed gap taxonomy.
3. Adversarial Verifier (GPT-5.6): proposes experiments intended to disprove the hypothesis.
4. Sandbox: runs code and references under policy, timeout, and output limits.
5. Evidence gate: only grounded evidence can confirm a diagnosis; otherwise the session is refuted or remains unverified.
6. Micro-problem generator (GPT-5.6): creates a sandbox-validated drill only after a confirmed gap. The hidden reference solution is never sent to the browser or ledger.
7. Skill ladder: persists progress by reasoning gap.

The evidence ledger records the investigation events so the UI can narrate the actual execution rather than a prose-only explanation.

After a terminal investigation, Download dossier creates a self-contained, print-friendly HTML record in the browser. It includes only ledgered theory, execution, verdict, validated-drill, refutation, and timeline evidence; a protected reference solution stops the export rather than being included.

The Class Misconception Atlas is a read-only view over recorded ledgers and persisted skill ladders. It shows no sample statistics: until a confirmed ledger exists, it explicitly says that the Atlas has no data yet. Refuted hypotheses also remain visible in the per-session graveyard rather than disappearing when a later theory replaces them.

Architecture at a glance

The full diagram suite lives in docs/DIAGRAMS.md as Mermaid sources that GitHub renders natively, with matching PNG exports in docs/diagrams/:

• Low-level investigation pipeline — the evidence gate in detail, including both fail-closed paths.
• Live investigation sequence — the polling browser and the worker thread side by side.
• Session state machine — why refutation is evidence, and why terminal states are only confirmed or unverified.
• Module dependency map — verified against the actual imports; no module imports a third-party package.
• Evidence products — Atlas, dossier, graveyard, and the double-gated Replay flow.

Measured behavior

These numbers were measured by scripts/grade_corpus.py against the human-labeled seed corpus using the live gpt-5.6 runtime on 2026-07-19. The per-case table is in reports/accuracy.md; rerun the script with your own key to regenerate it. ProofLadder quotes only numbers a fresh run can reproduce.

• Final-diagnosis accuracy: 7/8 against human ground-truth labels.
• Verified precision: 5/6 — of the six sessions the instrument confirmed with executed experiments, five carried the correct label.
• Honest abstentions: 2 — both closed unverified with the correct gap identified but unproven, rather than presenting an unearned confirmation.
• The one incorrect confirmation (a sibling dynamic-programming category) carried 0.99 pre-test confidence: on this run the instrument was most confident exactly where it was wrong. The report records that calibration failure instead of hiding it.

GPT-5.6 and Codex

GPT-5.6 is the live runtime, not a chat layer. It produces strict structured data for the Diagnostician, Adversarial Verifier, and Micro-problem Generator. The product distinguishes provider-backed results from unavailable, unverified, and replay states rather than presenting fallback templates as model output.

Codex accelerated the build. Concrete architecture, verification decisions, and the designated /feedback session ID are recorded in docs/SUBMISSION-EVIDENCE.md. The required ID belongs in the Build Week submission form; do not invent one or replace it with an unrelated chat URL.

Research grounding

The motivation is narrow and evidence-based. The Correct Answer Trap paper reports that models can under-detect flawed student reasoning when an answer happens to be correct. Related work includes McMining and misconception diagnosis from student-tutor dialogue.

Those papers motivate evidence-seeking diagnosis; they do not prove that ProofLadder is the first product of its kind, so this repository makes no universal novelty claim.

Future development

Planned work follows the same rule as the current build: no capability ships without the evidence gate that keeps it honest.

Near term

• Grow the seed corpus well beyond eight cases and widen the reasoning-gap taxonomy, keeping every label glossed with a definition so the Diagnostician classifies against mechanisms rather than guessing at bare terms.
• Capture additional flagship recordings, including a genuine refute-then-revise session, so the theory-graveyard arc is replayable evidence rather than a description.
• Use measured calibration failures (see the 0.99-confident miss above) to tune confirmation thresholds: an overconfident category should have to earn confirmation with sharper experiments, not fewer.

Medium term

• Languages beyond Python — JavaScript and Java first — through pluggable AST fingerprinting and per-language sandbox runners behind the same evidence gate.
• Classroom deployment: an authenticated multi-learner service with container-isolated execution, where the Class Misconception Atlas becomes the teacher's console and dossiers become hand-in artifacts.
• LMS and GitHub Classroom integration so investigations attach to real assignments instead of pasted snippets.

Long term

• Publish the verified misconception-fingerprint dataset (the scripts/export_fingerprints.py artifact) as an open research resource once it is large enough to support conclusions.
• Learning-outcome measurement: track whether learners who complete gap-matched drills stop re-triggering the same fingerprint in later submissions — the only metric that ultimately justifies the instrument.

Security posture

The sandbox is defense-in-depth for a local demo: AST policy checks, an isolated temporary directory, a restricted Python invocation, timeouts, resource controls where the operating system supports them, and bounded process output. It is not a replacement for container isolation, authentication, or multi-tenant controls in a public deployment.

Repository layout

app/        contracts, AST features, live agent runtime, sandbox, ledger, Atlas aggregates, pipeline
web/        zero-build browser interface, dossier export, Atlas, and live evidence narration
fixtures/   seed corpus and Golden input fixture
scripts/    optional recorder and measurement utilities
tests/      standard-library unit and HTTP tests
docs/       project guides, API reference, diagram suite, and Codex collaboration record

Documentation

• Getting Started — clone, configure, and run the app.
• Configuration — environment variables and local-server defaults.
• Architecture — system boundaries, data flow, and evidence lifecycle.
• Diagrams — Mermaid architecture, pipeline, sequence, and state diagrams with PNG exports.
• API Reference — local HTTP endpoints, request contracts, and error behavior.
• Development and Testing — contributor workflow and validation commands.
• Codex collaboration log and submission evidence — Build Week implementation narrative and required Codex session record.

Installation

ProofLadder needs no Python package installation. Clone the repository and use Python 3.11 or newer:

git clone https://github.com/Unknown1502/ProofLadder.git
cd ProofLadder

The local server uses the Python standard library. Node.js is only needed for the optional frontend syntax check listed above.

Quick start

1. For a live investigation, copy .env.example to .env and replace its OPENAI_API_KEY placeholder, or set that variable in the shell.

2. Start the local server:

   python server.py

3. Open http://127.0.0.1:8000, select Load sample case, then select Begin investigation.

Usage examples

Investigate a bundled learner submission

Choose a seed case from Load a seed failing submission (or use Load sample case) and begin an investigation. With a configured live runtime, ProofLadder records the hypothesis, executable experiments, and a verdict; without one, it ends in an explicit unverified state instead of fabricating a diagnosis.

Check whether live credentials are available

After starting the server, query its local health endpoint:

curl http://127.0.0.1:8000/api/health

The JSON response includes "ok": true, "runtime": "proofladder", and an openai_configured boolean without exposing the API key.