A proof system in Lean for LC3 Programs, following the article Write your Own Virtual Machine.
The purpose of this is to build formal verification tooling for a low-level Lean-based VM, in Lean.
Clone this repository and build the project.
lake build
This will give you a binary .lake/build/bin/lc3-lean
Run an assembled program, e.g. 2048:
.lake/build/bin/lc3-lean programs/2048.obj
If you add path-to-dir/.lake/build/bin/ to your PATH you can simply run
lc3-lean programs/2048.obj