emd: A Language of Eight Unicode Dashes and How Far It Can Be Verified

emd programs use eight Unicode dashes and 32 instructions. We define the language in Lean 4 and Rocq, proving encoding round trips, run determinism, step invariants and independence from line layout. A direct Turing-machine simulation proves universality using 11 instructions, preserves the final tape and never faults. In Lean we also prove a model of the 64-bit machine a refinement of the semantics, correctness of a mirror of the compiler in both directions, and soundness of a mirror of the static analyzer. These results concern models. Kani checks the Rust VM and CBMC its generated C, within stated bounds. The VM is compared with the models on finite cases, and the generated C with the VM; no proof connects the implementation to the models. A compiler written in emd compiles itself.