MLabs: Path Analysis on Covenant

[Proposal setup] Proposal title

Please provide your proposal title

MLabs: Path Analysis on Covenant

[Proposal Summary] Budget Information

Enter the amount of funding you are requesting in ADA

99861

[Proposal Summary] Time

Please specify how many months you expect your project to last

6

[Proposal Summary] Translation Information

Please indicate if your proposal has been auto-translated

No

Original Language

en

[Proposal Summary] Problem Statement

What is the problem you want to solve?

Cardano smart contract audits are slow, costly, and error-prone due to lack of tooling and analyzable IRs. Existing languages aren’t suited to static analysis.

[Proposal Summary] Supporting Documentation

Supporting links

• https://github.com/mlabs-haskell/covenant
,
• https://www.mlabs.city

[Proposal Summary] Project Dependencies

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

Yes

Describe any dependencies or write 'No dependencies'

The project will depend on Covenant as a library, but not its associated code generator. In particular, this avoids any dependencies on Nix or the Cardano ecosystem. This dependency is essential, as it gives access to the Covenant ASG in a programmatic manner in a way that is suitable for the analysis we wish to do.

[Proposal Summary] Project Open Source

Will your project's outputs be fully open source?

Yes

License and Additional Information

Apache 2.0 License

[Theme Selection] Theme

Please choose the most relevant theme and tag related to the outcomes of your proposal

Research

[Campaign Category] Category Questions

Mention your open source license and describe your open source license rationale.

We intend to license the project under the Apache 2.0 License. This permissive and widely adopted license allows broad use, modification, and redistribution, while ensuring attribution and protection through explicit patent grants and disclaimers. All components of the project will be fully open source and maintained in public repositories throughout the entire project lifecycle and beyond.

How do you make sure your source code is accessible to the public from project start, and people are informed?

All source code will be hosted in a public GitHub repository under the Apache 2.0 license. Milestone updates, releases, and relevant documentation will be shared via MLabs channels to ensure transparency, accessibility, and public awareness throughout the development process.

How will you provide high quality documentation?

We will maintain Covenant’s standard of precise, high-quality documentation by fully covering all new functionality and tooling. Documentation will follow the Diataxis framework and be published alongside the code at github.com/mlabs-haskell/covenant, ensuring clarity, consistency, and ease of use for auditors and developers.

[Your Project and Solution] Solution

Please describe your proposed solution and how it addresses the problem

Problem

For any onchain script, Cardano or otherwise, auditing is a critical step to ensure that it is both correct and secure. For Cardano scripts specifically, auditing is currently tedious, manual and quite error-prone. This is for a range of reasons.

Firstly, few, if any, automated tools exist for performing the kinds of analysis auditors want on Cardano scripts. This forces an auditor to write manual, low-level tests on a per-script (or even per-script-functionality) basis. This takes extensive time, and due to its tedious and error-prone nature, potentially compromises the audit itself. This forces audits to take longer, and cost more, while potentially providing fewer guarantees.

Secondly, none of the languages currently used in the ecosystem for Cardano scripts are particularly suited to non-simulating analysis. This stems from a mixture of factors for each such solution:

• Plinth is embedded into Haskell, but is different enough from Haskell that any Haskell tooling is unable to cope with these differences. Indeed, even non-analytical Haskell tooling (such as editor plugins) often struggles with Plinth. Furthermore, Plinth is (or claims to be) Turing-complete, which severely limits what analysis is even possible statically.
• Plutarch is also embedded into Haskell, but due to being a true embedded language, cannot benefit from Haskell-level analysis tooling. Furthermore, Plutarch is also Turing-complete in the same way Plinth is, which similarly limits static analysis.
• Aiken compiles directly to UPLC, skipping any analyzable intermediate stage, and its Turing-completeness further limits the feasibility of robust static analysis.
• UPLC itself is untyped and Turing-complete, which makes static analysis nearly impossible in a meaningful way. Furthermore, UPLC is a low-level language, which makes it quite ‘distant’ from whatever language the script to be audited was written in, making it hard to perform relevant analysis on it.

While it could be possible, with considerable effort, to make tools that perform the kind of analysis an auditor would need, in practice they would be limited to simulation-style analysis. This is inferior to static analysis, which doesn’t require actually running the script (and setting up the environment needed to do so). This is particularly true of UPLC.

Thirdly, even if analysis tools existed that could do static analysis of the languages actually used to write scripts (such as Plinth or Plutarch), they would be limited to scripts written only those languages: for example, a tool made for Plinth could not be used on a script written in Plutarch. This is undesirable, as there are a multitude of reasons why a given script would be written in a given language, and forcing auditors to maintain N tools to do the same task due to the possibility of having to work with N different languages is unreasonable.

