Emilyvas

Project Owner

TypeBridge: Intent-to-Contract Agent Compiler

Expert Rating

n/a

Type SingularityNET RFP
Funding Request $40,000 USD
RFP Guidelines An AI-native Development Environment for the ASI:Chain

Overview

We compile MeTTa type specs into verified Rholang contracts. Input: agent behavior as MeTTa dependent types. Processing: type-directed generation with Hyperon verification. Output: Rholang contracts proven correct before deployment. This isn't LLM code generation — it's formal synthesis where types guarantee correctness. M1 delivers the compilation pipeline with 15+ verified templates. M2 adds a 2-5 agent simulation arena for interaction testing. M3 completes lifecycle tooling and runs a DevNet beta with external developers. We're type-theory people applying compiler techniques to agent development.

RFP Guidelines

Open for Proposals

An AI-native Development Environment for...

Ending on:

13 Feb. 2026

Days

Hours

Minutes

Type SingularityNET RFP
Total RFP Funding $50,000 USD
Proposals 21
Awarded Projects n/a

SingularityNET

Feb. 4, 2026

View RFP

This RFP seeks proposals for the development of an AI-native Development Environment (IDE) that improves the efficiency and accessibility of blockchain application development for the ASI:Chain.

Proposal Description

Our Team

We're a research-engineering team with background in compiler design, type system research, and smart contract verification. Our experience spans Haskell/Plutus formal methods, AI agent orchestration, and production deployment systems. We got interested in MeTTa because its dependent types solve problems we've been wrestling with in contract verification. We bring compiler techniques to the neural-symbolic agent development problem.

Company Name (if applicable)

Lattice Protocol Labs

Project details

Autonomous agents managing real value on-chain need correctness guarantees, not probabilistic code generation. TypeBridge compiles MeTTa type specifications into verified Rholang smart contracts through type-directed synthesis.

**The old way:** Developer writes Rholang contract manually, hopes tests catch bugs, deploys to chain, discovers behavioral issues in production.

**What TypeBridge does:** Developer specifies behavior in MeTTa types, compiler generates Rholang proven correct by Hyperon inference, simulation validates multi-agent interactions, deployment happens with verified safety properties intact.

## Pipeline: Input → Processing → Output

**Input:** MeTTa dependent type specifications expressing agent behaviors within the Atomspace. Example:

```

(: transfer (-> Account Account (Amount >0) (Result (Balance >=0))))

```

This isn't just a function signature. It encodes preconditions (amount must be positive), postconditions (balances never go negative), and invariants that any correct implementation must satisfy. Developers compose these specs from a library of 15+ verified templates covering token operations, oracle interactions, and multi-party protocols.

**Processing:** Type-directed code generator transforms MeTTa specs into Rholang process calculus expressions. This is systematic synthesis, not LLM generation. Each Rholang construct is selected because it satisfies type constraints verified by Hyperon inference. The generator:

- Operates over verified Rholang templates matched to MeTTa type structures

- Uses Hyperon pattern matching to find valid template compositions

- Handles Rholang-specific concerns (name channels, process spawning, CBC Casper state management)

- Verifies compositions preserve correctness properties at each step

**Output:** Rholang contracts deployable to the BlockDAG with formal behavioral guarantees. Correctness isn't tested — it's proven by the type system before the contract touches the chain.

## Three-Layer Architecture

**Layer 1: Intent (MeTTa Types)**

Developers work directly with MeTTa's dependent type system. No abstraction layer hiding the underlying formalism. We provide a curated template library (token transfers, oracle queries, escrow, voting) as starting points. Each template pairs a MeTTa type spec with a verified Rholang implementation and Hyperon-checkable correctness proof.

Developers compose and specialize these templates. The type system ensures compositions are valid. Hyperon inference verifies behavioral properties hold.

**Layer 2: Compilation (Type-Directed Generation)**

The generator is a compiler, not an AI. It performs type-directed synthesis:

1. Parse composed MeTTa specification

2. Match type structure against template library

