Junaid Rasheed

Software Engineer

Software Engineer at IOHK building the future of decentralized finance on Cardano. I specialize in Haskell and TypeScript, with deep experience in blockchain protocols, property-based testing, and formal verification. Previously led engineering teams at PRODA, delivering high-impact systems that drove measurable business outcomes. PhD in Computer Science with published research on automated verification of floating-point programs.

GitHub LinkedIn Email

Experience

Software Engineer

IOHK

July 2025 – Present

United Kingdom

  • Designed and implemented scalable ETL pipelines to capture reward-eligible dApp user events, streaming DynamoDB data to S3, applying Parquet transformations across bronze/silver/gold layers, and loading curated datasets into Snowflake to power reward attribution and analytics.
  • Leading the design and implementation of multisig support for the project's dApp to enable institutional custody workflows and unlock participation from institutional investors.
  • Implemented cross-network bridging functionality for an upcoming Cardano project, enabling assets to be securely bridged from external chains into the Cardano ecosystem to reduce user friction and support increased liquidity and TVL.
  • Implemented an EVM-based stablecoin (including an ERC-4626-compliant implementation) and the supporting indexing infrastructure, including technology selection, data model design, and infrastructure setup for activity tracking and reward attribution.
  • Led significant improvements to the testing strategy for the DJED stablecoin, implementing a comprehensive suite of property-based tests designed to attack the protocol across hundreds of scenarios with precise on-chain failure assertions.

Engineering Lead

PRODA

April 2025 – July 2025

London, United Kingdom

  • Tech Lead for the ingestion team, managed agile processes, provided status reports to executives, and drove strategic direction while maintaining significant hands-on technical contributions.
  • Managed team members from junior to senior levels, giving regular one-to-one meetings and performance reviews, driving improvements across cross-functional teams.

Full Stack Engineer

PRODA

March 2023 – April 2025

London, United Kingdom

  • Designed and implemented automated OpenAPI spec generators for our Haskell monolith, reducing lead times from 6–7 days to 3–4 days for new TypeScript teams. This work directly contributed to the creation of several high-impact TypeScript services, generating new sales opportunities and increasing ARR.
  • Developed an automated versioning and publishing system for our generated specs that integrates with our CI/CD pipelines, ensuring seamless deployments and consistency across services.
  • Spearheaded a scalable greenfield TypeScript project to replace an outdated ETL automation system. Reduced processing times from 5 minutes to 1 minute, with around 30% of all data uploads now processed by the new service. Reliability improved significantly, reducing the failure rate to less than 1%.
  • Built a robust SFTP-based ingestion service using GCP (with GCS for storage and a TypeScript Cloud Run function) deployed via Terraform and GitHub Actions. Collaborated closely with Business Analysts, product managers, and clients.
  • Implemented k6 load testing with TypeScript to automate testing of our main Haskell service. Identified performance bottlenecks, leading to a 10–20% reduction in ingestion times and enabling a 240% increase in data throughput.

Computer Science Teaching Assistant

Aston University

January 2018 – December 2022

United Kingdom

  • Delivered tutorials and marked exam papers for 'Programming Language Concepts' and 'Data Structures and Algorithms' modules over 5 years.
  • Led tutorials for 'Software Project Management' and 'Multi-Agent Systems' modules for 2 years.

Web Developer

Mobile Fun / magic42

July 2016 – June 2018

United Kingdom

  • Developed and maintained Magento websites for Mobile Fun and magic42 clients.
  • Implemented Jenkins and Puppet scripts for automatic deployment, continuous integration, and backup of Magento websites.
  • Worked full-time during placement year (July 2016 – September 2017) and part-time during final year of undergraduate degree (October 2017 – June 2018).

Projects

PropaFP

Author

A state-of-the-art tool for auto-active verification of floating-point programs. Uses a novel process combining symbolic simplifications, interval arithmetic, and nonlinear real provers to verify numerical programs against tight error bounds.

Haskell 8

simplex-method

Author

A Haskell library implementing the two-phase simplex method in exact rational arithmetic. Currently being refactored to enhance performance, code quality, and extensibility.

Haskell 6

LPPaver

Author

An automated prover targeting problems that involve nonlinear real arithmetic. Implements novel algorithms using numerical methods and is comparable to state-of-the-art provers.

Haskell 5

sc-tools

Contributor

A collection of Haskell libraries for building Cardano applications. Includes coin selection, transaction balancing, a minimal wallet implementation, mockchain for testing, and a CLI tool for transaction analysis.

Haskell 18

aern2

Contributor

A Haskell library for Approximating Exact Real Numbers (AERN) based on interval computation. Provides arbitrary-precision real number arithmetic with guaranteed error bounds.

Haskell 25

exact-function-plotter

Contributor

An exact-real function plotter in the browser. Visualizes mathematical functions with guaranteed precision using exact real arithmetic.

Haskell 1

Publications

thesis 2022

Automatic Numerical Proving for Auto-active Verification of Floating-Point Programs

Junaid Rasheed

PhD Thesis, Aston University

Developed novel methods for automatic numerical proving and auto-active verification of floating-point programs. The research produced two open-source tools: LPPaver for automated proving of nonlinear real arithmetic, and PropaFP for verification of floating-point programs.

PDF
paper 2022

Auto-active Verification of Floating-point Programs via Nonlinear Real Provers

Junaid Rasheed, Michal Konečný

SEFM 2022 - Software Engineering and Formal Methods

We give a process for verifying numerical programs against their functional specifications. Our implementation is capable of automatically verifying programs against tight error bounds featuring common elementary functions. We demonstrate and evaluate our implementation on several examples, yielding the first fully verified SPARK implementations of the sine and square root functions.

PDF arXiv Journal

Skills

Languages

Haskell TypeScript JavaScript Python C#

Backend & DevOps

GCP Terraform Kubernetes Docker CI/CD Datadog

Expertise

Functional Programming Blockchain Development Event-Driven Architecture Formal Verification Full Stack Development Software Design

Leadership

Team Management Agile Scrum Project Management Mentorship

Education

PhD in Computer Science

Aston University

October 2018 – March 2023

Sponsored by AdaCore. Thesis titled "Automatic Numerical Proving for Auto-active Verification of Floating-Point Programs". Developed performant novel methods for automatic numerical solving, implemented in LPPaver and PropaFP.

BSc in Computer Science

Aston University

October 2014 – July 2018

First Class (83%)

Received the Best Student Award for the highest performance among my cohort in the final year.