Idea
Project / Application checks
Check application rules against the program.
An API can pass its tests and still read the wrong user’s data or break an account balance when requests overlap. Checking these rules requires considering paths and combinations of requests that individual test cases may miss.
Tests exercise chosen inputs. Yichus also analyzes programs compiled from Bosatsu, a typed functional language, to check declared rules independently of the agent’s summary. Its access checker reasons about supported database operations across requests; other checks explore bounded cases, sample inputs, or prove a translated theorem.
Read the scope beside each result: holds, violated, or could not decide (the tools use different labels). An incomplete search cannot pass. An access violation can mean a guard was not proven, without demonstrating a leak. A pass covers the stated property and assumptions, not the whole application.
Use them to gate an agent’s changes in CI, to let the agent check its own work as it goes, and to check an agent’s report against the program.
Try itThis Notes API reads a fixed user’s notes. Press After the fix to compare the repair: reading the caller’s notes instead.
Loading the recorded access check. Read the Notes example.
Code & run Run the handler, check access, and compare the fix
Read the source: the version with the bug · the fixed version
Other verifiers answer questions like these:
- Protocol check: explore compiled handlers under declared requests, retries, and fault bounds.
- Distributed-systems check: explore a declared model’s message schedules and crashes within stated bounds.
- Law check: test sampled inputs or exhaust a declared finite domain. Lean proofs establish the translated theorem for supported shapes.
- Claim check: compare supported structured claims with program evidence.
These build on established model checking, property-based testing, and Lean proofs.
Choose the property you need to check
Safety and permissions develops the ownership example into guards and role-protected routes. Checks and proofs separates sampled tests, finite checks, and Lean proofs. The distributed-systems checker explores declared message schedules and faults.
These tools consume Bosatsu programs and explicit declarations. They report their assumptions and unsupported cases; they do not certify an entire deployed system.
All Yichus projects · Work with your agent