SmartCodeVerifier: Automated Formal Verification Tool for Smart Contract Code

[GENERAL] Name and surname of main applicant

Input Output Global Inc.

[GENERAL] Are you delivering this project as an individual or as an entity (whether formally incorporated or not)

Entity (Incorporated)

[GENERAL] Requested funds in ada

200000

[GENERAL] Please specify how many months you expect your project to last (from 2-12 months)

12

[GENERAL] Please indicate if your proposal has been auto-translated into English from another language

No

[GENERAL] Summarize your solution to the problem (200-character limit including spaces)

An automated tool, combining both model checking and theorem proving techniques, to formally verify smart contract implementations with proof artifacts and counterexample generation capabilities.

[GENERAL] Does your project have any dependencies on other organizations, technical or otherwise?

Yes

[GENERAL] If YES, please describe what the dependency is and why you believe it is essential for your project’s delivery. If NO, please write “No dependencies.”

Our tool will use two third-party software, namely: Lean4 and Z3. There is close to no risk in their usage as they are open source with permissive licenses (Apache 2.0 and MIT) and are also very mature with several stable major releases. Their use in other industrial products is well-established (Frama-C, SparkAda, CBMC, ...)

[GENERAL] Will your project’s output/s be fully open source?

Yes

[GENERAL] Please provide here more information on the open source status of your project outputs

All the Lean formalization, rewriting rules, optimizations, translation to SMTlib and the whole tool itself will be open-source under Apache 2.0. The SMT models developed will also follow the SMTLib2 standard for broad reusability across multiple solvers.

Future developments to enhance this tool will be added to the open-source repository.

All contributions from the community to improve the tool and add features will be welcomed.

[METADATA] Horizons

Developer Tools

[SOLUTION] Please describe your proposed solution

The challenge we are addressing is the difficulty developers face when trying to exhaustively verify their smart contract implementations. In the current state-of-the-art for Cardano's smart contracts, two main approaches exist: the use of interactive theorem provers like Coq or Agda to formally verify the intended behavior of smart contracts, and the use of testing techniques like property-based testing.

Existing formal verification tools for Cardano smart contracts are predominantly based on interactive theorem provers. While these tools can ensure security, correctness, and reliability, they typically require expert knowledge of formal methods. Their expressive power makes them valuable for proving complex and intricate properties. However, the steep learning curve, limited support for automated reasoning, and inability to produce counterexamples for falsified theorems make them almost inaccessible to non-experts. Additionally, most of these approaches require developers to express their smart contracts in a formal language, potentially creating gaps between the source code and the formal model's semantics. These gaps often appear when abstractions are introduced to facilitate reasoning.

As a result, most developers and auditors prefer to use powerful testing techniques like property-based testing, e.g., QuickCheck-Dynamic for Haskell or the Fuzz library for Aiken. However, these testing techniques require significant development effort and do not guarantee exhaustiveness. Specifically, the effort needed to implement test scenarios and attacks can grow exponentially with the number and complexity of test objectives. Moreover, the generated scenarios or attacks may still be insufficient to cover all edge cases, leaving bugs and security vulnerabilities undetected.

Our proposed solution is an Automated Verification Tool, developed in Lean4, that combines symbolic model-checking and theorem proving techniques to hide the complexity of formal verification of smart contract implementations. Our goal is to deliver a push-button verification approach where users simply annotate their smart contract code with a set of properties that must be satisfied.

To achieve this, we will provide a universal annotation language with a well-defined syntax and semantics to ensure consistency across the various Cardano smart contract ecosystems (e.g., Plinth, Aiken, Plu-ts, Opshin). Dedicated transpilers are also expected to be developed to automatically translate the annotated smart contract code into Lean4, thus eliminating the need for users to learn Lean4 themselves. This approach streamlines the verification process and avoids discrepancies between the source code and its formal representation.

