Group motivation

Software failures can lead to significant costs and even human hardship and danger. We believe that with an appropriate set of tools and techniques it is possible to improve the reliability of both existing and new software without a huge upfront investment.

Formal methods do not have to be “too expensive” or “too time consuming”; simple things can drastically improve the assurance of software, even without complete verification. Furthermore, academia is constantly generating new ideas. Which of those translate into suitable tools for a given context? There is a spectrum of assurance and we believe in combining different techniques to gradually bring software from zero assurance to fully verified. We aim to identify, use and improve upon the most suitable tools for the job.

We offer high-assurance services and team augmentation for clients who either have high-assurance needs or are themselves solution providers in this space. In particular, we are happy to assist in the following areas:

• Specification: help craft and lay specifications, and assess their aptness to an original goal by proving relevant properties about them
• Testing: help create better test suites, and build tools for executing them over complex domains
• Auditing: comprehensively test a system, report and showcase behaviours that are potentially harmful to system security or safety, assess code quality
• Tooling: improve existing tools to suit the testing/verification needs of a particular project, or write domain-specific tools from scratch
• Refactoring: help improve existing code bases through the use of modularisation, strongly typed code, purity, and other compile-time guarantees
• Full-fledged verification: assist in projects aiming to develop a completely verified piece of software

Within that context, one of our current main activities is the audit of Cardano smart contracts. Cardano is a very relevant target for our work, as it has strong formal foundations and all of its core components are both open-source and developed in Haskell, a first-class typed functional programming language.

Auditing activity

Security audits on Cardano require more than a generic understanding of blockchain technology. They demand deep knowledge of Cardano’s ledger, transaction model, governance mechanisms, and smart contract ecosystem. As a long-standing contributor to the Cardano ecosystem, Tweag has helped shape core components of the platform, including early work on the cardano-ledger implementation. Building on years of experience developing Cardano technologies, contributing to production systems, and auditing critical infrastructure, we help teams understand the true security posture of their protocols before deployment. Our reviews assess both risks arising from Cardano’s unique architecture and those introduced by project-specific design choices, business logic, and operational assumptions. The objective is not only to identify vulnerabilities, but also to uncover subtle edge cases and interactions that can compromise a protocol in production.

We believe that security is most valuable when it is transparent, actionable, and grounded in a thorough understanding of the underlying platform. Every audit is an opportunity to strengthen a project’s design, improve development practices, and build trust with users, stakeholders, and the wider community. Alongside rigorous manual review, we leverage cooked-validators, an open-source framework developed by Tweag to model realistic transaction scenarios and perform automated attack simulations against Cardano smart contracts. This allows us to systematically explore adversarial behaviors and validate security assumptions under conditions that closely resemble real-world usage. The result is more than an audit report: it is a comprehensive assessment that combines platform expertise, practical attack analysis, and actionable recommendations to help projects launch, evolve, and govern their systems with confidence.

See the products we have audited.

Agda work

Beyond high-value security audits on Cardano, we also carry out formal verification work for clients, in particular using Agda. Agda is a dependently-typed functional programming language, relatively close to Haskell, that lets us express correctness properties at the type level alongside the programs we write, or develop fully formal models of a given domain. A few examples of Agda-related work carried out by the group:

• Our audit of Marlowe included a formal model, which was part of the scope of the audit.
• We formalized the safety properties and proofs of Minotaur, an experimental blockchain protocol designed to combine stake from existing blockchains.
• We mechanized missing features in the Cardano Ledger specification, covering the Shelley and Alonzo eras of Cardano.
• We have contributed to the development of the formal specification of Leios, the new iteration of the Ouroboros consensus protocol.