Projects that are audited with CertiK undergo a rigorous security assessment are delivered an audit report which details the full scope of project risk and vulnerabilities. We publish the results of the security assessments in our Code Audit History module.

The Code Audit History module contains all the audit reports that are available for a project. The module includes the status of a project’s audit findings (unresolved, acknowledged, partially acknowledged, resolved) alongside the severity of the findings. You can determine whether a project is taking actionable steps to address the results of its audit.

A “View Findings” option is available, which makes it quick to retrieve audit findings. “View Findings” presents only the code-level audit findings, allowing you to quickly reference these findings without having to parse through the full report (which is still available through the “View PDF” option).

Security risks are categorized based on their severity level and are defined in the following ways:

• Critical: Critical risks are those that impact the safe functioning of a platform and must be addressed before launch. Users should not invest in any project with outstanding critical risks.

• Major: Major risks can include centralization issues and logical errors. Under specific circumstances these major risks can lead to loss of funds and/or control of the project.

• Medium: Medium risks may not pose a direct risk to users funds but they can affect the overall functioning of a platform.

• Minor: Minor risks can be any of the above but on a smaller scale. They generally do not compromise the overall integrity of the project but they may be less efficient than other solutions.

• Informational: Informational errors are often recommendations to improve the style of the code or certain operations to fall within industry best practices. They usually do not affect the overall functioning of the code.

We have recently extended our state-of-the-art Formal Verification results into Skynet project profiles. Projects that have undergone formal verification will now be identified with a “Formal Verification” tag, and there will be a section within the Code Audit History module that provides users with detailed information on a project’s formal verfication results.

Formal Verification is a rigorous methodology for verifying the correctness of smart contracts using mathematical algorithms and logic. This process involves analyzing source code, formalizing it into logical assertions, and then proving that these assertions hold within the given context and constraints of the code.

The formal verification section within the Code Audit History module contains a tooltip that explains the formal verification results:

True: Automated formal verification (symbolic model checking) proves that well-known functions in the smart contracts adhere to their expected behavior.

False: Automated formal verification (symbolic model checking) proves that well-known functions in the smart contracts do not adhere to their expected behavior.

Inapplicable: The specification of the property is too generic and does not accurately capture the intended behavior of the smart contract.

Inconclusive: The model checking engine fails to derive a conclusion regarding the property's validity.

You can also click on “Formal Verification Details” to examine detailed information about the finding, and find the complete Formal Verification results in the Audit Report.

With the growing importance of secure and reliable smart contract deployment, CertiK's Formal Verification service offers valuable assurance for crypto projects and communities looking to improve their reputation and build trust with their users. By utilizing formal verification, projects can reduce the risk of vulnerabilities and exploits, and ensure the highest level of security and trust.

To learn more about how CertiK is enhancing trust, transparency and security in the Web3 space with Formal Verification, you can refer to our collection of blog posts on formal verification at CertiK Resources.