Formal Verification SPEEDRUN | It's TOO easy, with Halmos, Kontrol, and Certora

[@frackinfamous6126]

LFG sir! This is going to be a fun one.

[@mentasuavesuave01]

Clear and direct to the subject. Thanks Patrick

[@rikanghuang7714]

Learning formal verification this way is so hilarious aahahaha

[@PatrickAlphaC]

Makes it a bit more approachable yeah?

[@parameshvar9857]

Cyfrin my dream job!!!

[@jimmybaker4821]

Formal verification is way too hard tho and it barely works. Like certora prover is so hard to even write tests for. And halmos tests fail for like 90% of tests coz it doesnt bave any of the cheatcodes.

[@PatrickAlphaC]

We will make it easier. We must

[@bruidbarrett]

Which is the best then?

[@tilakmadichettitheappdeveloper]

Hello Patrick ! I didn't quite what was being explained this video. I was under the assumption that formal verification means 3rd party websites like etherscan will recognize that a given s.c belongs to whatever contract address it's deployed to. This video seems quite out of context. Is it part of a bigger video that I can watch ? Thanks, Tilak

[@PatrickAlphaC]

Ahh, good question! So the terms are confusing: Verified on etherscan: when you deploy a smart contract and confirm the bytecode matches solidity Formal verification: turning code into math prove your codebase does one thing. We have a video on this earlier in my KZbin. This video was just a speedrun of using popular formal verification tools

[@tilakmadichettitheappdeveloper]

@@PatrickAlphaC oh thank you very much for explaining ! I have another question.... slightly unrelated.. You talked about nonce being the latest transaction count for a given account in the matter part of your foundry course.but in the beginning you had a whole demo on nonce being something the node runner has to crack (or solve) to demon's proof of work....so which one is it ?

[@mbharatm]

The two nonces referred to are totally unrelated. Nonce literally means number used once as a unique counter. The same term pops up in different contexts. HTH

[@tilakmadichettitheappdeveloper]

@@mbharatmOkay thanks for clarifying

[@PatrickAlphaC]

@@tilakmadichettitheappdeveloper yeah nonce is a confusing term, because it has slightly different contexts depending on when you use it. The general definition: a number only used once. For proof of work chains, this is the “answer” they try to crack. The nonce is a number used once for the block. For wallets, the nonce is essentially the “transaction count” of the wallet, and can only be used once. In both cases, it’s just “a number only used once”

[@rikanghuang7714]

I was learning formal verification hahahaha

[@pedrogorilla483]

You said it was too easy…

[@PatrickAlphaC]

Well… once you get through all the bullshit it is

[@fakemonkgin]

waiting for cyfrin security part2