This artifact contains the complete mechanized Coq proofs of the lemmas and theorems about System DE. The VM image is preinstalled with the dependencies required to build and verify the Coq development. No special hardware is required to build and validate the proof scripts as long as the host machine has 4 GiB of memory available to run the VM.