Make one TypeScript function faster, and see exactly how much of "it still does the same thing" was checked.
Try it without installing anything: scasella.github.io/faithful replays recorded sessions and re-runs the checks, Z3 included, in your browser.
A model can rewrite your function so it runs faster. It can also change what the function does without telling you. In
the recorded session above, the model's rewrite of clamp dropped the check that throws when the lower bound is larger
than the upper bound. It agreed with the original on all 1000 generated test inputs. Z3, a solver that searches for a
counterexample, found one: clamp(-2, -1, -3). The original throws, the rewrite returns -1. Faithful rejected the
rewrite and showed that input.
That is the whole idea. Faithful is an LLM-assisted way to optimize a single TypeScript function: it gives a model your
function and checks every rewrite it proposes. A rewrite must compile, be free of side effects, match the original on
generated inputs, survive a bounded solver search for a difference, and measurably run faster. One that clears those and
is significantly faster is then checked in Lean 4, a proof assistant, against a spec you agreed to in plain words before
any rewrite was tried. You get a patch, the spec, the Lean file, and a VERIFY.md with which anyone can re-check the
result. Your source files are never modified.
Every result carries exactly one of five labels, and the tool never rounds a claim up: a rewrite that is faster but not proved is delivered as exactly that. What a proof covers is stated precisely below: it is about a Lean model of your function and the agreed spec, not about the TypeScript on every input.
Where it stands (0.1.0). Early. The translator accepts a narrow subset of TypeScript: 39 of the 74 functions in its own test corpus and 0 of 20 sampled from three real libraries (measured 2026-10-05). Functions outside the subset can still be optimized on the Tested label only. In the 2026-10-05 campaign, 72 of 130 candidate rewrites were faster but not proved, and 3 were accepted with a proof. The method, the tables and the caveats are in docs/LAUNCH.md.
What you need. Node 22.12 or later, pnpm, and the Codex CLI signed in: the model calls go through it and nowhere else, and nothing leaves your machine except those prompts, which the UI shows verbatim. Proofs need Lean 4 and Mathlib, about 12 GB of disk. To see it work first, use the live showcase, or the examples: five small functions to run it on.
Faithful takes one TypeScript function and looks for a faster version that does the same thing, and says exactly what was checked. A fixed translator (no model involved) turns the function into a Lean 4 model. You and a model agree on a spec in plain words, after a challenge run that looks for inputs where spec and code disagree. Lean then checks a proof that the original meets that spec. A model proposes faster rewrites, and each one must pass a compile check, a purity check, a differential test against the original, a bounded Z3 check where available, a benchmark with confidence intervals, and a Lean proof against the same spec. Only then is it delivered at the strongest label its evidence supports. The point of the tool is in one line: a faster version, checked as far as the evidence goes, and a label that never rounds up a claim.
Every claim carries exactly one label, strongest first (TIER_LABEL in packages/core/src/tiers.ts):
| label | meaning |
|---|---|
| Proved | Lean 4 accepted a theorem that Faithful wrote, relating the Lean model of the function to the agreed spec, using only the standard axioms. |
| Proved (trusting the compiler) | As Proved, except that the proof uses native_decide, so Lean's compiler and runtime are in the trusted base. |
Verified to k (shown as e.g. Verified to k=6) |
Z3 found no input within the stated bounds where the candidate differs from the original. |
| Tested | The candidate passed compile, purity and the differential test on the generated inputs, and nothing stronger. |
| Not proved | No accepted proof exists. A failed proof is a failed proof: it shows neither that the function nor that the spec is wrong. |
Wherever "Proved" appears, this sentence appears with it (N is the number of inputs on which the model was checked against the TypeScript):
Proved for the Lean model of this function. The model is produced by a fixed translator (docs/TRANSLATOR.md) and checked against the TypeScript on N inputs.
What is proved, and what is not: the theorem is about the Lean model and the agreed spec, under stated preconditions (integers within ±2^53, BMP strings, in-range indices, carve-outs you accepted). It is not a theorem about the TypeScript itself, and Faithful never says a TypeScript function was proved on every input. Each label's meaning, what it does not mean, and how it could be wrong: docs/TIERS.md.
Speedups are printed with their 95% CI and the declared input distribution. Estimates and lower bounds are rounded down and upper bounds up, and "faster" is said only when the interval, as printed, lies above 1. Faithful prints no scores, grades or percentages.
Requires Node 22.12 or later, pnpm, the Codex CLI (for model calls), and about 12 GB of free disk for the Lean toolchain
and the Mathlib cache (what faithful doctor checks).
pnpm install
pnpm build
node packages/cli/dist/bin.js doctor # checks Node, Codex, Lean, Mathlib cache, Z3, disk
node packages/cli/dist/bin.js setup --yes # installs and caches the Lean toolchain (run without --yes to read the cost first)
faithful below means node packages/cli/dist/bin.js (or pnpm faithful <command> from the repository root).
faithful setup states its cost before it starts: the pinned Lean toolchain (about 0.4 GB) and the Mathlib build cache
(about 2 GB to download, about 7 GB on disk), about 1 to 15 minutes depending on your connection. Without --yes it
prints this and downloads nothing. If elan is not installed, setup stops unless you also pass --install-elan, which
runs elan's official installer and installs Lean under ~/.elan.
faithful # open the browser UI for the repository in the current directory
faithful --repo <path> # ... or for another repository
faithful optimize <file> --fn <name> --repo <path> # run the workflow headlessly; <file> is relative to --repo
faithful optimize <file> --fn <name> --tested # if the translator refuses the function, continue on the Tested tier only
faithful verify .faithful/<fn> # re-check a delivered result without trusting it
faithful showcase-record <file> --fn <name> # record a full session for the static showcase
pnpm faithful runs in the Faithful checkout, so the current directory is Faithful itself: pass --repo to point it at
your own code (without --repo, optimize also uses the current directory). The UI also takes --port <n> and
--no-open; the browser opens by itself on macOS only, elsewhere open the URL it prints. optimize also takes
--minutes N (optimizer time budget, default 10), --proof-attempts N (default 10), --proof-minutes N (default 12)
and --yes (do not ask: treat a throw as a precondition, agree to the spec, never accept a faster-but-not-proved
candidate).
Environment: FAITHFUL_MODEL (default gpt-6-luna), FAITHFUL_EFFORT (default low; it also applies to proof attempts
unless FAITHFUL_PROOF_EFFORT is set), FAITHFUL_PROOF_EFFORT (default high), FAITHFUL_CODEX_BIN,
FAITHFUL_CODEX_TIMEOUT_MS (default 300000), FAITHFUL_Z3_BIN, FAITHFUL_LEAN_DIR.
examples/demo holds five small functions. Start the UI on them with
node packages/cli/dist/bin.js --repo examples/demo; the README there says what to expect.
- Select a function in your repository.
- Translate it into a Lean 4 model with the fixed translator, or see exactly why it is refused.
- Agree on a spec: the model proposes one in plain words and Lean; a challenge run looks for inputs where spec and code disagree; you rule on each disagreement (fix the spec, carve the inputs out, or treat a throw as a precondition).
- Prove the original meets the agreed spec (default budget: at most 10 attempts and 12 minutes; Lean checks every attempt).
- Optimize: the model proposes faster rewrites; each goes through compile, purity, differential test, bounded Z3 check (when available), benchmark, and a Lean proof for a candidate that is significantly faster than the current best.
- Deliver a patch, a provenance file and
VERIFY.md. Your source files are never modified;faithful verifyre-checks the delivery.
The translator accepts subset v1 of TypeScript: integer arithmetic (as Int with a ±2^53 range check), booleans,
BMP strings, arrays, tuples, records and options, loops and recursion with a termination measure it can find, and a
fixed library of builtins. It refuses floats, bitwise operators, regular expressions, Map/Set, dates, randomness,
I/O, async, this, generics, overloads and more, each with a refusal code and a line number. On the 74-function
corpus, 39 are in the subset; on a sample of 20 functions from real libraries, 0 are. Refused functions can still be
optimized on the Tested tier only. Full description: docs/TRANSLATOR.md.
A static site opens on a landing page, then replays recorded sessions and re-runs the funnel (translate, compile,
purity, differential, Z3) live in the browser. The default recording is clamp: a rewrite that passed 1000
differential inputs is rejected because Z3 found the input [-2,-1,-3], on which the original throws and the rewrite
returns -1. The local UI shows the same landing page as its start screen when you tick "Show this page when Faithful
opens" (kept in a session cookie).
It is hosted at https://scasella.github.io/faithful/. To build it yourself: pnpm --filter @faithful/showcase build; the output is apps/showcase/dist.
Z3 in the browser. z3-solver 5.2.0 needs SharedArrayBuffer, so it works only with cross-origin isolation. The
showcase gets it on static hosting from the vendored coi-serviceworker 0.1.7, which reloads the page once on the first
visit. Without isolation the SMT stage shows "not available here". Tested in headless Chrome (154, and 155 on the hosted site) only; Firefox and
Safari are untested.
The demo media is produced by node scripts/make-media.mjs <recording> from a real recorded session under
apps/showcase/public/recordings/ (the script refuses fixtures, and the development sample unless told otherwise). It
needs Chrome (set CHROME if it is not the macOS app path) and ffmpeg, and records the built showcase. The current files
come from apps/showcase/public/recordings/clamp.json.
The GIF at the top is docs/media/faithful-demo.gif.
Video (MP4, 1280x720): docs/media/faithful-demo.mp4
packages/core tier vocabulary and the Proved sentence, toolchain stamp, subprocess runner, .faithful store
packages/translate TypeScript subset v1 -> Lean 4 model (deterministic; no model call)
packages/engine sandbox, differential and mutation testers, benchmark, evidence line
packages/smt IR -> SMT-LIB, Z3 drivers, "Verified to k"
packages/prover Lean project, proof checking, axiom policy, Codex driver, spec and proof generation
packages/session event-sourced session state
packages/cli faithful commands, local server, autopilot for measurements
apps/ui browser UI served by the CLI
apps/showcase static replay site
lean/ Lake project: pinned Lean 4.34.0 + Mathlib, Faithful runtime library
- docs/DESIGN.md: the design contract, non-negotiables, deviations
- docs/TIERS.md: what each label means and does not mean
- docs/TRANSLATOR.md: the subset, the translation, refusal codes, gaps, red-team history
- docs/SMT.md: the bounded SMT tier
- docs/PROOFS.md: proof generation, checking, tuning and held-out results
- docs/BENCH.md: benchmark method and limits
- docs/SECURITY.md: what is isolated, what leaves the machine, what is not protected
- docs/LAUNCH.md: launch report with the measured tables
MIT (LICENSE). Code adapted from other projects, the library sample's sources, the vendored service worker and the third-party software shipped in the showcase are listed in NOTICE.md.
Faithful runs the Codex CLI, Lean 4 with Mathlib, and Z3 as separate tools on your machine. It does not redistribute them, except Z3's WASM build in the static showcase, and it is not affiliated with their authors.