Type a program. The trust & effect checker proves — live, in your browser — exactly what the code is allowed to do, and refuses anything that lies. The whole checker runs client-side (Pyodide) — no server, nothing leaves your tab.
Booting the checker…