TokenMasterX GitHub

For GitHub Copilot CLI

About half the tokens with --lean.

--lean is a launcher flag. It drops the tool definitions your prompt does not need.

  • Up to · with --lean53%fewer tokens
  • Up to · with --lean54%lower cold-start cost
  • No flags9–29%fewer tokens

Measured November 1, 2026 under GitHub's default routing, on Copilot CLI 1.0.105 with GPT-6 Astra, on 15 short Django caller lookups. Each saving is against its own stock run on the same day. "Up to" is the best pooled result of any run under default routing. The no-flags range is the 95% confidence interval of its run; the point estimate is 19%.

Proof-driven. The rules behind these savings are proved by a computer, and the code is held to those proofs.
Start Results Proofs Install

01What every call carries

Every call pays for the same prompt again.

Copilot CLI sends its system prompt and every tool definition with each request, and each request is billed for them. TokenMasterX removes tools only when you start the launcher with --lean, and it keeps a family when the launch prompt or flags ask for it.

First-call input tokens

13,589

Median of 15 lookups, as billed by GitHub. One chip is about 125 tokens.

Same as stock.

Tool definitions in the request

7,819

Copilot CLI's own estimate. Every built-in tool is sent.

Hover or tap a tool to see what keeps it.

02What that adds up to

A smaller prompt adds up with every call.

With --lean, each call carries 7,555 fewer input tokens: the drop in median first-call input, from 13,589 to 6,034. Set the slider to your own volume.

100

755,500input tokens a day not sent

$0.76a day at the cache-read price

GPT-6 Astra reads a cached token at $1 per million and writes one at $12.50. A call that misses the cache costs more, so the dollar figure is a floor. The estimate counts input tokens only and assumes the number of calls does not change. For your own bill, type /tokenomics in Copilot CLI.

04Trim without breaking the cache

Shape each tool result once, as it arrives.

A provider's prompt cache matches from the first byte. Reading a cached token costs 0.05 to 0.1 times the input price, and writing one costs 1.25 times. Change an earlier byte and everything after it is written again.

16ktokens sent
15kread at 0.1×
1kwritten at 1.25×
2.75kcost, in input-token units

An illustration with round numbers: one chip is 1,000 tokens, with GPT-6 Astra's price ratios. The measured case is PRS-1, where rewriting old tool output (v5) raised cache-weighted cost by 61.6% (95% CI +19.6% to +111%). A computer-checked proof shows that shaping each result once leaves earlier messages unchanged. Under default routing only the view hook shapes output. In bring-your-own-model mode a local bridge shapes grep, glob and whole-file view results and keeps the session folder out of the system prompt, so sessions in one folder share a cached prompt.

05What we measured

Savings against stock Copilot CLI, run by run.

Each bar is the reduction against the same run's stock arm, and the white line is its 95% interval from a paired bootstrap over tasks. Cold-start cost prices each first call as a cache miss; as billed is what GitHub charged. Tables, protocols and limits.

06Proof-driven development

The savings are measured. The rules behind them are proved.

Each mechanism has rules the code must always keep, such as never changing text the provider has already cached. We state them as theorems about a model of the code and check the proofs with Lean 4, which accepts a proof only if every step is valid.

  1. 1

    State a rule the code must keep.

  2. 2

    Prove it, and let a computer check the proof.

  3. 3

    Hold the code to the proof, and change them together.

