First 6502 program "proven" "correct". All memory locations are currently unbounded integers and massive holes in the implementation but the VCG works!
Conversation
Will you be putting this online when you are done? I will admit I went to your Github yesterday hoping it would be there! Curious to see how you are doing stuff, as I have attempted to do something similar in Lean 4, but didn't end up making much progress!
1
1
Yes, it will be public eventually.
2