|
|
|
|
|
|
by DoubleDecoded
670 days ago
|
|
|
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. |
|
|