To minimize user intervention and eliminate the need for manually writing proofs, the verification tool will rely on a set of normalization and simplification techniques, along with SMT solving, to automatically prove/refute as many proof obligations as possible. Proof artifacts will be automatically reconstructed using SMT results and the applied rewriting rules. The tool will also allow users to inspect any unsolved subgoals, enabling them to identify missing auxiliary lemmas. 

The expressive power of the annotation language will enable users to describe both global properties related to the blockchain state, and transaction-related or temporal properties. This capability will allow the formal verification of individual smart contracts, but also of entire decentralized application (DApp) protocols composed of multiple interconnected minting and validator scripts. Hence, users will be able to assess the correctness and security of their DApp protocol as a whole.

Consequently, users will NOT be required to model the blockchain state, blockchain events, or even assumptions guaranteed by the Cardano ledger rules, as these will be considered implicitly in the backend Lean4 formalization. 

The tool’s support for counterexample generation across multiple blockchain events for falsified properties will help users identify potential issues and vulnerabilities within their DApp protocol.

Our approach stands out by seamlessly integrating formal verification into the traditional smart contract development workflow via an easy-to-use CLI tool. The tool's architecture consists of several key components, as illustrated in the diagram below:

• Universal Annotation language: A formal annotation language that, in addition to the usual logical operators, will provide a set of builtin primitives (e.g., transaction-related helper functions, blockchain state observers, temporal operators) to express properties characterizing the expected behaviors of smart contracts or showing absence of security vulnerabilities/deadlock state (see an example in the VSCode screenshot).
• Smart contract language to Lean4 transpilers (C1): Each dedicated transpiler is expected to provide several essential capabilities to facilitate user experience. It will automatically translate annotated smart contract code into Lean4 while ensuring that a predefined set of coding rules are met. Moreover, any Lean4 type-checking errors are expected to be pushed back to the source code level for debugging purposes. A transpiler may also offer the option to automatically generate a set of proof obligations, either to address common security vulnerabilities (e.g., large datum attacks, large value attacks, etc) or to establish low-level correctness.
• Plinth and Plutus Ledger Api Lean4 formalization (C2): This Lean4 formalization serves multiple crucial purposes, namely: it ensures the correctness and absence of security vulnerabilities in all exposed Plinth and Plutus Ledger Api libraries; it provides the fundamental components for developing the Plinth-to-Lean4 transpiler, including the built-in primitives for the universal annotation language and the automatic generation of proof obligations; it introduces the low-level functionalities required to formalize the EUTxO blockchain state; and it may also be used to directly specify and prove Plinth-based smart contracts in Lean4.
• EUTxO Blockchain state Lean4 formalization (C2): Lean4 formalization characterizing the blockchain state and events necessary for smart contact verification. In essence, the EUTxO Ledger state will be modeled as a reactive system, following a state-machine framework. The formalization will account for the assumptions guaranteed by the Cardano ledger rules to accurately define well-formed and well-balanced script contexts, immutability of the blockchain state and absence of double-spending (i.e., a UTXO cannot be spent more than once). 
• CEK Machine Lean4 formalization (C2): Lean4 formalization of the CEK machine to evaluate Plutus Core terms. This formalization is necessary for proving smart contracts code at the UPLC level. Note that for this use case, the properties to be verified must still be expressed using the formal annotation language.
• Lean4 Optimizer (C3): A preprocessor that will apply a set of normalization and simplification rules aiming at reducing model complexity and generating formulas optimized for efficient SMT solving. This optimization phase is essential to enhance the performance of the verification process by allowing the SMT solver to automatically prove or refute as many proof obligations as possible without requiring any user intervention. By simplifying the model representation, the preprocessor will play an essential role in minimizing manual effort while maximizing the tool’s verification capabilities on significant DApp protocols.
• Lean4-to-SMT Translator (C4): Translator to efficiently encode a Lean4 specification into SMTLib2 format while accurately handling higher-order logic to first-order logic transformations as well as induction proof schemas for recursive functions. 
• SMT solvers (C5): Backend solvers invoked to automatically verify smart contract properties, generate proof artifacts or counterexample traces. 
• Interactive proof mode (C6): An interactive mode that will be made available on demand, allowing users to inspect any unsolved subgoals during the verification process. This mode will provide advanced users with the flexibility to explore the proof state, enabling them to assist the backend solvers by providing the necessary reasoning steps to resolve challenging properties.