3. Select Rholang fragments satisfying type constraints

4. Compose fragments while preserving verified properties

5. Use Hyperon inference to validate the composition

6. Generate final Rholang contract with CBC Casper-compatible state handling

Where templates can't be directly composed, Hyperon's pattern matching searches for valid combinations. This is bounded synthesis over a known-correct template space, not unbounded program generation.

**Layer 3: Simulation (Multi-Agent Arena)**

Generated agents run in a scoped simulation: 2-5 agents, deterministic execution, sequential message delivery. The arena operates entirely within the Atomspace, making all state transitions visible to Hyperon inference.

Agents interact through simulated Rholang name channels following formal process reduction semantics. Hyperon verifies multi-agent properties (deadlock freedom, liveness, fairness) during execution — catching bugs that per-agent type checking misses.

Simulation produces Atomspace traces queryable via MeTTa. Developers can ask temporal questions (what happened after event X?), causal questions (what caused state Y?), and property questions (when was invariant Z violated?).

## Why This Works: Bounded Synthesis Over Verified Templates

We're not solving general program synthesis. We're providing a curated library of verified patterns and a compiler that composes them correctly.

The pieces already exist:

- MeTTa's dependent types express behavioral constraints

- Hyperon inference verifies these constraints

- Rholang compiles to the BlockDAG with formal concurrency semantics

- Singularity Compute provides deployment infrastructure

What's missing is the bridge. We build that bridge by scoping aggressively:

**M1 scope:** Compilation pipeline + 15 templates. No simulation, no deployment. Just core type-directed generation with Hyperon verification.

**M2 scope:** Add simulation for 2-5 agents with deterministic interactions. No adversarial testing, no concurrent scheduling. Sufficient to validate template compositions.

**M3 scope:** DevNet deployment, lifecycle management, monitoring. Beta with 10-20 developers.

This is feasible because we're engineering proven components together, not inventing new theory.

## Neural-Symbolic Integration in Practice

The pipeline hybridizes three paradigms:

- **Symbolic:** Type-directed generation reasons about program structure via type constraints

- **Neural:** Template selection uses embeddings in the Atomspace for semantic matching

- **Inference:** Hyperon verifies correctness through pattern matching + logical deduction

No single approach suffices. Their integration through the Atomspace makes verification tractable.

Critical distinction: This isn't AI writing code. It's formal methods verifying that generated code satisfies specifications. LLM output needs human review because the model doesn't understand correctness. TypeBridge output is correct by construction — the type system guarantees it.

## What This Enables

Developers can build verified autonomous agents without expertise in both MeTTa and Rholang. Learn MeTTa types through the template library. See specs become verified contracts. Deploy to DevNet with integrated tooling.

The template library becomes shared infrastructure. As it grows through community contributions, TypeBridge evolves from a tool into ecosystem-wide verified contract patterns for agent development.

Each successful deployment grows the community of developers who understand why neural-symbolic approaches matter for on-chain agent correctness.

Open Source Licensing

MIT - Massachusetts Institute of Technology License

Background & Experience

Links and references

MeTTa Language: https://metta-lang.dev/

Hyperon Implementation: https://github.com/trueagi-io/hyperon-experimental

SingularityNET Ecosystem: https://singularitynet.io/

MeTTa Code Examples: https://github.com/trueagi-io/metta-examples

Activity Summary

Milestones

3

Total

Discussion

0

Total Comments

Reviews

0

Total Posted

Project Team

2

Total People

Total Milestones
3
Total Budget
$40,000_USD
Last Updated
13 Feb 2026

Milestone 1 - Intent-to-Rholang Compilation Pipeline

Description

