This page describes what emath treats as untrusted, the defenses in place today, the defenses planned for later stages, and how to report a problem.

• .emath files, and the files and libraries they use.
• Values given with --set.
• Receipts read back by emath resume, and run folders (.dream/NAME/) read back by emath dream resume, fork and watch.
• The Rust that emath native generates and builds with rustc, and the Lean that emath export lean --check hands to Lean.

• No outside effects from a file. An .emath file can compute, show and check. It reads only the .emath files it uses, and cannot run commands, open the network, or write files.
• Bounded runs. The interpreter counts its work in engine steps and stops a line at the work limit (100,000,000 steps unless a file raises it), and a definition nested past 10,000 calls stops with a message instead of crashing.
• Refusal instead of guessing. A step that cannot be done refuses with a reason instead of giving a wrong answer.
• No hidden code paths. Mathematics is written in emath; the engine does not dispatch on subject names.
• Sealed records. A --json receipt and every line of a dream journal carry the SHA-256 of the engine and of every file read, and a seal. emath resume and emath dream resume refuse when the record, the engine or any file it read has changed.
• Guarded writes. emath dream refuses to start a run under a name that already exists. emath fmt does not make a change that would alter more than spaces.
• Determinism. A run gives the same answer every time, so a result can be reproduced and audited.

emath native runs without the work limit: a line runs until it ends. It builds and runs a program on your machine, so treat a file you run natively like any other code you compile and run.

These belong to later stages and are not implemented yet:

• Content-locked package resolution for package publishing.
• Sandboxing for bridges to outside solvers.

Please do not open a public issue for a security problem, and do not post exploit inputs publicly. Contact the author (Aditya) privately with a description and a minimal reproduction. A dedicated reporting address and disclosure policy will be published before the first public release.