Smart Vault: Implement prover rules #103
Conversation
facuspagnuolo
changed the title
facuspagnuolo
changed the base branch from
master
to
authorizer/implement_authorizer_rules
facuspagnuolo
changed the base branch from
authorizer/implement_authorizer_rules
to
master
lgalende
changed the base branch from
master
to
authorizer/implement_authorizer_rules
lgalende
changed the base branch from
authorizer/implement_authorizer_rules
to
master
…n-envfree summaries
facuspagnuolo
changed the base branch from
master
to
authorizer/implement_authorizer_rules
lgalende
force-pushed
the
smart_vault/implement_smart_vault_rules
branch
from
f533892 to
bedaf26
Compare
…to smart_vault/implement_smart_vault_rules
|
Once the job is completed, the results will be available at https://prover.certora.com/output/50838/6d545a11459f4c9ab688c82d377a5ebe?anonymousKey=28fe67d6613a80827ee20a959bb54dbdab1f975e |
|
Once the job is completed, the results will be available at https://prover.certora.com/output/50838/a0c79f741bbc407d86daa38fddbaf02e?anonymousKey=0b5a743314776a55c567732b856ff934334eef5e |
|
Once the job is completed, the results will be available at https://prover.certora.com/output/50838/8d112f7488fa4c41bf6617eee5093b6c?anonymousKey=56e8a8897da438317be4e24d5bd5993ba7080829 |
|
Once the job is completed, the results will be available at https://prover.certora.com/output/50838/b57d5bd734554b3cb28e28837c2e430f?anonymousKey=2a7d9d4d182e225c20f5bdbab9ddfc5c2f3ba42e |
|
Once the job is completed, the results will be available at https://prover.certora.com/output/50838/b8748a2a8d454771bb152a2b89a68e13?anonymousKey=34b726abf22868d9a1b2343bfcaf16d1601ed813 |
This PR adds rules written in CVL2 in order to formally verify the SmartVault contract by making use of the Certora Prover.