The architecture is illustrated below:

Architecture of the automate verification tool (yellow: components developed in this project, green: already existing software components, white: potential future developments)

Key features of our solution include:

• Proof Automation: The tool will leverage normalization, simplification techniques, and SMT solving to automatically prove or refute as many proof obligations as possible. Proof artifacts will be automatically reconstructed based on SMT results and applied rewriting rules, streamlining the verification process.
• Execution Traces: Counterexample generation across multiple blockchain events for falsified properties, which will help users identify potential issues and vulnerabilities within the DApp protocol with greater accuracy.
• User Experience: Designed for a seamless experience, developers will continue working in their preferred smart contract language without needing to interact with Lean4 code in most cases. There's no requirement for users to model the proof execution environment (e.g., blockchain state, transaction submission, or fund transfers). Instead, they will only need to annotate their smart contracts with global state properties aligned with their business logic and security specifications.
• Automated property generation: The tool will be able to automatically generate properties related to common vulnerabilities, such as double satisfaction, large datum attacks, and large value attacks. This will allow users to focus on defining properties specific to their smart contracts without being burdened by common security concerns.
• Advanced Capabilities for Experts: In rare cases where the automated solver cannot resolve complex problems, advanced users can manually intervene using Lean, though this will be an exception rather than the norm.

Mock of the future integration into VSCode, where users only have to annotate their code with the specification (left panel), run the tool through a simple CLI command (bottom panel), and can see realistic traces of execution leading to a property violation (right panel)

Our tool will primarily benefit two key user groups:

1. Smart contract developers: They will be able to formally verify their contracts without needing specialized expertise, leading to more secure and reliable contracts for the Cardano ecosystem.
2. Auditors: Auditors will gain a powerful tool to automatically check contract properties, enhancing the thoroughness of their audits and reducing the time required for manual review.

By greatly simplifying formal verification, this tool will set a new standard for smart contract security in Cardano. The impact will be demonstrable through reduced security vulnerabilities, fewer on-chain failures, and an overall increase in trust for Cardano smart contracts. We expect the Cardano ecosystem to benefit from more efficient audits and more secure smart contracts, promoting wider adoption of blockchain technology for critical applications.

[IMPACT] Please define the positive impact your project will have on the wider Cardano community

Value to the Cardano community

The proposed verification tool, SmartCodeVerifier, will significantly enhance the security and reliability of smart contracts within the Cardano ecosystem by making formal verification more accessible to developers. This will significantly reduce the risks of critical vulnerabilities in deployed contracts and reduces reliance on manual testing methods, such as property-based testing, which often overlook critical edge cases.

In this Catalyst fund, our focus will be on delivering the core components of the verification tool, establishing the foundation for future expansions. This will enable other teams or projects to contribute by developing and integrating new language modules into the tool. These contributions may include transpilers for additional languages to Lean4, formalization of core libraries, and tools to translate counterexamples back into the original programming language.

We envision a future where various smart contract programming languages (such as Plinth, Aiken, Plu-ts, Opshin, Plutarch, etc.) and compilation pipeline languages (PIR, Typed Plutus Core, Untyped Plutus Core, and more) are integrated within a single verification framework. New developments will leverage the already formalized blockchain state, as well as the optimization and rewriting rules that ensure the tool’s scalability and efficiency.

The core infrastructure of the tool can be extended to support other blockchains. For example, with the proper implementation of a new blockchain state and events, and the appropriate transpiler and formalization, our tool could verify smart contracts written in Compact for Midnight.

Measuring Impact

While we won’t directly track usage or contract verifications (since users will be free to download the tool from GitHub), we can measure impact in other meaningful ways:

