What on monogate.dev you can re-run yourself, with the commands to do it, and what you cannot, because it runs on a private repository.
python3 -m venv .venv . .venv/bin/activate pip install monogate-forge eml-compile --version
That installs the newest monogate-forge release on PyPI. Before each deploy the site installs the same release and runs every compile command it shows against it, so the lessons are checked against what you have, not against unreleased source.
Save this as clamp_demo.eml. Its contract says the result never exceeds limit. The Lean target needs @verify(lean); the Verilog target needs @target(fpga).
module clamp_demo;
@verify(lean, theorem = "clamp_demo_bounded")
@target(fpga, clock_mhz = 100)
fn clamp_demo(request: Real, limit: Real) -> Real
requires (limit > 0.0)
ensures (result <= limit)
{
min(request, limit)
}eml-compile clamp_demo.eml --profile-only eml-compile clamp_demo.eml --target python -o clamp_demo.py eml-compile clamp_demo.eml --target c -o clamp_demo.c eml-compile clamp_demo.eml --target verilog -o clamp_demo.v eml-compile clamp_demo.eml --target lean -o clamp_demo.lean eml-compile clamp_demo.eml --allocate
Each command writes one file, or prints a profile or a resource plan. The site's command check runs all six in an empty directory holding only the source above and requires each to exit 0. It does not compare what they print.
clamp_demo.lean states the theorem clamp_demo_bounded. Whether Lean accepts its proof is a separate step: it needs MachLib, the Lean library the theorem is stated against, and #print axioms. Level 1, Lesson 4 shows the commands and how to read the answer.
Four checks run before each deploy, from scripts in the public monogate-dev repository. They are not scheduled, so a result can change between deploys without the site noticing.
scripts/check_site_commands.mjs): every compile command on the site, run against the newest monogate-forge on PyPI beside the source its page shows. A command whose source the page does not show is checked for argument errors only. Only the exit status counts; printed output is not compared.scripts/check_site_figures.mjs with scripts/site_figures.json): each registered number against what measures it (machlib's README count, the lesson counts, the SuperBEST totals and operator lists in the monogate library). Figures and tables this site only repeats (the /superbest node-count tables, operator count and savings estimates, and T42-QCC's equation count) are compared with monogate.org's data, cell by cell for the tables, which does not make them measurements. Phrases retired as false must not come back. A number that is not registered is not checked.tools/lean_claims/check_claims.py with scripts/lean_claims.json): every registered theorem must be declared at its pinned machlib revision, compile, and have no sorryAx in its #print axioms. That covers the cost-theory table on /superbest and the forward-error theorems the Electronics Lab cites. machlib and monogate-lean are public, so this check needs nothing private.scripts/check_lesson_proofs.mjs with scripts/lesson_proofs.json): each lesson line that gives a theorem's verdict, proved or not, is re-derived. The page's own Lean command runs on the page's own source with the same PyPI compiler, the emitted file is compiled against a committed MachLib checkout, and #print axioms must agree with the page, including any report the page quotes. MachLib is public, so this check needs nothing private either.SOURCE.json summary, and no check here re-reads a capture. The Lean theorems its certificates cite are in machlib, and the Lean-claims check compiles those.