33 lines
1.3 KiB
Markdown
33 lines
1.3 KiB
Markdown
## 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
|
|
- 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](https://formal.land/docs/tools/coq-of-solidity/specification-project) to get a feel for them.
|
|
- Motivated by bugs [listed here](https://github.com/kadenzipfel/smart-contract-vulnerabilities)
|
|
|
|
### 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. |