Workbench
Lean proofs in this browser
This page compiles the exact Bosatsu source you supply and checks supported
Yichus/Law obligations in a pinned Lean WebAssembly worker. It
registers api_lean_check for an agent connected through WebMCP.
The runtime downloads only when a proof is requested. The page needs browser
shared memory and may reload once to enable its isolated worker.
The result is a source-bound local Wasm run. A verified law passed Lean
elaboration and an axiom audit for its generated law and witness theorems;
the separate native leanchecker replay is not part of this
browser result. Its receipt says independentKernelReplay: false.
Unsupported laws and failed checks are inconclusive.
Bool example · List example · Full API workbench
Preparing browser isolation…
Where this fits
What this is about: Checks and Proofs