Milestone 1 delivers the core type-directed compilation pipeline transforming MeTTa dependent type specifications into verified Rholang smart contracts. The pipeline operates over the Atomspace using Hyperon inference to verify that generated Rholang satisfies behavioral constraints encoded in MeTTa types. This milestone focuses exclusively on compilation infrastructure and the template library — no simulation no deployment tooling. The template library provides 15+ verified MeTTa-to-Rholang patterns in three categories: token operations (transfer mint burn approve with balance invariants) oracle interactions (query callback timeout with liveness guarantees) and multi-party protocols (escrow atomic swap voting with safety properties). Each template pairs a MeTTa type specification with a verified Rholang implementation and Hyperon-checkable correctness proof. The type-directed generator accepts composed MeTTa specifications and produces Rholang through systematic type-driven selection of contract fragments. Hyperon inference validates each composition step. The generator handles Rholang-specific concerns including name channel management process spawning and CBC Casper-compatible state management on the BlockDAG.

Deliverables

1. MeTTa Intent Specification Framework: Atomspace library providing dependent types for agent behavioral specification with parameterized types for financial operations communication patterns and state machines. Full documentation with examples. 2. Verified Template Library (15+ templates): MeTTa-to-Rholang pairs covering token operations (5+) oracle interactions (4+) and multi-party protocols (6+). Each includes type spec Rholang implementation Hyperon-verifiable correctness properties and composition rules. 3. Type-Directed Rholang Generator: Compilation engine transforming composed MeTTa intent specs into Rholang contracts via type-directed synthesis. Handles template composition name channel allocation process generation and BlockDAG-compatible state patterns. 4. Hyperon Verification Integration: Pre-generation type checking and post-generation correctness verification via Hyperon inference. Reports detailing which properties hold and which need manual review. 5. Developer Documentation: Step-by-step guide for specifying intents in MeTTa types composing templates generating Rholang and interpreting verification results.

Budget

$8,000 USD

Success Criterion

1. Pipeline Completeness: Generator compiles 15+ distinct MeTTa intent specs into valid Rholang contracts across all three template categories (token, oracle, multi-party). 2. Correctness Rate: Hyperon inference confirms behavioral correctness for 90%+ of generated contracts using library templates. Remainder produces clear diagnostics. 3. Composition Depth: Generator handles 3-level template compositions (e.g., escrow wrapping token transfer wrapping oracle query) with preserved correctness at each level. 4. Error Detection: Pipeline rejects 95%+ of intentionally malformed MeTTa specs (type errors, unsatisfiable constraints, incompatible compositions) with actionable messages. 5. Usability: 3+ developers unfamiliar with the system produce a verified Rholang contract from MeTTa spec within 2 hours in structured evaluation. 6. Performance: Pipeline completes within 60s for single-template specs and 5min for 3-level compositions.

Milestone 2 - Multi-Agent Simulation Arena

Description

Milestone 2 delivers a scoped multi-agent simulation where 2-5 agents from MeTTa type specs interact through simulated Rholang channels within the Atomspace. The arena validates behavioral correctness of agent compositions from the M1 pipeline catching interaction-level bugs that per-agent type checking misses. The arena operates entirely within the Atomspace — all simulation state is accessible to Hyperon inference. Agent interactions follow Rholang's formal operational semantics allowing Hyperon to reason about multi-agent properties (deadlock freedom liveness fairness) during simulation. Scope is deliberately constrained: deterministic execution 2-5 agents sequential message delivery fixed interaction scenarios. No adversarial testing or concurrent scheduling. This ensures tractability while validating critical multi-agent properties. The simulation produces trace logs in the Atomspace recording every state transition and channel communication. Developers query traces using MeTTa. Singularity Compute stub interfaces prepare for distributed simulation.

Deliverables

1. Simulation Engine: Atomspace-native engine instantiating agents from MeTTa type specs executing Rholang channel interactions via formal process reduction. Supports 2-5 agents with sequential delivery and deterministic execution. 2. Scenario Library (8+ scenarios): Bilateral exchange multi-party escrow oracle arbitration token auction voting protocol timeout recovery cascading transitions governance proposals. 3. Hyperon Property Checker: Runtime verification during simulation checking deadlock freedom channel liveness balance conservation protocol completion. Generates violation reports with Atomspace trace references. 4. Trace Analysis Toolkit: MeTTa query interface for simulation traces. Temporal queries (before/after event X) causal queries (what caused state Y) property queries (when was invariant Z violated). Visual sequence diagrams. 5. Simulation CLI/API: Command-line and programmatic interface for running simulations configuring scenarios extracting results. Integrated with M1 pipeline for seamless specify-generate-simulate workflow.

