1.3 KiB
1.3 KiB
Intro
- Formalland 2 years old
- Formal verification for code, proofs
- Find a way to fully specify smart contracts
- Formal verification as means of security (no bugs -> no stealing)
- Alternatives include:
- Testing (Unit, Value)
- Human expertise
- Quite niche in the field of computer science
- Alternatives include:
- We can be sure that the program follows intended behavior after verification
Smart contracts
- Notion of users
- Admin - owner
- We need to look through some examples here to get a feel for them.
- Motivated by bugs listed here
Example of Smart Contract
- Stablecoins (USDC)
- Possible specification(?) is to state that the amount of coins is fixed
Work
- Solidity
- VSC online
Questions during the meeting
-
What is the difference between a user and an admin in the context of smart contracts?
-
You mentioned that one possible specification is to state that the amount of coins is fixed. How does that relate to formal verification? To our project?
-
Is the idea to design a DSL? Could you elaborate on the specifics? Do you have a write-up about it or do we need to come up with it?
Yes. We want to simplify formal verification of smart contracts by creating a DSL.