Workbench
Yichus / Program workbench
Analyze a Bosatsu program
Load or edit a program, check its database access, draw its dependencies, and run a function on chosen inputs. The tools run in this browser.
01 / Check the source
Check the program’s access rules
The example stores each user’s notes under their own key. Compile it, then run its checks. Make leaky replaces that key with a shared one so you can see the access check fail.
Edit the source, then compile again before checking it.
Work with your agent
WebMCP connects your agent to this page. Connection and tool instructions. Use yichus_page_feedback to read the current editor and displayed feedback. Start with api_guide, compile your sources, run the relevant check, and inspect its scope and evidence. After opening a generated app, use yichus_app_act to fill and submit its visible form, then yichus_app_feedback to read what the user sees. yichus_app_call makes a headless request without changing the visible form.
Engine still loading.
How to read a verdict
proven means no applicable property is violated or blocked.
Read the property details: warnings and assumptions can still qualify the result.
inconclusive means the check did not settle the question. A blocked property was not established because its check could not run or finish. Warnings can include bounded evidence or deployment assumptions; the composite flag is not an unconditional proof of the application.
02 / Explore the structure
Draw definitions and dependencies
Browse packages and checked types, then follow a definition's direct users and dependencies. A shared type does not prove shared behavior or an access policy. Switch to the full map to see every dependency at once. In that map, follow a definition’s arrows down to the definitions it uses. Layer 0 has no dependencies on other user definitions; higher layers depend on definitions below them. Select a card to try that definition in the evaluator. How these facts are generated and checked.
No map yet. Choose Draw the program to explore the source above.
The full map's arrows point to user-definition dependencies. Card sizes fit their labels; numerical details are under All measurements. Browse groups for large programs, or scroll sideways through the full map. Platform primitives and access-policy guarantees are outside this edge set.
All measurements
See the stack by type family
The stack groups definitions by layer and type shape. Wires join each
definition to the ones it uses. The engine produces this same picture for
the browser and yichus organize stack --svg.
No picture yet: run api_organize with lens stack.
03 / Evaluate a definition
Run a function on chosen inputs
Select a map card or enter a binding below. Seed inputs, edit their values, then evaluate to see the output.
Static fact Holds for every input.
Observed Seen in seeded runs: bounded observation, not proof. An unchanged result does not prove independence.
Save a CLI run with --record and open it here, or copy this run back to the CLI. Follow a complete replay example.
No evaluation yet. Choose Seed inputs to start.
output:
04 / Run the app
Run the generated application
A connected agent can open a generated app here with
yichus_app_open. You can use the same app while the agent
tests its routes, stored data, and recovery after a crash.
The app’s engine, data store, and test token issuer run in this tab.
Where this fits
What this is about: Safety and Permissions