I heard great things about Certora. If you search the ubiquity org for me writing the term "Certora" you can see that I listed a security checklist with a lot of what you filed issues for.

I heard great things about Certora. If you search the ubiquity org for me writing the term "Certora" you can see that I listed a security checklist with a lot of what you filed issues for.

I guess you mean this topic: #197

This issue doesn't include only 2 topics you mentioned at #197:

• bug bounty program
• incident handling

Regarding the bug bounty program, we have an implicit rule (which we applied at least 2 times) to reward 10% of the funds at risk. So I think a simple mention of bug bounty program somewhere at https://ubq.fi/ is enough, without going into details of severity, possibility, etc...

Regarding the incident handling, all of the tutorials that I read goes simply to:

1. Pause contracts
2. Find the root cause
3. Fix the root cause

The most important is step 1 which pauses contracts. If it is not on time then all other mitigation steps don't make sense. So a separate incident response tutorial seems to be a low priority issue right now.

I heard great things about Certora. If you search the ubiquity org for me writing the term "Certora" you can see that I listed a security checklist with a lot of what you filed issues for.

Certora is closed sourced and has a pretty steep learning curve. I've had great experience using https://github.com/a16z/halmos which seems to be the most user friendly out of all of the tools.

They asked me to schedule a call with them. I am under the impression that we can bring on one of their engineers to implement things.

If you're interested I can consider your availability before booking

https://calendly.com/d/444-zpr-54m/30-minute-meeting

They asked me to schedule a call with them. I am under the impression that we can bring on one of their engineers to implement things.

If you're interested I can consider your availability before booking

https://calendly.com/d/444-zpr-54m/30-minute-meeting

Of course they asked for a call since they need to sell the product. Certora is a proprietary paid "formal verification as a service" company. They bring on one of the engineers since the product is really complicated. I'd rather use one of the open-sourced solutions and have one of the core team members to solve this issue in order to keep the context/knowledge in Ubiquity DAO instead of outsourcing solving this issue.

Still an active issue?

Still an active issue?

Yes

/start @Keyrxng

/start @Keyrxng

@gentlementlegen like I suggested please revert the code since start is broken

/start

@0x4007 should be good to go for now hopefully.

@sushant-rumsan, @Keyrxng, this task has been idle for a while. Please provide an update.

/start

@alexandr-masl

Basically we have 2 invariants that should be proved (one, two). In some cases formal verification is not possible if there're too many code paths to prove. Not sure if https://github.com/a16z/halmos or https://docs.runtimeverification.com/kontrol are able to prove that invariants.

@alexandr-masl

Basically we have 2 invariants that should be proved (one, two). In some cases formal verification is not possible if there're too many code paths to prove. Not sure if https://github.com/a16z/halmos or https://docs.runtimeverification.com/kontrol are able to prove that invariants.

Hey, thanks for pointing this out. I'm currently researching all the presented solutions to find the one that fits best. I'll keep you updated on my progress

start

start

/start

/help

Available Commands

/wallet 0x0013f4217f6a8B48A92f7EA5d811A5F8D8364B93

/start