These problems currently make audits long, tedious, expensive and ultimately unreliable. This creates problems both for script developers, who are forced to pay larger sums of money for audits, and for auditors, who must spend a lot of time doing work that ultimately should be automated, allowing them to focus on the kind of analysis a machine cannot do well.

These problems motivated the creation of Covenant: a Turner-total, fully hash-consed, call-by-push-value IR designed as an intermediate target for languages designed to write Cardano scripts. The choices that went into Covenant were designed to allow a combination of two desirable factors:

• Similarity to the source language(s) in the IR; and
• Static analyzability

This puts Covenant into a powerful niche as a target for auditor static analysis tooling, as it effectively addresses all of the problems we listed above, while also providing other benefits:

• Covenant’s combination of static typing, Turner totality (without proper codata), hash consing and call-by-push-value make it ideal for static analysis. By not claiming Turing-completeness, while also maintaining a lot of useful information, Covenant allows a wide variety of analysis tools.
• Any tool written for Covenant could be used on scripts written in any language that can output Covenant. Thus, per-front-end-language tooling would become unnecessary. Furthermore, as Covenant maintains a lot of contextual information about the script that would be lost at the level of UPLC, such tools wouldn’t suffer from the loss of information that a tool written against UPLC would.
• Covenant itself does not depend on Plutus, Nix or the Cardano ecosystem at all, provided the code generator is not being used. As it is written in conventional, simple Haskell, and is distributed via Hackage, tool development and use becomes as easy as any other Haskell program.

However, presently, no analysis tooling based on Covenant exists.

Solution

We propose an analysis tool for Covenant, designed to perform path analysis. Intuitively, path analysis allows an auditor to specify an input to track, as well as a script which receives this input, with the output being a set of paths that potentially affect or interact with this input. An input could be any of the following:

• A field of a datum or redeemer
• A field (or sub-field) of the script context
• A local binding within the script

The output would be a set of paths through the ASG to its root node from a node where the input is first interacted with, with each node along that path (potentially) interacting with that input. An ‘interaction’ could be any of the following:

• Constructing a value based on the input
• Branching on the input
• Looping or reducing on that input

The analysis tool will be configured using JSON, and will produce its output as JSON, to allow for interoperability with other tooling. The initial design would work as a CLI tool; we will design the tool to support both interactive (with a human auditor synchronously directing it) and non-interactive (such as in CI pipelines) use.

The tool will be written using Haskell, in a similar approach to Covenant, and will be published on Hackage. No dependencies on Plutus, Nix or the Cardano ecosystem will be needed to build, or use, the tool. We will provide documentation of the input and output formats, as well as what the tool can do, following the Diataxis framework.

Market

Our primary target audience are onchain script auditors. The goal of our project is primarily to provide a useful tool to automate away an otherwise tedious, manual and error-prone task. Furthermore, our secondary audience are Cardano ecosystem developers more generally, as our tool will demonstrate the ease and convenience of working with Covenant as an IR for tooling of all kinds.

Features

• A CLI tool that performs path analysis on a script in Covenant IR
• The CLI tool accepts a JSON formatted configuration with a documented structure to specify an input to keep track of
• The CLI tool outputs a JSON formatted result, specifying paths which the input can affect
• The CLI tool is documented using the Diataxis framework
• The CLI tool is distributed on Hackage
• No dependency on Plutus, Nix or the Cardano ecosystem

[Your Project and Solution] Impact

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

We foresee three major impacts of our work. Firstly, this tool in itself will significantly benefit auditors working on Cardano scripts, as it will allow the automation of a currently tedious, error-prone and manual task. This will allow audits to give higher assurances, find issues more quickly and cheaply, and allow auditing teams to focus their efforts on more complex issues and concerns.

Secondly, this tool will demonstrate that Covenant’s serial form is easy to work with for the purposes of tooling, regardless of whether this tooling is designed for auditing, or for some other purpose. Lastly, this tool will show the benefits of using Covenant as a target for languages used to write Cardano scripts today, as it will provide a benefit that none of these languages currently can.

Sharing Outputs and Opportunities

We are committed to open communication and knowledge sharing throughout the project lifecycle. We will actively engage with the Cardano community through various channels, including:

• Open-source repository: maintaining a public repository where all project code, documentation, and updates will be readily available.
• Community forums and social media: participating in discussions, sharing progress updates, and addressing questions and feedback from the community.
• Technical publications and presentations: disseminating our findings and insights through conference presentations, blog posts, and academic publications.
• Workshops and tutorials: organizing educational events to introduce developers to Covenant and its benefits.

