DoubleDecoded

Thanks for showing Register state and flags. Is this all instructions?

"could break the guarantees" is a weak guarantee then.

https://github.com/andrew-johnson-4/lambda-mountain

Working on verifiable correctness for programs written in LM or anything that generates annotated assembly. Basically low-level proofs that accessed memory is valid and live or that function pre/post-conditions are met.

The goal is that these proofs are compiler agnostic, so more people can use them.