Atlendis Protocol Audit by Runtime Verification

Introduction

After publishing the Atlendis protocol V1 whitepaper, Atlendis Labs is excited to announce the completion of the Atlendis protocol’s smart contract audit conducted by Runtime Verification.

Atlendis Labs engaged Runtime Verification early in the development process to get feedback on its smart contracts’ design and once the code was finalized, the formal review began. The scope of the audit included all the smart contracts of the protocol, in particular the main pool from which borrowers take loans, and the NFT position contracts that represent lenders deposits.

Audit context and report summary

Security is a focal point for the Atlendis Labs’ development team. It was also clear from the beginning that a third-party would then review and test-proof the Atlendis protocol’s smart contracts, ensuring a high standard of security for lenders and borrowers.

Runtime Verification was charged with this task and the audit was conducted from January 10th, 2022 to February 18th, 2022.

First, the auditors read and analyzed the documentation and whitepaper to understand the theory and underlying logic of the protocol.
Then, they rigorously reasoned about the business logic of the contract, mapping features to the code and validating security-critical properties to ensure the absence of loopholes in the business logic and inconsistencies between the whitepaper’s described functionalities and the code implementation.
Finally, during the proofing and testing phase, the auditors proceeded to check if the code was vulnerable to Runtime Verification’s known security issues, and they verified some properties of the arithmetic library with the Coq proof assistant.

The Runtime Verification team found that “the code is generally well written and thoughtfully designed, following best practices.”

Some issues have been identified, regarding implementation flaws and potential security vulnerabilities, which the Atlendis Labs team addressed. The audit team also made a series of suggestions on input validations, gas optimization and code readability.

The report also thoroughly addresses external vulnerabilities surging from token integrations.

Finally, because replicating real-life usage conditions is almost impossible and manual code review cannot guarantee to find all possible security vulnerabilities, the Atlendis Labs team will shortly announce its Bug Bounty program for the community to take part in perfecting the protocol’s security.

Atlendis Labs would like to thank the Runtime Verification team for their insightful feedback and suggestions that have helped improve the Atlendis protocol. The Atlendis Labs team hopes to be engaged in a long-term relationship with Runtime Verification and looks forward to working together again in the future, to advance the development of the Atlendis protocol.

About Atlendis

The Atlendis Labs team recently published the whitepaper of the Atlendis protocol V1, revealing the theory and rationale behind the Atlendis protocol to the community.

Atlendis brings uncollateralized crypto loans to institutional borrowers, through an innovative and capital-efficient DeFi lending protocol. Similarly to a revolving line of credit, the Atlendis protocol allows entities to borrow, i.e. issue bonds as many times as they need, up to a preset borrowing limit, without any collateral. The borrowing rate is discovered via a limit order book specific to each borrower. The rate is fixed at borrowing time and does not change throughout the duration of the bond. It can however differ from one bond issuance to the next. The funds are not shared among borrowers and liquidity providers choose their own lending rates, therefore, liquidity providers are only exposed to their chosen borrowers and keep ownership over their investment profile.

About Runtime Verification

Runtime Verification Inc. is a technology startup based in Champaign-Urbana, Illinois. The company uses formal methods to perform security audits on virtual machines and smart contracts on public blockchains. It also provides software testing, verification services and products to improve the safety, reliability, and correctness of software systems in the blockchain field.

What’s next

The Atlendis Labs team is happy to host Runtime Verification for a community call and AMA that will touch base on the audit report and the Atlendis protocol’s security on March 29th at 3pm CEST. Join the Atlendis’ Discord to find more information and engage with the team. Receive a calendar invite here.

Also, now that the audit of the Atlendis protocol’s smart contracts is completed, the smart contracts’ code has been open sourced and is hosted on the Atlendis Labs’ GitHub. The launch of Atlendis Labs’ Bug Bounty program is therefore the logical next step and will be announced shortly. Subscribe to Atlendis Labs’ newsletter to be informed as soon as it launches.

Additional resources

Atlendis Protocol Smart Contract Audit Conducted by Runtime Verification is Completed