[Your Project and Solution] Capabilities & 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?

MLabs has a proven track record of delivering high-quality projects on Cardano, with a history of collaboration with IOG, Intersect and other important organizations within the Cardano Ecosystem. Our expertise in Haskell and blockchain development, paired with a strong focus on formal verification and testing, ensures a robust and reliable solution.

We will validate the feasibility of Covenant through iterative development, prototyping key features, and gathering feedback from the community. We will maintain transparency by regularly sharing our progress publicly, ensuring accountability and trust throughout the project.

Our team's deep understanding of Cardano's intricacies and our commitment to open-source development demonstrate our capability to deliver this project successfully. We will adhere to strict financial management practices, providing detailed reports and transparent accounting in this submission to ensure responsible use of funds.

[Milestones] Project Milestones

Milestone Title

Configuration format and conformance

Milestone Outputs

1. A design for a JSON-based configuration file format, which describes which input to a script we want to perform path analysis for.
2. A Haskell project, not dependent on Plutus, Nix or Cardano, which implements data types representing all the information provided by the configuration file format from item 1.
3. JSON deserialization code for each of the data types from item 2, designed to correspond with the design from item 1.
4. At least two conformance cases of configuration files following the design from item 1. At least one of these must be a ‘negative’ case (meaning it should fail to parse).
5. Tests to ensure that the conformance cases defined in item 4 behave as expected. That is, ‘positive’ cases (ones that should deserialize) end up deserializing to the right data types with the right values in their fields, while ‘negative’ cases (ones that shouldn’t deserialize) indeed fail to deserialize.
6. Publish the project on Github, together with CI that ensures the tests from item 5 are run. The project must also follow proper Haskell practices, as defined by a code standards document in the same repository.

Acceptance Criteria

1. A Haskell project published on Github, containing all the required data types, and their deserialization code, as per the description in the ‘Outputs’ section of this milestone exists.
2. The project from item 1 contains at least two conformance cases, represented as configuration files. At least one of those files must be a ‘negative’ case; that is, it should not deserialize.
3. The project from item 1 has CI, which ensures that tests to validate all conformance cases from item 2 are run. These tests should show that the conformance cases from item 2 behave as expected.
4. The project from item 1 must have a code standards document. That project should faithfully implement those standards; where reasonable, maintenance of these standards should be verified by the CI from item 3.
5. The project from item 1 must not depend on Plutus, Nix, or the Cardano ecosystem.

Evidence of Completion

1. Haskell project on Github implementing the stated requirements from the ‘Outputs’ section of this milestone.
2. Conformance cases for the configuration format, as configuration files, as part of the project from item 1.
3. The results of the CI implemented for the project in item 1, specifically demonstrating that conformance cases from item 2 behave as expected.

Delivery Month

2

Cost

24588

Progress

20 %

Milestone Title

Output format and conformance

Milestone Outputs

1. A design for a JSON-based output format, which describes a set of paths through the Covenant ASG.
2. Additional data types for the project from Milestone 1, which correspond to the information in the design from item 1.
3. JSON serialization code for each of the data types from item 2, designed to correspond with the design from item 1.
4. Additional tests for the project from Milestone 1, designed to ensure that the serialization code from item 3 behaves as per the design from item 1. These tests should be run by the CI from the Milestone 1 project.

Acceptance Criteria

1. The project from Milestone 1 has been extended with additional data types, and serialization code, as per the ‘Outputs’ section of this milestone.
2. Tests for the project from Milestone 1 have been added to ensure that the additional data types added in item 1 behave according to the design from the ‘Outputs’ section of this milestone. These tests should pass.
3. The CI for the project from Milestone 1 has been extended to run the tests specified in item 2.

Evidence of Completion

1. Haskell project from Milestone 1, extended with all the requirements from the ‘Outputs’ section of this milestone.
2. The CI runs the additional tests described in the ‘Acceptance Criteria’ of this milestone, and these tests pass.

Delivery Month

3

Cost

25127

Progress

50 %

Milestone Title

Tool implementation

Milestone Outputs

1. Added functionality to the Milestone 1 project which, when given a deserialized configuration file (in the form of a Milestone 1 data type) and a Covenant ASG, will produce either an error, or a Milestone 2 data type corresponding to the path analysis of the input described by the deserialized configuration file in that ASG.
2. Tests for the functionality in item 1. These tests must pass, and be run by the CI.

Acceptance Criteria

1. The project from Milestone 1 has been extended with the functionality described in the ‘Outputs’ section of this milestone.
2. Tests for the functionality in item 1 exist and pass. The CI runs these tests.

