Back to all stories
Case Study
CertiK’s Audit Synopsis of Taxa Network’s Smart Contracts
CertiK’s Audit Synopsis of Taxa Network’s Smart Contracts

In June 2019, we announced our partnership with Taxa Network. Taxa Network is a privacy-preserving, computationally powerful, highly developable, blockchain agnostic layer-2 infrastructure.

While scalability is a major pillar for blockchain projects, many have learned that TPS speeds aren't the only answer to facilitating adoption. To make blockchain infrastructure massively usable, there’s much to be done with its middleware to address its ability of handling complex business logic featuring intensive computation and heavy data, while ensuring a reasonable level of privacy.

Leveraging the state-of-the-art privacy technologies, Taxa aims at becoming the universal logic layer of the layered blockchain infrastructure that enables computationally-powerful, privacy-preserving, highly-developable applications for all, and enabling real-world deployment of trustless technologies to develop and thrive.

Audit Synopsis

CertiK worked closely with the Taxa team to audit the design and implementation of theTaxaToken and TaxaLockFoundation smart contracts. The auditing process paid special attention to the following considerations:

  1. Testing the smart contracts against both common and uncommon attack vectors.
  2. Assessing the codebase to ensure compliance with current best practices and industry standards.
  3. Ensuring contract logic meets the specifications and intentions of the client.
  4. Cross referencing contract structure and implementation against similar smart contracts produced by industry leaders
  5. Thorough line-by-line manual review of the entire codebase by industry experts.

During the audit process, CertiK’s smart label applied 100% formal verification coverage on the source code. Unlike manual security checks, Formal Verification examines the entire code logic at-scale and mathematically ensures your program works only as it’s intended to. To do that, the process thoroughly checks your program by calculating it against every possible value for all variables -- making it completely air tight.

Overall, CertiK found Taxa’s smart contracts to be structurally sound and not vulnerable to issues including integer overflow, functional incorrectness, buffer overflow, and others. Check out the full audit report here!

CertiK looks forward to continuing working closely with Taxa in the future!

About CertiK

CertiK leads blockchain security by pioneering the use of cutting-edge Formal Verification technology on smart contracts and blockchains. Unlike traditional security audits, Formal Verification mathematically proves program correctness and hacker-resistance. CertiK was founded by Computer Science professors of Yale University and Columbia University, securing over $5B in assets, including many of the world’s top projects.

The research efforts of CertiK have received grants from IBM and the Ethereum Foundation, and notable investors include Binance Labs, Bitmain, Lightspeed Venture Partners, Matrix Partners, and NEO Global Capital, among others.

To request the audit/verification of your smart contracts, please email [email protected] or visit to submit the request.