Budget

$28,000 USD

Success Criterion

1. Scenario Coverage: All 8 scenarios execute successfully with M1-generated agents, producing correct traces verified by Hyperon property checking. 2. Detection Accuracy: Property checker identifies 90%+ of intentionally injected violations (deadlocks, balance errors, protocol deviations) across 20+ faulty configurations. 3. Trace Queries: MeTTa queries return results within 5s for simulations of 5 agents and 100 steps. All query types functional. 4. Pipeline Integration: End-to-end from MeTTa spec through generation through simulation completes without manual intervention for template-based compositions. 5. Scalability: Engine handles 5 agents with 200 steps without memory exhaustion or timeout (under 10min). Performance documented. 6. Validation: 5+ developers (2+ external) use the arena to identify and fix a multi-agent behavioral bug in structured evaluation.

Milestone 3 - Lifecycle Management and DevNet Beta

Description

Milestone 3 completes TypeBridge with lifecycle management DevNet deployment and a beta program. This transforms M1-M2 infrastructure into an end-to-end experience: specify in MeTTa generate verified Rholang simulate interactions deploy to DevNet monitor behavior. Lifecycle management: versioning of MeTTa specs with semantic diff tracking upgrade paths preserving Hyperon-verified invariants monitoring mapping on-chain events to MeTTa specs rollback leveraging Rholang's formal model for safe BlockDAG state transitions. DevNet integration: one-command deployment with pre-deployment Hyperon verification against actual DevNet state. Post-deployment monitoring connects on-chain events to the Atomspace for MeTTa-queryable live analysis. Beta program: 10-20 external developers build and deploy agents. Feedback drives documentation template expansion and feature prioritization. Singularity Compute validated through beta workloads.

Deliverables

1. Lifecycle Manager: Version control for MeTTa specs with semantic diffing (behavioral changes not text). Upgrade planner with Hyperon-verified safety. Rollback with formal guarantees. 2. DevNet Pipeline: One-command deployment from MeTTa spec to live contract. Pre-deployment Hyperon verification. CBC Casper-compatible transaction construction. Gas estimation for generated Rholang. 3. Monitoring: Dashboard mapping BlockDAG events to MeTTa behavioral specs. Real-time Hyperon property monitoring. Alerts for behavioral deviations. MeTTa query interface for live analysis. 4. Beta Program: Onboarding for 10-20 developers. Tutorial series for full workflow. Weekly office hours. Issue and feedback documentation. 5. Open Source Release: MIT-licensed release of all components. SingularityNET registry publication. Community template contributions. API docs and developer guide.

Budget

$4,000 USD

Success Criterion

1. DevNet Success: 10+ agent contracts from the pipeline deployed to DevNet executing correctly for 7+ days without violations. 2. Lifecycle: Semantic diff identifies behavioral changes in 90%+ of spec updates. 3+ upgrades on DevNet with Hyperon-verified safety. 3. Monitoring: 95%+ on-chain events correctly mapped to MeTTa specs. Alerts within 60s of detected deviations. 4. Beta Participation: 10+ external developers complete the full workflow. NPS 7+ from participants. 5. Community: Template library grows to 25+ (including contributions). 5+ participants contribute a template or docs improvement. 6. Release: All code MIT-licensed with passing CI, comprehensive docs, 80%+ test coverage on core components.

Join the Discussion (0)

Expert Ratings

Reviews & Ratings

No Reviews Avaliable

Check back later by refreshing the page.

The weighted average of the 4 perspectives Overall

0.0
Each RFP defines a maximum allowed budget, but teams can differentiate their proposal by offering a solution with a lower budget or a wider scope.Value for money

0.0
This rating indicates compliance to 'Must haves' but also adaptation of 'Nice to haves' and Non-functional requirements defined in the RFP.Compliance with RFP requirements