• GitHub Metrics: We will track metrics such as watchers, stars, and forks, which will indirectly indicate community interest and usage.
• Community Feedback: Through community Discords, working groups, GitHub discussions, and developer outreach, we will assess tool adoption and gather qualitative feedback on user experiences.
• Contributions and Engagement: We will monitor community contributions (issues, pull requests, forks) to gauge relevance, usage, and engagement within the open-source project.

Sharing Outputs

To maximize its impact, we will make all project deliverables publicly available and engage with the community:

• GitHub Repository: The entire toolset, including the Plinth formalization, blockchain state and event models, optimizations, rewriting rules, and SMTLib translations, will be fully open source and accessible to anyone.
• Documentation and Tutorials: Comprehensive documentation, including step-by-step guides and example use cases, will be created to make the tool easy to adopt. Tutorials for common use cases will also be provided.
• Community Outreach: We plan to present the tool at Cardano community events, conferences, and working groups to showcase its features and gather valuable feedback to drive adoption.
• Collaborations with Auditors: By partnering with auditing firms and developer groups, we will ensure the tool is used in real-world audits and development workflows, helping to establish best practices for smart contract verification within the Cardano ecosystem.

Value to the Cardano Community

By providing developers and auditors with an easy-to-use, robust formal verification tool, we will significantly reduce the risk of smart contract vulnerabilities in Cardano’s ecosystem. This will lead to more secure decentralized applications and build greater trust in Cardano’s blockchain infrastructure.

The tool’s core functionality will be extendable to cover a growing range of use cases, whether it be new programming languages or even other blockchains.

The tool's open-source nature will encourage ongoing innovation and improvements by the broader community, further enhancing its value.

[CAPABILITY & FEASIBILITY] What is your capability to deliver your project with high levels of trust and accountability? How do you intend to validate if your approach is feasible?

Our team is composed of highly skilled formal methods engineers and developers with extensive experience. With over 15 years of expertise in designing and implementing automated verification tools for complex, safety-critical systems, we specialize in creating tools that must be qualified to avoid false positives. We have also been involved in the design, development, and validation of production DApps like Djed, where we have devised an innovative testing framework that not only focuses on functional correctness but also on assessing the robustness of the on-chain code against attacks on submitted transactions.

Additionally, we bring significant experience in applying formal methods for smart contract verification (e.g., in Agda or using Kind2) and have conducted in-depth safety and threat analyses on Cardano smart contracts, identifying potential vulnerabilities, deadlocks, and computational errors. The team is also well-versed in Lean4 formalization and possesses advanced skills in meta-programming, along with a deep understanding of Lean4’s internal representation and codebase.

Moreover, we have already developed a proof of concept in Lean4, demonstrating the feasibility of the proposed solution. Specifically, we have formalized a representative set of Plinth libraries in Lean4 and implemented a set of optimization and rewriting rules, which have shown significant capability in simplifying and proving non-trivial formulas. Additionally, we have an initial Lean4-to-SMT implementation that automatically invokes an SMT solver for any remaining unsolved formulas. This progress underscores the potential of our approach in efficiently verifying complex smart contracts.

[PROJECT MILESTONES] What are the key milestones you need to achieve in order to complete your project successfully?

Core Automated Verification Framework In Lean4

A. Milestone outputs

• Preprocessing module that implements the optimization and rewriting rules for formula simplification
• Lean4-To-SMT translator that encompasses the handling of higher-order logic to first-order logic transformations as well as induction proof schemas for recursive functions. 
• Counterexample generator to translate back SMT terms to Lean4 terms
• Unsolved subgoals generator that allows users to inspect any unsolved formulas during the verification process.

B. Acceptance criteria

• Proven theorems showing soundness for each applied rewriting rule.
• Extensive test suite showing that the normalization and simplification rules have been properly implemented.
• Extensive test suite showing that Lean4 semantics is preserved up to the SMT solver invocation and the ability to produce counterexamples for complex recursive functions.
• Detailed formal specification for both the preprocessing module and Lean4-To-SMT translator. 