What is proved

  • Lean
    Cache.bridge_prefix_stable Cache.cache_prefix_kept
    Holds when
    Assumes call ids are never reused, the client sends the same instructions and tools on every call, and the provider caches them ahead of the items. A lone surrogate in a tool output breaks the token counter.
    Checked by
    test_bridge_rewrite_keeps_history_prefix
  • Lean
    Cache.shaping_prefix_stable
    Holds when
    Proved for the shaping map. The runtime keeps it unless shaping would pass a max_input_tokens cap. Assumes call ids are never reused.
    Checked by
    test_v6_plans_keep_earlier_messages test_runtime_keeps_v6_shaping
  • Lean
    Shaping.guard_never_expands Shaping.request_bytes_never_grow
    Holds when
    True in counted tokens and in bytes. That GitHub's billed count falls when the cl100k count falls is an assumption.
    Checked by
    test_shaped_results_never_expand
  • Lean
    Policy.greedy_never_expands Policy.protected_unchanged
    Holds when
    They also never edit a protected message. A test checks this for policy v1.
    Checked by
    test_plan_request_never_expands_and_keeps_protected_messages
  • Lean
    Folds.unfoldPaths_foldPaths Folds.unfold_foldSearchChecked Folds.foldSearch_not_injective
    Holds when
    fold_paths gives back its exact input. fold_search refuses any input it could not give back, and a proof shows the refusal is needed: without it, two different inputs fold to the same text.
    Checked by
    test_fold_paths_round_trip test_fold_search_round_trip and 1 more
  • Lean
    Routing.fired_family_kept Routing.excluded_subset_lean Routing.default_excludes_nothing
    Holds when
    Proved for the model, which drops only the 13 auxiliary tools. That the launcher routes only with --lean is a definition in the model, checked on main by a test. The triggers are keyword rules and miss some phrasings: "have an agent review this diff" drops task.
    Checked by
    test_routing_default_sends_every_tool test_routing_lists_match_the_lean_model and 1 more
  • Lean
    Routing.resume_same_list Routing.resume_chain_keeps_first_list
    Holds when
    Proved for the model, when the resume's TOKENMASTER_KEEP_TOOLS adds no tool. Which session record applies is the launcher's lookup, which the conformance tests check. A resume the launcher cannot tie to a record is routed again, and a resume without --lean sends every tool.
    Checked by
    test_routing_resume_keeps_the_first_list
  • Lean
    SessionPrefix.system_same_across_sessions SessionPrefix.folder_recoverable
    Holds when
    There is exactly one folder line, and only the BYOK bridge does the rewrite. The folder path is assumed to have no newline, and whitespace around it is not recovered after the move.
    Checked by
    test_session_prefix_same_system_and_recoverable_folder
  • Lean
    NavCap.assemble_le NavCap.fit_prefix NavCap.uncut_overflow_attained
    Holds when
    Counted in the navigation server's own counter, with every result measured whole. Its fallback estimate can undercount non-ASCII text. The proofs found a case that reached 2,401 tokens, and it is fixed.
    Checked by
    test_navigation_results_within_budget test_uncut_read_within_budget and 2 more
  • Lean
    Measurement.cold_term_is_coldened_charge Measurement.ratio_of_sums_ge Measurement.resample_within_task_range Measurement.hero_monotone
    Holds when
    Cold repricing is exactly the extra charge of a cold cache, and the bootstrap interval stays within the per-task range. The recorded data match. Not proved: the interval's 95% coverage, and the Wilcoxon and Holm-Bonferroni steps.
    Checked by
    test_cold_repricing_matches_the_definition test_bootstrap_interval_within_task_range and 2 more

Hover or tap a claim to see its theorems, what it assumes and the tests that check it.

07How it is checked

A proof covers a model. Four checks tie it to the real code.

  1. 1

    Lean checks every proof.

    Lean 4 accepts a proof only if every step is valid, and a clean build means no step was skipped.

  2. 2

    Tests run the real code.

    Conformance tests run the Python on generated inputs and on the recorded study data. Each names the Lean theorem or definition it checks.

  3. 3

    Every assumption is written down.

    The write-up lists what the models assume about the code and marks each as tested, read from the code, or assumed. One is known to be false: the token counter raises on a lone surrogate (open finding 1).

  4. 4

    Gaps become findings.

    Where a claim and the code disagree, the gap is recorded. Writing and reviewing the proofs found mistakes in our own claims. Most are fixed, and the rest are published.

Code and proofs change together: #18, #19 and #20, the last three routing pull requests, each updated the proofs write-up and the conformance tests; #18 and #20 also changed Routing.lean.

What writing the proofs found

  • Navigation results could pass the 2,400-token cap: footers sat outside the budget, and one branch skipped a newline (2,401 tokens observed). Every result is now measured whole.
  • fold_search was not lossless when a copied line looked like a folded entry. It now refuses to fold that input.
  • fold_paths dropped trailing newlines. It keeps them now.
  • v6 shaping reverted a whole request when it measured no smaller on the JSON wire, which is not what a provider bills, so that call missed the cache. It no longer does.
  • A resumed session ran the routing again, so its tool list could change. A resume tied to the session's record now sends the recorded list.
  • A lone surrogate in a tool output makes the token counter raise, which fails that bridge call and every later call that resends the output.
  • The routing triggers miss some phrasings: "have an agent review this diff" drops task.
  • Whitespace around the session folder path is not recovered after the move.
  • Open findings stay published. Where a test can reproduce one, it does.

