
Institutional Finance

Engineers' Hub
Deep dives, implementation guides, research, and real-world verification insights for engineers working on complex software.
Better softwareA more open world

Institutional Finance

Smart Contract Security
This article presents two complementary methodologies for threat modeling: Certora's "4 A's" framework and the STRIDE framework. Soroban smart contracts teams who invest in this essential process early will lay the groundwork for security, resulting in simpler architecture, fewer bugs, and faster audits.

Smart Contract Security
We provide a roadmap for Stellar smart contract builders to prepare for a security audit through the Soroban Security Audit Bank. By designing for security, writing clean & tool-friendly Rust code, rigorously testing, and running security tools beforehand, projects can be well-prepared. Be audit-ready so your project gets a faster, deeper, and more valuable security review.

Smart Contract Security
How to design Solidity smart contracts that are easier to formally verify.

Smart Contract Security
Our experience formally verifying Rust smart contracts for Soroban and Solana has helped us identify what makes a Rust smart contract easy or difficult to verify. This blog post shares five best practices distilled from our observations to help Web3 developers write Rust smart contracts that are not only secure and readable, but also verifiable.

Smart Contract Security
Learn the best practices for writing secure Uniswap v4 hooks to prevent vulnerabilities and enhance DeFi security. Follow expert guidelines to safeguard your smart contracts.

Formal Verification
In this post (the sequel to “How to optimize your gas consumption without getting REKT”), we focus our attention on Solidity/Yul libraries that realize the mathematical and economic computations that lie at the heart of the DeFi world, and explain why equivalence checking is a potent tool in the hands of developers and auditors who wish to work on such code.

Formal Verification
In our previous post, we described our new verification tool for Solana contracts. In this post, we show the verifier in action on SPL Token 2022, a widely-used Solana application. In the next post, we will show how to find bugs in the confidential extension of SPL Token 2022.

Formal Verification
Developing a DeFi product is an engineering problem of deceptive depth — it is easy to write a smart contract in Solidity that (mostly) does what you want, but it is hard to do it well.

Formal Verification
In this blog, we discuss our efforts to apply mutation testing in the context of automated verification.