Guide

Worked WebMCP requests

Start with the before-and-after programs for organization and access. They include complete requests with the source filled in. The calls below cover verification, frontend generation, and reports. The editable safety lessons demonstrate owner keys and role authority; analysis input recipes provide complete protocol cases and implementation views.

Read each linked file as UTF-8, then replace the uppercase variable with its full text. Pass sources as an array of file objects and numeric parameters as numbers. Most calls work through the browser connection or local Node server; the Lean proof call below needs a configured native or Node host, or the isolated browser Lean Wasm page.

If a result differs, call api_compile with the same sources. Check the source files and topology, then follow the reported finding.

api_law_check over an explicit Bosatsu domain

Use the complete finite-law Bosatsu source. It declares a FiniteObligation over the distinct values [1, 0], a predicate that accepts only zero, and a witness that reaches zero. Run:

api_law_check({
  "sources": [{
    "fileName": "finite-law.bosatsu",
    "source": LINKED_FILE_CONTENTS
  }],
  "mode": "exhaustive",
  "maximum": 2
})

The result is violated with replayable input 1; its listed scope records two values entries with replayable input values 1 and 0, not just their count. Reducing maximum to 1 is inconclusive, never a sampled pass. api_obligations currently accepts sampled Obligation declarations only, so this finite verdict does not select a commit strategy.

api_lean_check on a direct Bool law

Use the complete Bool-law Bosatsu source. It declares a law over both Bool values and a witness that True exists. With a local proof host configured, or on the browser Lean page, call:

api_lean_check({
  "sources": [{
    "fileName": "lean-bool.bosatsu",
    "source": LINKED_FILE_CONTENTS
  }]
})

The default compact result keys rows by obligation and names each proved predicate, its quantified domain, and fullReceiptSha256. An inconclusive not-admitted row means this translation or method could not check the law; seek another proof route rather than treating the law as false. Pass that digest back as receipt_sha256 to the same live host to fetch the exact full lean-law-run native receipt or lean-wasm-law-run Node or browser receipt; a missing cache entry requires another check of the current source. The main browser workbench needs a proof host; its separate Lean page runs the pinned Wasm checker. A false mutation, unsupported translation, or incomplete checker run does not produce a verified receipt. The command-line equivalent is yichus lean --toolchain PATH --source lean-bool.bosatsu --json --view compact --result FULL.json; the result file holds the full native receipt named by the view’s digest. The Node CLI uses yichus lean lean-bool.bosatsu --lean-wasm-root DIRECTORY and records that independent kernel replay was not run.

api_lean_check on a recursive list law

Use the complete List[Bool] Bosatsu source. Its check recurses on the bound tail of a Nil/Cons match. The generated Lean theorem uses induction to check the law for every finite Boolean list, and a separate theorem proves the named witness using the empty list. With the local proof host configured, call:

api_lean_check({
  "sources": [{
    "fileName": "lean-list.bosatsu",
    "source": LINKED_FILE_CONTENTS
  }]
})

The CLI equivalent is yichus lean --toolchain PATH --source lean-list.bosatsu --json, or on Node, yichus lean lean-list.bosatsu --lean-wasm-root DIRECTORY. This translator accepts only its checked structural List[Bool] shape: one direct law check, one direct filled witness, a tail-only self-call, and expressions in its supported grammar. Other recursive shapes, host externals, and finite obligations remain inconclusive. The isolated browser Lean page supports this list shape.

Use an existing theorem to verify an implementation

The complete modular-inverse example defines modular exponentiation, a primality check, and an inverse law in Bosatsu. Its proof connects those generated functions to Mathlib's arithmetic definitions, then applies ZMod.pow_card_sub_one_eq_one, an existing form of Fermat's little theorem. A separate proof establishes the named witness.

Install the optional theorem library beside the pinned native Lean toolchain from a Yichus checkout, then check the source:

node scripts/install_lean_mathlib.mjs /path/to/lean-4.34.0-platform
  yichus lean --toolchain /path/to/lean-4.34.0-platform \
    --source lean-inverse.bosatsu --emit-lean Proof.lean \
    --json --view compact --result FULL.json

--emit-lean saves the generated definitions and theorem goals before verification, including when an author proof is unfinished. Edit the exported lean_proof and lean_witness strings and rerun the command. The author term can use definitions from its package by their names; imported helpers receive distinct generated package namespaces. A saved Lean module is not a verified receipt.

The integer grammar accepts Int or a declared, non-generic product with at least two fields, all Int. Predicates and helpers must be monomorphic, capture-free named functions. Supported operations are integer addition, subtraction, multiplication, modulus, comparison, equality, and Boolean not, and, and or, plus local bindings, conditionals, and input-field projections. Other compiled builtin helpers, including Bosatsu/Char helpers, are outside this translated closure. Destructure products into names, then compare their fields: literal patterns such as case Query(0, 1) require mutable pattern slots and are not admitted. Division, arbitrary higher-order calls, other data types, and mutual recursion are not admitted. Self-recursion requires a top-level zero test of an integer parameter; Lean must prove each recursive call decreases that parameter's toNat. Negative branches retain their Bosatsu behavior. The modulus adapter preserves Bosatsu's divisor-sign convention, including the defined zero-divisor case.

