A = Author, CA = Co-author, C = Contributor  |  archived  |  AI-assisted

Blockchain & EVM

• anoma-explorer A (2026) — Block explorer for Anoma built with Elixir/Phoenix LiveView.
• anoma-envio A (2026) — TypeScript/GraphQL indexer for Anoma events.
• anoma-swap CA (2026) — Token swap interface for Anoma: Phoenix frontend + Rust ZK-proof backend for Resource Machine logic proofs.
• pa-evm C (2026) — Protocol Adapter bridging the Anoma Resource Machine to Ethereum and Arbitrum. Solidity/Rust.
• anomapay-erc20-forwarder C (2026) — ERC-20 Forwarder contract for AnomaPay. Solidity.
• toyevm A (2026) — A 7-day, exercise-driven tutorial for building an Ethereum Virtual Machine from scratch in Rust. (work in progress)

Distributed Systems & Protocols

• mailbox-actors A (2025) — Formal model of mailbox-based actor systems in Lean 4: actor semantics, message delivery, and system composition. Documentation.
• avm-lab CA (2025) — Anoma Virtual Machine: formal Agda specification and Rust implementation with interaction trees, transactional execution, and control flow analysis.
• engine A (2023-2025) — Elixir library implementing the Anoma engine architecture: OTP supervision tree, GenStage messaging, compile-time validated DSL. archived
• dexes A (2025) — HyperCow: SPEEDEX-based decentralized exchange prototype on Anoma (Elixir). 60+ PRs.
• tango A (2024) — Replicated in-memory data structures library in Elixir. archived
• nspec CA (2023-2025) — Anoma specification tooling and MkDocs infrastructure. 100+ PRs. archived
• art CA (2023-2025) — Anoma Research Topics index: LaTeX template, paper editing, Zenodo publication system. archived

Compiler & Language Tooling

• juvix CA (2021-2023) — Strongly-typed, eager-semantics functional programming language for intent-centric decentralized applications. Co-authored from first commit; shipped 50+ compiler PRs in Haskell across the parser, name resolution, termination/positivity checkers, Core IR, and Geb backend. archived
• vscode-juvix A (2021-2023) — VS Code extension for Juvix: syntax highlighting, REPL, CodeLens, hover/typecheck. 50+ releases. archived
• juvix-mkdocs A (2023) — MkDocs plugin for literate Juvix programming with build-time typechecking. archived
• juvix-docs A (2022-2023) — Documentation source for docs.juvix.org. archived
• juvix-stdlib CA (2022-2023) — Juvix standard library and CI setup. archived
• juvix-containers A (2022) — Docker containers for Juvix CI. archived
• homebrew-juvix A (2022) — Homebrew tap for macOS distribution of Juvix. archived
• vamp-ir C (2022) — Release automation for this zero-knowledge circuit language (Rust). archived

Formal Verification & Proof Assistants

• athena A (2017) — Translates Metis ATP proof output into compilable Agda code. Haskell. archived
• online-atps A (2017) — CLI for remote automated theorem provers via SystemOnTPTP. Haskell. archived
• agda-metis A (2017) — Agda formalization of Metis prover reasoning steps. archived
• agda-prop A (2017) — Library for classical propositional logic in Agda. archived
• agda-pkg A (2018-2020) — Package manager for Agda. archived
• agda-unimath C (2020) — 8 merged PRs improving the documentation website. archived
• apia C (2016-2017) — Proof-reconstruction project in Haskell. archived
• HoTT-Book C (2019) — Corrections and contributions to the HoTT Book. archived
• plfa.github.io C (2019) — Programming Language Foundations in Agda. archived

AI-Assisted Projects

Built end-to-end with agentic workflows using Claude Code, opencode, and frontier models (Claude Opus, MiniMax). Each project drove design and implementation while the type checker, tests, and code review stayed in the loop.

• sumabot.online A (2026) production project delivered with AI-assisted workflows. AI-assisted

Other

• agda-mode-vscode C (2021) — Agda mode for VS Code.
• hott-cheatsheets A (2019) — Community reference cheatsheets for the HoTT Book. LaTeX. archived
• flask-ponywhoosh A (2015) — Flask extension integrating PonyORM with Whoosh for full-text search. Python. archived
• ponywhoosh A (2015) — PonyORM full-text search via Whoosh. Python. archived
• python-atxt A (2015) — Tool to extract text data from different file formats. Python. archived
• prop-pack A (2017) — Collection of TPTP problems and TSTP solutions for testing automatic provers. archived
• arsi A (2014-2016) — Selection algorithm on rough sets for missing data. Mathematica. archived
• poirot A (2014-2016) — Text search and analysis platform in Mathematica for large-scale textual data. Developed for Observatorio de Tierras. Source code is private. archived