IntersectContent & Educationhydra
Formal Verification in Lean 4 and Blaster — Cardano Auditor Training Program 2026
No Witness Labs
ID: 69fd84b3b05ff80adc7d5c58
An eight-session intensive auditor-training programme covering Lean 4 programming, type theory and Curry–Howard intuition, theorem proving, SMT integration via Blaster, EUTxO contract modelling, and a complete practical audit workflow culminating in each learner producing a reproducible Lean 4 + Blaster audit of a non-trivial smart contract. Two live cohorts of 25–30 learners across 12 months; full curriculum released MIT-licensed in Q3.
Ask (ADA)
618,000
Ask (USD)
$154,500
Peg
$0.25
Eff. ADA @ spot
583,900
Peg vs market
—
Scorecard
7 of 19 criteria answered
Amber · 100%· pending review
How this score works
Each criterion is worth between 1 and 4 points. The score is the points earned out of the points on criteria that have been answered — shown as a percentage. Green is 75% or higher, Amber is 50–74%, and Red is below 50%.
Some criteria are checked automatically against the proposal data (open source, doxxed team, treasury return clauses, etc.). Others are human-judgment calls — value for money, public good, whether the deliverables are realistic. Those stay blank until a DRep ticks them.
Criteria can also be marked Not applicablewhen they don't fit the proposal — for example, "open source" doesn't apply to a DAO governance proposal with no software output. Those are excluded from the score entirely, neither helping nor hurting.
Green requires 80% coverage. If less than 80% of the applicable criteria (by points) have been answered, the verdict stays at Amber — "pending review" — even when every answered criterion passes. This proposal's coverage is currently 38% (7 of 19 applicable criteria answered). The auto-calculated band would have been Green, but coverage is below the threshold so the verdict is shown as Amber to flag that judgment criteria are still pending.
Vote intent
Export & audit
↓ Download scorecard.mdRaw payload · Treasury (true) / Admin (—)
{
"schema_version": "1.0.0",
"id": "hydra-nowitness-lean4-auditor-training",
"ingestion": {
"ingested_at": "2026-05-11T14:30:00Z",
"ingested_by": "claude-opus-4.7",
"source_documents": [
"Hydra proposal page (pasted) — Proposal ID 69fd84b3b05ff80adc7d5c58"
],
"extraction_notes": "All fields populated from proposer-supplied Hydra text. Pillar 4 stated as primary; Pillars 1 and 2 stated as secondary/supporting. Repayment language is conditional residual-return, not revenue-share. Lead instructor bio includes a literal [FILL — Irfan's bio: ...] placeholder in the source text — flagged in metadata. Proposer entity given as 'No Witness Labs' on Hydra form but the body uses both 'No Witness Labs LLC' and 'No.Witness Labs' interchangeably."
},
"source": {
"channels": [
"hydra"
],
"hydra_id": "69fd84b3b05ff80adc7d5c58",
"onchain_tx_hash": null,
"onchain_action_id": null
},
"identity": {
"title": "Formal Verification in Lean 4 and Blaster — Cardano Auditor Training Program 2026",
"proposer_name": "No Witness Labs",
"proposer_type": "organisation",
"proposer_url": "https://nowitnesslabs.com",
"doxxed": true,
"primary_contact": "Irfan Ali (lead instructor); Jonathan Rodriguez (CEO); Mladen Lamesevic (COO)",
"team_size_disclosed": 7,
"team_size_disclosed_note": "Named team: Jonathan Rodriguez, Mladen Lamesevic, Irfan Ali, Vu, Mazen, Nikhil Shetty, Thuy. Funded roles in this proposal: Irfan Ali (~0.5 FTE), 1 TA, 1 coordinator (~0.2 FTE)."
},
"classification": {
"official_pillar": "Community & Ecosystem Growth",
"official_pillar_confidence": "stated",
"working_category_suggestion": "Content & Education",
"working_category_confidence": "high",
"tags": [
"formal-verification",
"auditor-training",
"lean4",
"smart-contract-security",
"education",
"open-source",
"osc-tsc-incubation"
]
},
"ask": {
"ada_amount": 618000,
"ada_amount_note": "Total including 18,000 ADA Intersect administration fee. Work package itself is 600,000 ADA.",
"usd_amount": 154500,
"usd_peg_price": 0.25,
"pegged": true,
"currency_basis": "usd_pegged",
"duration_months": 12,
"milestone_count": 4,
"milestone_payments_disclosed": true,
"raw_ask_text": "Requested budget: 618,000 ADA. USD equivalent $154,500 (ADA/USD 0.25)*. This conversion rate was specified by the proposer. Total work package budget 600,000 ADA / $150,000 (ADA/USD 0.25). Intersect Budget Administration fee 18,000 ADA / $4,500. Total budget 618,000 ADA / $154,500."
},
"treasury_return": {
"has_return_clause": true,
"types": [
"unspent_funds"
],
"expected_return_pct": null,
"expected_return_pct_note": "No fixed percentage. Conditional residual return: unspent contingency reserve, unfinished milestone funds, and unfilled-cohort variable costs return to treasury. No revenue share (all deliverables MIT public good).",
"raw_return_text": "Yes — conditionally. No profit-sharing or revenue-share return (all deliverables are public-good open-source artifacts under MIT, with no tuition fee charged to learners and no commercial revenue stream attached), but residual unspent ADA is returned to treasury under the conditions below. Repayment is conditional and triggered by the following circumstances: Scope cannot be completed... Engagement terminated early... Cohort fill below threshold... Contingency reserve unused. The 20,000 ADA contingency reserve is held in reserve. If unspent at the end of the engagement, the remaining balance is returned to the Cardano Treasury. Milestone-slip policy. Each milestone has a 30-day grace window."
},
"lifecycle": {
"pipeline_state": "hydra_early",
"hydra_submitted_at": "2026-05-08T07:07:00Z",
"hydra_close_at": null,
"hydra_support_pct": null,
"onchain_submitted_at": null,
"onchain_vote_close_at": null,
"onchain_result": null,
"status_last_checked_at": "2026-05-11T14:30:00Z"
},
"links": {
"hydra_url": null,
"adastat_url": null,
"ipfs_cid": null,
"ipfs_gateway_url": null,
"github_url": "https://github.com/no-witness-labs/formal_verification_lean4_course",
"website_url": "https://nowitnesslabs.com",
"forum_thread_url": null,
"other": [
{
"label": "NoWitness Labs X",
"url": null
},
{
"label": "Catalyst Fund 14 project #1400085 (Hydra Manager) — milestone tracker",
"url": "https://milestones.projectcatalyst.io/projects/1400085"
},
{
"label": "Evolution SDK incubation page",
"url": "https://committees.docs.intersectmbo.org/intersect-open-source-committee/policies/project-incubation-process/incubated-projects/evolution-sdk-no-witness-labs"
},
{
"label": "Intersect news — Evolution SDK enters incubation",
"url": "https://intersectmbo.org/news/intersect-no-witness-labs-evolution-sdk-enters-incubation"
}
]
},
"content": {
"abstract": "An eight-session intensive auditor-training programme covering Lean 4 programming, type theory and Curry–Howard intuition, theorem proving, SMT integration via Blaster, EUTxO contract modelling, and a complete practical audit workflow culminating in each learner producing a reproducible Lean 4 + Blaster audit of a non-trivial smart contract. Two live cohorts of 25–30 learners across 12 months; full curriculum released MIT-licensed in Q3.",
"problem_statement": "Cardano's biggest off-chain risk is unaudited or under-audited smart contracts; the bottleneck is the small number of engineers who can perform formal-verification-grade audits. Cardano cannot scale TVS on smart contracts faster than the auditor population that can verify them.",
"proposed_solution": "Fund a structured 12-month auditor training programme taught in Lean 4 augmented by Blaster (SMT delegation to Z3), led by Irfan Ali. Two live cohorts of ~25–30 selected learners. Curriculum hardened to publication standard (Q1), Cohort 1 delivery (Q2), open-source release + Cohort 2 intake (Q3), Cohort 2 delivery + cumulative impact report (Q4). All materials MIT-licensed, governed under Intersect OSC/TSC incubation framework.",
"deliverables": [
"8-session curriculum hardened to publication standard",
"Two live cohorts of 25–30 learners each (≥40 graduates total at ≥80% completion)",
"Public MIT-licensed curriculum repo: 8 sessions, exercises, recordings, reproducible Nix dev environment, worked-example audit artifacts",
"≥40 reproducible Lean 4 + Blaster audit artifacts (one per graduate's final project)",
"Public auditor-graduate roster on curriculum repo (opt-in)",
"Bi-weekly community office hours during cohort active weeks",
"Quarterly OSC/TSC reviews and progress reports",
"Cumulative impact report at M4"
],
"milestones": [
{
"name": "Milestone 1",
"deliverable": "Curriculum Foundation: 8-session materials hardened, infrastructure live, Cohort 1 intake",
"ada_release": null,
"deadline": null
},
{
"name": "Milestone 2",
"deliverable": "Cohort 1 Delivery: 8 live sessions, recordings published, final-project showcase",
"ada_release": null,
"deadline": null
},
{
"name": "Milestone 3",
"deliverable": "Open-Source Release + Cohort 2 Intake",
"ada_release": null,
"deadline": null
},
{
"name": "Milestone 4",
"deliverable": "Cohort 2 Delivery + Cumulative Impact Report",
"ada_release": null,
"deadline": null
}
],
"team": [
{
"name": "Jonathan Rodriguez",
"role": "CEO — Program sponsor; cross-engagement coordination",
"background": "Long-standing TypeScript and Cardano off-chain experience"
},
{
"name": "Mladen Lamesevic",
"role": "COO — Program operations, OSC/TSC liaison",
"background": null
},
{
"name": "Irfan Ali",
"role": "Lead instructor (curriculum author)",
"background": "Bio left as [FILL] placeholder in source proposal"
},
{
"name": "Vu",
"role": "Developer / TA capacity",
"background": null
},
{
"name": "Mazen",
"role": "Developer / TA capacity",
"background": null
},
{
"name": "Nikhil Shetty",
"role": "Developer / TA capacity",
"background": null
},
{
"name": "Thuy",
"role": "Developer / TA capacity",
"background": null
}
],
"risks_disclosed": [
"Cohort fill risk — minimum 15 learners per cohort; below threshold triggers scope renegotiation and partial return",
"Milestone slip risk — 30-day grace window with pause option for Intersect"
]
},
"metadata": {
"open_source": "yes",
"open_source_url": "https://github.com/no-witness-labs/formal_verification_lean4_course",
"has_prior_funding": true,
"prior_funding_sources": [
"Project Catalyst Fund 14 — project #1400085 (Hydra Manager, 81,000 ADA, 26,400 ADA distributed to date)",
"Intersect OSC + TSC incubation (non-monetary, Evolution SDK)"
],
"has_prior_delivery": true,
"prior_delivery_evidence": "Catalyst F14 milestone-administered delivery (active); existing formal_verification_lean4_course repo; audit firm track record: 320+ vulnerabilities found, $500M+ value protected, 18 protocols secured, zero post-audit exploits",
"is_administered_by_intersect": true,
"administration_fee_pct": 3,
"duplicate_of_existing_solution": "unknown",
"duplicate_notes": "Proposer claims existing formal_verification_lean4_course repo is the only Lean 4 Cardano auditor curriculum; no other formal-verification training programme cited in Cardano space. Worth verifying against Plutus Pioneer and Aiken training programmes."
},
"_meta": {
"title": "Formal Verification in Lean 4 and Blaster — Cardano Auditor Training Program 2026",
"proposer": "No Witness Labs"
}
}