0.0
RFPs will offer varying degrees of freedom. This rating indicates the quality of the team's specific solution ideas, the provided details, and the reviewer's confidence in the team's ability to execute.Solution details and team expertise

0.0

Review Headline

0 /50 chars

Review Summary

0 /5000 chars

The weighted average of the 4 perspectives Overall

0.0
Each RFP defines a maximum allowed budget, but teams can differentiate their proposal by offering a solution with a lower budget or a wider scope.Value for money

0.0
This rating indicates compliance to 'Must haves' but also adaptation of 'Nice to haves' and Non-functional requirements defined in the RFP.Compliance with RFP requirements

0.0
RFPs will offer varying degrees of freedom. This rating indicates the quality of the team's specific solution ideas, the provided details, and the reviewer's confidence in the team's ability to execute.Solution details and team expertise

0.0

Review Headline

0 /50 chars

0 /5000 chars

Warning: Adding final group rating for this project will prevent expert users from adding new or editing existing reviews

Reviews and Ratings in Deep Funding are structured in 4 categories. This will ensure that the reviewer takes all these perspectives into account in their assessment and it will make it easier to compare different projects on their strengths and weaknesses. Overall (Primary) This is an average of the 4 perspectives. At the start of this new process, we are assigning an equal weight to all categories, but over time we might change this and make some categories more important than others in the overall score. (This may even be done retroactively). Feasibility (secondary) This represents the user\'s assessment of whether the proposed project is theoretically possible and if it is deemed feasible. E.g. A proposal for nuclear fission might be theoretically possible, but it doesn’t look very feasible in the context of Deep Funding. Viability (secondary) This category is somewhat similar to Feasibility, but it interprets the feasibility against factors such as the size and experience of the team, the budget requested, and the estimated timelines. We could frame this as: “What is your level of confidence that this team will be able to complete this project and its milestones in a reasonable time, and successfully deploy it?” Examples:

A proposal that promises the development of a personal assistant that outperforms existing solutions might be feasible, but if there is no AI expertise in the team the viability rating might be low.
A proposal that promises a new Carbon Emission Compensation scheme might be technically feasible, but the viability could be estimated low due to challenges around market penetration and widespread adoption.

Desirability (secondary) Even if the project team succeeds in creating a product, there is the question of market fit. Is this a project that fulfills an actual need? Is there a lot of competition already? Are the USPs of the project sufficient to make a difference? Example:

Creating a translation service from, say Spanish to English might be possible, but it\'s questionable if such a service would be able to get a significant share of the market

Usefulness (secondary) This is a crucial category that aligns with the main goal of the Deep Funding program. The question to be asked here is: “To what extent will this proposal help to grow the Decentralized AI Platform?” For proposals that develop or utilize an AI service on the platform, the question could be “How many API calls do we expect it to generate” (and how important / high-valued are these calls?). For a marketing proposal, the question could be “How large and well-aligned is the target audience?” Another question is related to how the budget is spent. Are the funds mainly used for value creation for the platform or on other things? Examples:

A metaverse project that spends 95% of its budget on the development of the game and only 5 % on the development of an AI service for the platform might expect a low ‘usefulness’ rating here.

A marketing proposal that creates t-shirts for a local high school, would get a lower ‘usefulness’ rating than a marketing proposal that has a viable plan for targeting highly esteemed universities in a scaleable way.
An AI service that is fully dedicated to a single product, does not take advantage of the purpose of the platform. When the same service would be offered and useful for other parties, this should increase the ‘usefulness’ rating.

Emilyvas

Project Owner

Project leadership and architecture. Designs the type-directed MeTTa-to-Rholang pipeline and Hyperon inference integration. Ensures neural-symbolic coherence across components.

View Profile

Account Pending

Systems Engineer

Implements Rholang generation engine and simulation arena. Builds DevNet deployment and lifecycle tooling. Handles BlockDAG integration, CBC Casper, and Singularity Compute.

Account Pending