search

GaloisInc / formal-verso

Formal Verification for Soroban
BSD 3-Clause "New" or "Revised" License
1 stars 0 forks source link

[contract] Verify Auth #2

Open scuellar opened 3 months ago

scuellar commented 3 months ago

The example contract for Auth is described in the Soroban tutorial and the code can be found here.

rperoutka commented 2 months ago

I added the start of a verification script for the Auth contract in auth.saw. I had to add bits for the AddressObject type to soroban.saw to enable creating a fresh variable of type Address for the spec. Verification currently fails when symbolic execution attempts a call to Address::requireAuth.