C. Evidence of milestone completion

• Code committed to the repository.
• Demonstration of the tool verifying simple properties on basic valid theorems.
• Demonstration of the tool generating counterexamples on basic faulty theorems.

Plinth and Plutus Ledger Api Formalizations

A. Milestone outputs

• Lean4 formalization of all Plinth libraries including all the necessary correctness theorems.
• Lean4 formalization of all Plutus Ledger API libraries including all the necessary correctness theorems.

B. Acceptance criteria

• All Plinth modules, necessary for smart contract verification, have properly been formalized in Lean4 and the formalization preserves the Plinth semantics.
• All Plutus Ledger API modules have properly been formalized in Lean4 and the formalization preserves the semantics.
• The identified theorems cover all potential failure modes for each Plinth and Plutus Ledger Api library.
• Successful demonstration of the tool to prove or refute theorems expressed in the Plinth and Plutus Ledger Api formalizations.

C. Evidence of milestone completion

• Both formalizations committed to the repository.
• All identified theorems have been proven

State-Machine Framework In Lean4

A. Milestone outputs

• Dedicated Lean4 syntax and term elaborator for state-machine specification that will generate the appropriate Lean4 representation.
• Introduction of basic temporal operators to support the specification of temporal properties.
• Implementation of bounded model checking strategy for counterexample detection on state-machine.
• Implementation of K-induction strategy for invariance satisfaction on state-machine.

B. Acceptance criteria

• Extensive test suite covering simple, moderate, and complex state-machine formalization.
• Extensive test suite to validate the bounded model checking (BMC) strategy, covering counterexample generation over significant execution cycles.
• Extensive test suite to validate the K-induction strategy, namely: the induction proof schema showing that all expressed properties hold for all reachable states.
• Detailed formal specification for the syntax and semantics for the state-machine framework, temporal operators and the model checking strategies.

C. Evidence of milestone completion

• Code committed to the repository.
• Demonstration of the tool verifying properties on state-machine formalizations.
• Demonstration of the tool’s capacity to generate counterexamples over several execution cycles.

EUTxO Blockchain state Lean4 formalization

A. Milestone outputs

• State-machine representation of the Ledger state necessary for smart contract verification, including the required blockchain events (e.g., pay to wallet, registration/deregistration, certification, etc.).
• Formalization of the necessary assumptions guaranteed by the Ledger rules and Cardano node for smart contract verification (e.g., well-formed and well-balanced script contexts, blockchain state immutability, absence of double-spending, etc.).

B. Acceptance criteria

• Extensive test suite, including proven theorems, establishing the correctness of the EUTxO blockchain state formalization. 
• Modeling of a set of smart contracts instantiating the EUTxO blockchain formalization to showcase the tool’s capacity to prove/refute global state, transaction-related and temporal properties.
• Demonstration of counterexample generation over several blockchain events.
• Detailed formal specification of the Ledger rule assumptions considered in the blockchain state formalization.

C. Evidence of milestone completion

• Code committed to the repository.
• Demonstration of the tool verifying properties on protocols composed of multiple interconnected minting and validator scripts. 
• Demonstration of the tool’s capacity to generate counterexamples over several blockchain events.

Documentation, Support material

A. Milestone outputs

• Comprehensive user documentation, tutorials, and examples.
• Guide on how to use the tool and its current capabilities
• Guide on how to contribute to the project.

B. Acceptance criteria

• Published user manual and tutorials covering all tool features, including installation, usage and how to contribute to the project.
• Clear examples showing the step-by-step process for using the tool.

C. Evidence of milestone completion

• Documentation publicly available on the project website and GitHub repository.
• Contributing guidelines published

[RESOURCES] Who is in the project team and what are their roles?

Jean-Frédéric Etienne