Evidence of Completion

1. Haskell project from Milestone 1, extended with all the requirements from the ‘Outputs’ section of this milestone.
2. The CI runs the additional tests described in the ‘Acceptance Criteria’ of this milestone, and these tests pass.

Delivery Month

4

Cost

24911

Progress

70 %

Milestone Title

Tool interface and publication

Milestone Outputs

1. A CLI application, providing a frontend to the functionality from Milestone 3, and making use of the serialization and deserialization logic from Milestones 1 and 2. This application will be in the same repository as the Milestone 1-3 work.
2. The CLI application from item 1 is published on Hackage.
3. The CLI application follows the CLIG standards.

Acceptance Criteria

1. A CLI application, as described in the ‘Outputs’ section of this milestone, exists and is included in the same repository as the Milestone 1–3 codebase.
2. The application described above is published and publicly available on Hackage.

Evidence of Completion

1. CLI application implemented and publicly released
2. Source code and package published on Hackage

Delivery Month

6

Cost

25235

Progress

100 %

[Final Pitch] Budget & Costs

Please provide a cost breakdown of the proposed work and resources

Milestone 1 – Configuration Format and Conformance (114.0h)

Design JSON config format: 10.0h

Implement Haskell types: 28.5h

Implement deserialization: 24.0h

Write conformance cases: 18.0h

Test deserialization: 17.0h

CI setup and code quality checks: 16.5h

Subtotal: 114.0h

Milestone 2 – Output Format and Conformance (116.5h)

Design JSON output format: 12.0h

Add Haskell types for output: 27.0h

Implement serialization: 25.0h

Write tests for output types: 31.0h

Extend CI for new tests: 21.5h

Subtotal: 116.5h

Milestone 3 – Tool Implementation (115.5h)

Integrate Covenant ASG: 24.0h

Implement path analysis logic: 37.0h

Error handling & edge cases: 22.5h

Testing & validation: 21.0h

Extend CI coverage: 11.0h

Subtotal: 115.5h

Milestone 4 – CLI Interface and Publication (117.0h)

Design CLI UX & argument handling: 16.0h

Integrate CLI with analysis backend: 30.0h

Test CLI behavior (interactive + CI): 20.0h

Publish to Hackage: 6.0h

Write CLI usage doc (Diataxis – Information): 18.0h

Write learning/goals/understanding docs (Diataxis): 27.0h

Subtotal: 117.0h

Total Hours: 463

Total Budget: $51,040 USD

Blended Rate: ~$110/hour

Converted at $0.51/ADA: 99,861 ADA

**In the interest of full transparency, please note we have applied a conservative USD/ADA exchange rate in pricing this proposal. This is to ensure our operations remain stable regardless of market conditions. Although we firmly believe the future of Cardano is bright, we recognize the price of ADA and all cryptocurrencies is inherently volatile. Our financial obligations are denominated in fiat. Most importantly, this includes the salary of our engineers whose hard work makes projects like this possible.

In the unlikely scenario of severe negative price movement beyond our forecasted rate, it is possible that MLabs may need to temporarily suspend work on this proposal until the market recovers. Rest assured, this decision would be made solely to protect our business's long-term viability and never taken lightly.

We appreciate your understanding and support, and we are excited to see what we can achieve together.

[Final Pitch] Value for Money

How does the cost of the project represent value for the Cardano ecosystem?

This project represents value for money for the Cardano ecosystem by addressing a fundamental, yet largely silent, problem that exists today. Auditing an onchain script is already one of the most difficult tasks that can be asked from a team, to say nothing of the significant responsibility such a task carries with it. However, despite the importance of audits to the health of the Cardano ecosystem as a whole, and to our trust in scripts more specifically, it is currently a tedious, low-level, error-prone and manual task, forcing auditors to spend their time on solving (and re-solving) problems that really don’t require a human’s capabilities. This is a doubly painful result: not only do we drive up the cost of audits (in terms of time, money, and so on), but we also get worse results.

By making this tool, and showing how Covenant makes such a tool easy to both implement and use, we create long-term leverage: auditors will spend less time on mechanical trace-throughs, and more time on high-value logic checks. This will reduce audit costs and increase their rigor. At the same time, we demonstrate Covenant’s potential as an ecosystem-wide IR, making it easier for other tools to follow suit. For a relatively modest cost, the Cardano ecosystem gains a reusable, extensible, and broadly applicable auditing primitive—open source, highly interoperable, and aligned with ecosystem goals.

[Required Acknowledgements] Consent & Confirmation

Terms and Conditions:

Yes