Projects

A = Author, CA = Co-author, C = Contributor

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)

mailbox-actors A (2025) – Formal model of mailbox-based actor systems in Lean 4: actor semantics, message delivery, and system composition. Documentation
avm-lab A (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.
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.
nspec CA (2023-2025) – Anoma specification tooling and MkDocs infrastructure. 100+ PRs.
art CA (2023-2025) – Anoma Research Topics index: LaTeX template, paper editing, Zenodo publication system.

juvix CA (2021-2023) – Functional programming language for intent-centric decentralized applications. Led product direction and shipped 50+ compiler PRs in Haskell.
vscode-juvix A (2021-2023) – VS Code extension for Juvix: syntax highlighting, REPL, CodeLens, hover/typecheck. 50+ releases.
juvix-mkdocs A (2023) – MkDocs plugin for literate Juvix programming with build-time typechecking.
juvix-docs A (2022-2023) – Documentation source for docs.juvix.org.
juvix-stdlib CA (2022-2023) – Juvix standard library and CI setup.
juvix-containers A (2022) – Docker containers for Juvix CI.
homebrew-juvix A (2022) – Homebrew tap for macOS distribution of Juvix.
vamp-ir C (2022) – Release automation for this zero-knowledge circuit language (Rust).

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

agda-mode-vscode C (2021) – Agda mode for VS Code.
hott-cheatsheets A (2019) – Community reference cheatsheets for the HoTT Book. LaTeX.
flask-ponywhoosh A (2015) – Flask extension integrating PonyORM with Whoosh for full-text search. Python.
ponywhoosh A (2015) – PonyORM full-text search via Whoosh. Python.
python-atxt A (2015) – Tool to extract text data from different file formats. Python.
prop-pack A (2017) – Collection of TPTP problems and TSTP solutions for testing automatic provers.
arsi A (2014-2016) – Selection algorithm on rough sets for missing data. Mathematica.
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.