Senior Formal Methods Engineer at IOG with more than 15 years of experience in developing automated formal verification tools qualified for use at the highest level of certification in critical industries. He is also currently the architecture lead for the Djed implementation on Cardano and has put in place a property-based testing methodology to extensively assess the correctness and robustness of Plutus smart contracts against all potential attacks. He has also specified and proved the adaptation of the Djed protocol on the EUTxO model and has developed a set of Plutus libraries to produce optimized on-chain code.

Romain Soulat

Technical lead for the Plutus High Assurance team at IOG and formal method engineer for 10+ years. Romain has extensive experience in using various model checkers in different industries (Avionics, military, cybersecurity) and has developed model checkers for several kinds of automata.

Alasdair Hill

Formal Method Engineer at IOG. Alasdair has developed the ledger specification for the Alonzo era. As such, he has extensive experience in formalizing the blockchain state.

[BUDGET & COSTS] Please provide a cost breakdown of the proposed work and resources

We are only seeking funding for the part of the development cost. Project management, coordination of the team, community engagement and outreach will be essential parts of this project and are already funded.

Development Costs

• Core Automated Verification Framework In Lean4 (Milestone 1)
• Developers, formal methods experts required to extend Lean with model checking capabilities. This milestone will require significant effort to architect the tool in such a way that all the other components will fit together

• Estimated cost: ₳85,000 Ada

• Plinth and Plutus Ledger Api Formalizations (Milestone 2)
• Developers familiar with the internals of Plinth and Plutus Ledger API, formal methods experts to develop the necessary formalizations that are semantically equivalent. This budget also covers the efforts necessary to prove all the theorems to show the correctness of the formalization.

• Estimated cost: ₳35,000 Ada

• State-Machine Framework In Lean4 (Milestone 3)
• Formal methods experts to develop in Lean4 a state machine model and temporal operators. Model checker experts to properly implement the BMC, and K-induction strategies.

• Estimated cost: ₳30,000 Ada

• EUTxO Blockchain state Lean4 formalization (Milestone 4)
• Formal method experts with deep knowledge of the EUTxO model and the different ledger rules to be implemented. Significant efforts will be spent in ensuring the correctness of the model with respect to the Cardano Node and Agda ledger specification.

• Estimated cost: ₳40,000 Ada

• Documentation, Support material (Final Milestone)
• Developers to produce quality tutorial material and engage with the community to produce useful and up-to-date tutorials.

• Estimated cost: ₳10,000 Ada

[VALUE FOR MONEY] How does the cost of the project represent value for money for the Cardano ecosystem?

The costs outlined in the previous section have been carefully estimated to reflect the complexity and scope of the project, ensuring that each element contributes to delivering a high-quality, secure tool for the Cardano community. Below is the reasoning behind the cost structure:

Development Costs

The vast majority of the project’s budget is allocated to the development of the automated verification tool. This includes extending Lean4 with model checking capabilities, formalizing the relevant parts of the Cardano blockchain and Plinth, optimization and rewriting rules, and integrating calls to SMT solvers. These tasks require highly specialized knowledge in formal methods, blockchain technology which is reflected in industry-standard developer rates.

Marketing and Community Engagement

IOG will cover the cost of outreach and community engagement as part of its daily activities to ensure that the tool is widely adopted by developers and auditors.

Documentation and Reporting

Comprehensive documentation is essential for ensuring that the tool is usable by developers and auditors without needing deep formal methods expertise. The cost for creating detailed guides reflects the time and effort needed to produce high-quality materials.

Value for Money

This project represents significant value for money for the Cardano ecosystem because:

• Increased Security: By making formal verification accessible to all Plinth developers, the tool will reduce the likelihood of bugs and vulnerabilities in smart contracts, potentially saving developers and projects from costly failures.
• Broader Adoption: The tool will set a new standard for smart contract verification in Cardano, encouraging widespread use.
• Open Source Contribution: The entire tool will be open source, allowing the community to contribute, extend it to other smart contract programming languages, and improve it over time, creating long-term value for Cardano.

This project will offer lasting value through improved security and usability for the Cardano ecosystem, ensuring a high return on investment for the funding provided.