Ensuring smart contract security

SNAPSHOT

0

DeFi Hacks Prevented

0

Runs/Month

0M+

Solidity Lines Verified

$0B

Protected TVL

Testimonials

“Certora’s technology helped to cover security on decentralized Aave Protocol, essentially finding vulnerabilities that are usually difficult to find in manual code reviews and audits. When building mission-critical software such as financial technology, Certora is a must.”

Read more
JaredFlatow

Stani Kulechov, CEO and Founder of Aave

“Formal verification from Certora is the most powerful tool we have to ensure that we are building a secure, impenetrable system -- the top priority for any serious smart contract developer."

Read more
jeffWu

Jeff Wu, CTO and Co-founder, Notational Finance

“Certora has been a crucial partner along Balancer's journey to ensure excellence in our code quality/security"

Read more
ernandoMartinelli

Fernando Martinelli, Co-founder & CEO, Balancer

“Certora has been a critical security partner in Stakehouse Protocol’s formalization efforts. We are consistently impressed by the team’s hands-on approach and their Certora Prover tool efficacy. It reinforces the key mechanisms while giving clarity and adversarial simulation for our Multichain ETH scenarios.”

Read more
MattShams

Matt Shams, CEO, Blockswap Labs

"Certora gives us so much peace of mind as we develop smart contracts at Syndicate. With formal verification running on every single commit, we can maintain a fast development velocity without decreasing security."

Read more
WillPapper

Will Papper, Co-founder and CTO, Syndicate

“Certora has unlocked TrustToken’s ability to iterate quickly while maintaining confidence in the security of our smart contracts. Our team has discovered and fixed numerous unintended bugs thanks to this powerful tool.”

Read more
YuchenLin

Yuchen Lin, Lead Security Engineer, TrustToken

"Certora has given us the ability to practically apply formal verification methods to anything we do on-chain. They have an excellent team who we've partnered with closely over the years, and the process of writing invariants with them has proven to be invaluable in writing better smart contracts."

Read more
JaredFlatow

Jared Flatow, VP of Engineering, Compound Finance

“The Certora prover plays an important role in our overall safety strategy by providing an accessible way to quickly iterate on formal specifications and determine the correctness of bytecode. It's what we reach for when both time and safety are of the essence. Engineers can learn to use it in a few days and don't need a Ph.D. in formal methods to create good specifications. The tool recently helped us to uncover an inconsistency in an updated version of one of our oldest smart contracts, which was a surprising result. The Certora team is highly responsive and promptly addresses issues we encounter.”

Read more
KurtBarry

Kurt Barry, Protocol Engineer, MakerDao

Protocols

Verification Reports

Education

Webinars & User Guides

Academic Papers

Core Team

Certora Prover builds on 30 years of academic research and hundreds of academic publications which pioneered the area of Formal Verification. The team combines academic leadership, industrial strength and Blockchain expertise.

Advisory Board

our investors

Eli Ben-Sasson

AVIVA GATT

elad Gil

yona Hollander

uri Kolodny

stani Kulechov

moti Rafalin

scott Shenker

balaji Srinivasan

Careers

Digital Marketing/UI designer
Senior Software Engineer
Security Engineer
Community Manager
Technical Project Manager
Senior Formal Methods Engineer
Security Researcher

Remote / Europe

Requirements

MUST

  • 3-5 years of professional design experience from a well known design studio.
  • Strong portfolio featuring examples of performance campaigns
  • The ability to refine other people’s ideas and come up with new ones to create a highly designed visual experience.
  • Experience in building digital assets for acquisition activities
  • Have strong offline/online design skills with extreme attention to details
  • Proficient in Adobe Creative Suite (Photoshop, Illustrator, InDesign)
  • Proficient in Figma
  • Proficient in PowerPoint

ADVANTAGE

  • UI/UX experience- Big Advantage
  • html/css/js/Wordpress – Big advantage
  • Experience working at a business-to-business vendor
  • Bachelor’s degree, or equivalent experience in the graphic design field
  • Videos and/or animations skills (Premiere/After effects)

SOFT SKILLS

  • Ability to prioritize, multi-task and manage work independently to adhere to critical project timelines in a fast paced environment
  • Team player and a strong Collaborator
  • You’re fluent in English, both written and spoken.

Responsibilities

  • Designing all company marketing materials:
    • Offline assets
      • Business cards & office documentation
      • Reports
      • Brochures 
      • Conference assets
      • Other merchandise as required
    • Online assets
      • PowerPoint presentations
      • Email newsletters
  • Implement our refreshed brand guidelines across our products:
    • Our public website
    • Tool report
    • Dashboard 

Contact Us


FAQ

  • Can we use the Certora Prover in our CI pipeline?

    This is exactly the intended use case of the Certora prover!

  • What can be tested or proven using the Certora Prover?

    The Certora Prover provides complete path coverage for a set of safety rules provided by the user. For example, a rule might check that only a bounded number of tokens can be minted in an ERC20 contract. The prover either guarantees that a rule holds on all paths and all inputs or produces a test input that demonstrates a violation of the rule.

  • What cannot be tested using the Certora Prover?

    The problem addressed by the Certora Prover is known to be undecidable. This means that there will always be pathological programs and rules for which the Certora prover will time out without a definitive answer. Our experience so far is that realistic customer’s programs are not pathological and can be successfully analyzed by the Prover. The Certora team is actively working to reduce the number of timeouts when analyzing smart contracts of customers.

  • How does formal verification differ from a traditional security audit?

    A traditional security audit usually involves a manual, holistic review of an entire system. Formal verification, on the other hand, produces a proof that a piece of software satisfies a specification. The Certora team is available for formal verification projects to write specifications and verify the code against these specifications. Often, verification projects find bugs in the code, and these bugs can be fixed during the course of the project, with the fixes proved correct. The team also produces a report describing the properties verified and bugs discovered. At the moment, we only analyze and review Ethereum bytecode.

  • Can we program our own rules into the prover into the future?

    Definitely, and we will assist you and review your rules for free.

  • What are the inputs to the Certora Prover?

    The Certora Prover takes as input the smart contract (either as EVM bytecode or Solidity source code) and a set of rules, written in Certora’s specification language. The Prover then automatically determines whether or not the contract satisfies all the rules. Just as good testing sometimes requires code refactoring, verification occasionally requires changes to the code. For example, because the verification happens via the public API to the contract, some state pieces may need to have getters added so that they are accessible.

  • How do I know that the written rules are correct?

    When the Certora Prover provides a test input that violates the rule, the user can check if this violation is due to a bug in the code or the verification rule. We also suggest performing a sanity check on the rules, e.g., by mutating the contract by adding an artificial bug and checking if any rule is violated. If no violations were found, the specification is missing a rule. The Certora Prover also automatically generates test cases for showing that a point in the program is reachable.

  • What is the technology behind the Certora Prover?
  • How does the Certora Prover differ from existing tools in the market?

    Unlike symbolic execution tools which select specific paths and a fixed set of bad patterns, such as MythX and Slither, the Certora Prover provides complete coverage for a user provided set of rules. Interactive theorem provers such as Coq and K can be used for interactively showing that a specific contract is correct. SMTChecker by the Solidity team and Verisol by Microsoft Research are similar to the Certora Prover in many respects but target Solidity sources with per program user assistance. This makes the tools hard to integrate into the CI pipeline --- the value of the verification is that it allows to move fast and break nothing!

x