Skip to content

@NyxFoundation NyxFoundation

Change the repository type filter

All

    Repositories list

    45 repositories

    • speca-lean4-plugin

      Public
      Python
      •0•0•3•1•Updated Aug 15, 2026Aug 15, 2026

    • verity

      Public
      The Provable Consensus Client — a formally verified Ethereum consensus client built with Lean 4.
      Rust
      •
      MIT License
      •0•14•0•1•Updated Aug 15, 2026Aug 15, 2026

    • gasper-lean4

      Public
      Formal Verification of Gasper in Lean 4
      JavaScript
      •
      MIT License
      •0•0•0•0•Updated Aug 14, 2026Aug 14, 2026

    • ethereum-vuln-dataset

      Public
      Curated corpus of past security fixes from the 11 Ethereum clients (vulnerability-only, STRIDE/CWE-labeled, relevance-scored)
      Python
      •
      Other
      •1•3•0•0•Updated Aug 13, 2026Aug 13, 2026

    • wallet-vuln-dataset

      Public
      Curated corpus of past security fixes from crypto wallet repositories — silent-fix heavy, custody threat model
      Python
      •
      Other
      •0•2•0•0•Updated Aug 13, 2026Aug 13, 2026

    • eris-agent-simulator

      Public
      TypeScript
      •
      MIT License
      •2•11•14•0•Updated Aug 12, 2026Aug 12, 2026

    • speca

      Public
      SPECA: Specification-to-Checklist Agentic Auditing Framework
      Python
      •
      MIT License
      •29•454•24•2•Updated Aug 12, 2026Aug 12, 2026

    • docs2formalspec

      Public
      Docs → RFC2119 spec + Lean4 formal verification, via local-class LLMs
      Lean
      •
      MIT License
      •0•17•0•0•Updated Aug 11, 2026Aug 11, 2026

    • skills

      Public
      Single source of truth for Nyx Foundation agent skills (hermes / Claude Code / workspace agents)
      Python
      •
      MIT License
      •0•0•0•0•Updated Aug 5, 2026Aug 5, 2026

    • formal-leanSpec

      Public
      Lean
      •0•2•5•1•Updated Jul 30, 2026Jul 30, 2026

    • rlmd-ghost-fv

      Public
      Formal-verification reference notes for the RLMD-GHOST consensus protocol (arXiv:2302.11326, CSF 2024)
      Lean
      •0•0•0•1•Updated Jul 29, 2026Jul 29, 2026

    • minimmit-fv

      Public
      Formal-verification reference notes for the Minimmit consensus protocol (arXiv:2508.10862, FC'26)
      Lean
      •0•1•1•1•Updated Jul 29, 2026Jul 29, 2026

    • leanSSZ

      Public
      Formally verified SSZ library in Lean 4 for the Lean Ethereum consensus spec (leanSpec)
      Lean
      •0•1•1•0•Updated Jul 28, 2026Jul 28, 2026

    • goldfish-fv

      Public
      A Lean formalization of the Goldfish consensus protocol (IACR ePrint 2022/1171)
      Lean
      •0•0•0•1•Updated Jul 26, 2026Jul 26, 2026

    • simplex-fv

      Public
      Formal-verification reference notes for the Simplex consensus protocol (IACR ePrint 2023/463)
      Lean
      •0•0•0•1•Updated Jul 25, 2026Jul 25, 2026

    • kurtosis-harness

      Public
      Finding-driven, client-agnostic reproduction harness for Ethereum-client audit findings (Kurtosis devnet, guarded negative control)
      Python
      •
      MIT License
      •0•0•0•0•Updated Jul 25, 2026Jul 25, 2026

    • lean4-speedup

      Public
      Making Lean 4 compilation faster on CPU — profiling, 3D-visualized architecture, and verified cache inventions (visioned vibe coding loop)
      Lean
      •0•0•0•0•Updated Jul 20, 2026Jul 20, 2026

    • visually-3d

      Public
      A platform to visualize machinery from blueprints/names in 3D, learn about part composition, connectivity, and roles.
      Python
      •
      MIT License
      •1•3•0•0•Updated Jul 19, 2026Jul 19, 2026

    • presentation-agent

      Public
      JavaScript
      •
      MIT License
      •4•0•0•16•Updated Jul 17, 2026Jul 17, 2026

    • interests

      Public
      NyxFoundation メンバーのリサーチアイデア・興味トピックの蓄積場所。誰でも閲覧・コメント可能。issueはメンバー管理。
      0•2•29•0•Updated Jul 17, 2026Jul 17, 2026

    • FoldNTT

      Public
      FoldNTT — a new, formally-verified, DSP-minimal NTT accelerator for Falcon/Proth primes; on-board Basys 3 demo, entirely Vivado-free (yosys + openXC7)
      Python
      •
      MIT License
      •0•3•0•0•Updated Jul 6, 2026Jul 6, 2026

    • consensus-ffi-poc

      Public
      Lean 4 formalization of Lean Consensus (3SF-mini) — generated from Rust via Aeneas
      Lean
      •
      MIT License
      •0•2•13•3•Updated Jun 27, 2026Jun 27, 2026

    • verifiable-stf

      Public
      Rust
      •0•0•2•2•Updated Jun 11, 2026Jun 11, 2026

    • eris-website

      Public
      HTML
      •0•0•0•1•Updated May 11, 2026May 11, 2026

    • verity-site

      Public
      HTML
      •
      MIT License
      •0•0•1•1•Updated May 4, 2026May 4, 2026

    • lean-atlas

      Public
      TypeScript
      •
      MIT License
      •1•18•1•0•Updated May 3, 2026May 3, 2026

    • nyx-website

      Public
      HTML
      •0•0•0•0•Updated Apr 30, 2026Apr 30, 2026

    • bb-crypto-inventory

      Public
      Blackbox Cryptographic Inventory Tool - LLM-agent-driven automated crypto asset discovery and vulnerability detection using only endpoint URLs
      Python
      •
      MIT License
      •1•0•0•1•Updated Apr 24, 2026Apr 24, 2026

    • lean4-client-proto

      Public
      Lean4 implementation of an Ethereum consensus client for pq-devnet-3 (3-Slot Finality, XMSS, leanMultisig)
      Lean
      •
      MIT License
      •0•0•0•0•Updated Apr 18, 2026Apr 18, 2026

    • lean-atlas-deprecated

      Public
      TypeScript
      •
      MIT License
      •0•0•0•0•Updated Mar 16, 2026Mar 16, 2026
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.