Check it yourself

lake -d proofs build
python -m pytest token-master-plugin/skills/token-master/tests/test_proof_conformance.py

Run both from the repository root. Install Lean 4 with elan first; lake reads the pinned version from proofs/lean-toolchain.

08What these numbers do not say

Read them with their limits.

Scope

  • Fifteen short lookups. Each November 1 session made two to four model calls. Long coding sessions were not measured.
  • One model on one build: GPT-6 Astra on Copilot CLI 1.0.105. PRS-6 added Claude Opus 5.5 on 1.0.98, through an evaluation relay.
  • --lean removes the same fixed prompt from every request, so it should save a smaller share of a long session. How much smaller is unmeasured.
  • With no flags, the saving comes from fewer model calls. These tasks ask the question navigation answers.
  • Two identical stock runs on the same day differed by 8.6% in raw tokens. The intervals do not include that noise.
  • Every session passed its grader in both November 1 runs, and both arms of PRS-6 passed all 88. The graders check lookups and a few edits.
  • Cold-start cost prices each first call as a cache miss. The bill itself fell 47% with --lean.

Retired or retracted

  • "Up to 58% fewer tokens." That was the best cell of PRS-6's relay run. It did not reproduce under default routing on October 27, when the lean tool set saved 47%.
  • The October 17 figures, which the repository retracted.
  • The early 72% Django pilot, which was never replicated.
  • History rewriting (v5), which raised cache-weighted cost by 61.6% in PRS-1.
  • Before the lean tool set, TokenMasterX saved cost on Copilot CLI but not reliably raw tokens.

Negative results stay published. They are in the results doc and its linked protocols.

09Try it

Install it, then run Copilot through it.

Windows PowerShell commands. The measured runs used graphify 0.9.91.

Leave out --lean and Copilot CLI keeps every built-in tool. Navigation and the view hook still work.

--lean reads the launch prompt (-p or -i), your flags and the skills and agents you have installed. An interactive session that starts without a prompt, and without a flag such as --agent, --fleet or --resume, keeps all 13 tools out, so set TOKENMASTER_KEEP_TOOLS if you need subagents or background shells mid-session.

Type /tokenomics in a session, or run tokenomics.py in a terminal for 0 model tokens, to see your measured tokens, GitHub's charges and the estimated savings.

1

Add the plugin

copilot plugin marketplace add All-The-Vibes/TokenMasterX
copilot plugin install token-master@token-master
2

Prepare the runtime, once

$plugin = "$HOME\.copilot\installed-plugins\token-master\token-master"
$runtime = "$HOME\.copilot\token-master-runtime"
uv venv --python 3.12 $runtime
& "$runtime\Scripts\python.exe" -m ensurepip
& "$runtime\Scripts\python.exe" -m pip install -r "$plugin\requirements-runtime.txt"
& "$runtime\Scripts\python.exe" -c "import tiktoken; tiktoken.get_encoding('cl100k_base')"
uv tool install graphifyy
3

Set up your repository

Start copilot in the repository and type /token-master. It indexes the repository with Graphify, then installs navigation, the view hook and /tokenomics. Approve the commands when Copilot asks.

4

Start Copilot through the launcher

& "$HOME\.copilot\token-master-runtime\Scripts\python.exe" "$HOME\.copilot\token-master\brainspace_copilot_bridge.py" --lean -- copilot

10Check our work

Every number links to its protocol and its per-call records.

Results and limits

Every run, interval and caveat, with how each figure was counted.

Proofs, checked by Lean 4

The proofs, the assumptions they make about the code, and the gaps found while writing them.

November 1: --lean

The protocol, written and hashed before the first session, with the analysis and per-call records.

November 1: no flags

The default setup, measured the same day on the same build against its own stock run.

PRS-6 protocol

Pre-registered before any study call, with the decision rules fixed in advance.

Mission and method

Why the harness is the unit of intervention, and the rules for measuring it.

MIT license. An experimental research toolkit, not an official GitHub product. github.com/All-The-Vibes/TokenMasterX