CertiK is proud to have successfully completed the audit of the ****Paxos PAX Gold (PAXG) project — the first tradeable, regulated token backed by physical gold.
Using a variety of intensive auditing techniques, including our industry-leading Formal Verification process, we’re proud to highlight PAX Gold as a more secure, safe, and protected asset — one that furthers Paxos’ goal of creating a global, frictionless economy.
Paxos’ tokenization of gold marks an expansion of its expertise in creating fiat-backed stablecoins. PAX Gold is backed by gold itself — one fine troy ounce of the highest quality of gold — ensuring that these funds are stable and democratized across countries and currencies.
By digitizing gold, Paxos does what currency was created to do — creates a clear, transparent and liquid way to move value.
Building on the success of their PAX stablecoin, PAXG goes further. With the gold market famously complex and high-barrier for users, PAXG democratizes access to gold in a fluid, decentralized way.
Like any other cryptocurrency, PAXG can move instantaneously, and unlike other crypto assets, PAXG is stable and backed by a physical, redeemable asset.
As a financial tech firm bridging the blockchain world to the world of traditional finance, Paxos occupies an important role. To ensure the safety of their project, and the security of their new asset, Paxos selected CertiK, the global leader in blockchain security, to ensure the success of their project.
What We Did
CertiK provided the audit review for PAXG, identifying and solving the most difficult-to-detect anomalies before launch and proving safety at a high-level.
As the world’s most advanced formal verification technology for smart contracts and blockchain ecosystems, CertiK is the leading cybersecurity firm, offering a Formal Verification audit process.
Unlike manual security checks, Formal Verification examines the entire code logic at-scale and mathematically ensures the program works only as it is intended. To do that, Formal Verification thoroughly checks the program by calculating it against every possible value for all variables.
Formal Verification attempts to prove or disprove that the intended algorithms, protocols, or business functionalities are correct — or unable to run incorrectly. Rather than depending on error-prone human judgment, mathematical systems calculate against near-infinite scenarios. By applying rigorous and complete mathematical reasoning against code, Formal Verification goes wider and deeper than any manual team can go alone.
Ilan Gitter, Senior Software Engineer at Paxos, commented, “By having our PAX Gold smart contract audited by CeriK, we were able to receive an extra layer of assurance on our code. Their formal verification process is thorough and robust, meaning that every eventuality was tested and Paxos can be confident in the security of the PAX Gold smart contract.”
The Results
Unlike other security companies, CertiK utilizes Formal Verification to conduct a multi-pronged approach that results in a full, holistic, and comprehensive security audit. By utilizing CertiK’s Formal Verification Platform, Static Analysis, and Manual Review, the CertiK team applied a comprehensive examination to the PAXG project.
CertiK used the following sources of truth about how PAXG should work:
- Client’s Projects README Files
- Previous Audit Reports
- Test Scenarios (PAXG provided high-coverage unit tests to simulate possible scenarios)
- Paxos Github Code Base
- Paxos Standard Token
The results and solutions presented by the CertiK team were implemented by the Paxos team for a safer, stronger product. We found, compared to the current PAX smart contract, the PAXG contract introduces:
- An additional fee logic, where the fee rate can be controlled by the feeController role.
- Support for delegate transfer, which enables transfer by transactor on behalf of the investor with consent from the investor (in the form of signature, where the signed message is associated with transaction details such as recipient, value, etc).
- An option for a transactor to charge the investor a certain amount of service fee.
Such a project requires the utmost in security protocols. To that end, PAXG ensures the use of sequence numbers and deadlines to prevent the signature from being abused. With the delivery of the audit report, CertiK concluded that the contract is not vulnerable to any classically known anti-patterns or security issues. PAXG received an exceptional 98% on its audit report.
CertiK would like to congratulate the Paxos team for passing the rigorous verification process of PAXG and wishes them luck on the success of their project.
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 audit@certik.io or visit certik.io to submit the request.
Twitter: https://twitter.com/CertiKCommunity
Reddit: https://www.reddit.com/r/CertiKOrg/
Telegram: https://t.me/certikorg
LinkedIn: https://www.linkedin.com/company/certik
