Archived Yichus Demo Route Index

This is the compatibility archive for older and specialist demo URLs. Use the current site landing page for the maintained product routes. The groups below identify what each archived hub contains and where to find its explanation.

Runnable UI, simulation, and benchmark routes

Run the compiled counter, browse generated calculators, or open the update-enqueue throughput benchmark. The runnable route map connects those examples to their commands and mechanism-level documentation.

Static analysis and API verification routes

Open the Explorer playground to edit Bosatsu and run browser analysis operations such as overview, path, trace, and query; a result can narrow the next operation.

Read the Explorer guide for typed-IR operations, query programs, and setup links.

Read the trace-boundary page to separate multi-file static analysis over fully typed, pattern-match-compiled IR from the trace view's static expression graph for only the first loaded file. Neither view records runtime events.

Open the service fixtures and Notes API page for working Notes routes, verifier links, and the limits of the smaller fixtures.

Bounded verification and admission routes

The interleaving checker demo explains typed-IR extraction, the author-supplied mapping from each implementation write to a modeled transition, and three-valued verdicts; that mapping is declared, not verified. The batch admission demo explains balance ranges computed from admitted debits and credits, then checks their endpoints to cover every operation ordering. Policies that do not fit those ranges use a search that enumerates concrete orderings only up to an operation cap and reports inconclusive when the cap is exceeded. The page also shows replay verification of the chosen ordering.

Time Travel generated game and renderer fixtures

Play the Time Travel puzzle for the full generated game surface.

Open the Time Travel stepper for the deterministic rules fixture.

Open the Grid smoke test to inspect the reusable grid renderer.