Local MCP uses api_lean_check with the same source file and a configured proof host. A verified result requires elaboration, an approved-axiom audit, source replay, and independent kernel checking of the generated law and witness. It covers every value of the declared input type. Unsupported syntax, failed termination, missing or changed libraries, and timeouts are inconclusive. This optional Mathlib bundle runs on native Lean; browser WebMCP does not yet provide it. The portable Lean runtime and native Mathlib have different pins.

api_access_check on the full four-route Notes API

Source: demos/service/notes-api.bosatsu. Load that file as the source string and call:

api_access_check({
  "sources": [{
    "fileName": "notes-api.bosatsu",
    "source": LINKED_FILE_CONTENTS
  }]
})

The access check holds: the read, write, add, and clear handlers key the owner-scoped table from Principal.user_id, so the owner-key findings hold. This tool does not establish the composite API verdict. Its tool page defines the three access statuses and parameters.

api_verify on full Notes with single-instance topology

Use the same linked source and declare the deployment topology:

api_verify({
  "sources": [{
    "fileName": "notes-api.bosatsu",
    "source": LINKED_FILE_CONTENTS
  }],
  "instances": 1
})

Verification is proven under instances: 1. The add route reads and then writes the same row. With no topology argument, api_verify uses the multi-instance default and reports the read-modify-write and bounded integrity properties as violations. The api_verify page contains an engine-generated request and response for this specimen.

Fixing a read-modify-write with Yichus/Transaction

When api_verify reports rmw-transactions violated and the service really does run on several instances, the fix is a transaction plan, not a topology declaration. The plan reads and writes the table through one named accessor, and the handler maps every outcome:

def stock_rows[s](scope: Scope[s]) -> TxTable[s, Stock]:
  tx_table(scope, "stock")

def reserve_plan[s](scope: Scope[s], sku: String, qty: Int) -> Txn[s, String, Response]:
  found <- tx_bind(tx_read(stock_rows(scope), sku))
  match found:
    case None: tx_pure(Response(404, sku))
    case Some(Stock(on_hand)):
      match cmp_Int(on_hand, qty):
        case LT: tx_pure(Response(409, sku))
        case _:
          _ <- tx_bind(tx_write(stock_rows(scope), sku, Stock(sub(on_hand, qty))))
          tx_pure(ok(sku))

def reserve_txn(db: Db, sku: String, qty: Int) -> IO[Outcome[String, Response]]:
  scope <- transaction(db)
  reserve_plan(scope, sku, qty)

def reserve(db: Db, _: Principal, req: ReserveRequest) -> IO[Response]:
  ReserveRequest(sku, qty) = req
  outcome <- flat_map(reserve_txn(db, sku, qty))
  match outcome:
    case Committed(response): pure(response)
    case Aborted(reason): pure(Response(500, reason))
    case RetryExhausted: pure(Response(503, "retry"))
    case CommitUnknown: pure(Response(503, "unknown"))

The imports are Scope, Txn, TxTable, Outcome, Committed, Aborted, RetryExhausted, CommitUnknown, transaction, tx_table, tx_bind, tx_pure, tx_read, tx_write from Yichus/Transaction. tx_read returns an Option; the route keeps its declared permissions. After the edit the same api_verify call reads rmw-transactions: proven. The guide's section "Atomic commands with Yichus/Transaction" (api_guide with section: "transaction") carries the full contract.

api_access_check on the literal-key Notes variant

Source: demos/service/notes-api-leaky.bosatsu. Load the linked file and call:

api_access_check({
  "sources": [{
    "fileName": "notes-api-leaky.bosatsu",
    "source": LINKED_FILE_CONTENTS
  }]
})

The list_notes handler uses a literal read key, so interpret the expected access:notes result as violated. Calling api_verify with instances: 1 cannot repair that access failure; its composite result remains unproven. See the failed read and the repair in the access diagram.

api_frontend from Notes routes and FrontendSpec

Load the API source above and demos/service/notes-app.bosatsu, which selects list, form, and action views. Then call:

api_frontend({
  "sources": [
    { "fileName": "notes-api.bosatsu", "source": LINKED_API_FILE_CONTENTS },
    { "fileName": "notes-app.bosatsu", "source": LINKED_FRONTEND_FILE_CONTENTS }
  ],
  "instances": 1,
  "transport": "in-process",
  "auth": "dev"
})

Generation should succeed because the composite API verdict is proven at the declared topology and each view matches a typed route. The returned HTML is the same kind of artifact as the deployed Notes App, where the four API routes appear as generated views. The api_frontend reference defines transport, authentication, and route-shape checks.

api_report on ProjectHub

Load the projecthub.bosatsu multi-entity service and frontend specification, then call:

api_report({
  "sources": [{
    "fileName": "projecthub.bosatsu",
    "source": LINKED_FILE_CONTENTS
  }],
  "format": "html",
  "detail": "summary"
})

Interpret the result by checking overview.surfaces for the service, data, and frontend structures, then follow each guarantee's evidence pointer. The ProjectHub App shows the generated frontend artifact for those typed routes. The api_report page defines the JSON and HTML formats and topology parameter.

Follow the inspect–edit–recheck workflow. The connection guide configures browser and Node MCP clients. The full catalog provides every parameter and generated per-tool page.