Hello all. I’ve been learning how to write specifications for smart contracts in act and prove the correctness of the implementation using klab and K framework. I’ll be producing specifications and proofs for SafeMath.sol, ERC20.sol, AccessControl.sol, and others in the process of verifying our system’s code. What’s the best place I can publish these specs and proofs once I’m done so the community can access?
2 Likes
Hi @kirk_tacen,
Welcome to the community 
.
I suggest posting publicly (such as a GitHub repository) and then sharing in the community forum.
I don’t know much about formal verification so look forward to seeing what you share.
For anyone like me without much exposure to formal verification the following looks like a nice introduction by RuntimeVerification:
Thank you @abcoathup, that is a good overview. Runtime Verification is one of the few smart contract auditors who perform formal verification, they know their stuff. I am also doing blog posts following my learning journey if that interests anyone. You can find them on my website. Working on specs and proofs for SafeMath.sol the next couple days (low hanging fruit), which I’ll publish to a public gitlab repository and post here as well.
3 Likes