Category: Software Development
Formally Modelling Optimism's Supernode: A Dafny Model, an AI Reviewer, and What They Achieved Together
Optimism's Supernode decides which cross-chain messages are valid and advances the cross-safe frontier: get it wrong in one direction and a chain builds on invalid state; wrong in the other, and the whole cluster stalls. This post covers a hand-written Dafny model of its core logic we built during a 10-week audit extension, and how we used it as the basis for AI-assisted fuzzing and comparison against the Go implementation.
What the TanStack npm compromise tells us about software trust.
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
On The Limitations of Audit Competitions
Audit competitions have surged in popularity recently, with numerous platforms vying to connect projects with independent security researchers. The premise is straightforward: organizations offer a cash prize to attract auditors eager to scrutinize their code for vulnerabilities. While cost-effective, the evolving ecosystem necessitates a closer examination of the drawbacks inherent in relying solely on audit contests.
GitHub Guidelines For Collaborative Coding
This blog is about Runtime Verification's guidelines for collaborative coding, which are designed to help teams manage their software development process and avoid introducing unneeded friction. It covers topics such as prioritizing work, opening PRs, reviewing PRs, addressing changes, and closing remarks. It also discusses the importance of trust and the use of CI in aiding collaborative coding.
