Formal Verification · Neurosymbolic AI · Language Design

Hyperpolymath

Proving Software Correct, Then Building On It

Dependent types (Idris2) for provable correctness. Neurosymbolic AI (ECHIDNA) for proof synthesis. Original programming languages exploring consent, linearity, and reversibility. All connected through a universal ABI/FFI standard.

300+
Repositories
20+
Arcvix Papers
98
Verified Protocols
PMPL
Palimpsest License
Arcvix papers in many repos — Many of these projects contain arcvix-style papers (look for arcvix-*.tex files) that explain the design logic, the research questions, and what I think makes each approach distinctive. If you want to understand why something is built the way it is, start there.

Feedback very welcome — I would genuinely appreciate feedback on the papers, the code, the architecture, or anything else. Open an issue, send a PR, or just start a discussion. All of it helps.

Formal Verification & Provable Safety

6
proven Core

Formally verified safety library in Idris2 with dependent types. 98 protocol implementations with mathematical correctness proofs. Arcvix paper inside.
proven-servers 98 Protocols

Idris2 ABI + Zig FFI + C headers for 98 network protocols. The universal ABI/FFI standard in practice.
typed-wasm

10-level dependent type safety for WebAssembly memory. Multi-module proofs. Potential arXiv paper.
valence-shell

Formally verified reversible shell. 250+ theorems across 6 independent proof systems (Lean, Coq, Agda, Isabelle, Mizar, Z3). Arcvix paper inside.
ochrance

Neurosymbolic filesystem verification with Idris2 dependent types. Progressive assurance: Lax, Checked, Attested.
januskey

Reversible file operations where data loss is architecturally impossible. Content-addressed storage with transaction support.

Neurosymbolic AI

4
echidna Core

Neurosymbolic theorem prover. Neural proof synthesis accelerates formal verification. Rust + Julia + Idris2. Arcvix paper inside.
hypatia Core

Neurosymbolic CI/CD intelligence engine. Pattern detection, dispatch, and automated remediation across 300+ repos. Arcvix paper inside.
panll

Binary-star neurosymbolic IDE. ReScript TEA frontend, ECHIDNA-powered analysis, 50+ monitoring panels. Arcvix paper inside.
conative-gating

Motivation-aware neural gating for proof search. Intention directs computation. Arcvix paper inside.

Original Programming Languages

6
nextgen-languages 14 Languages

Monorepo of original programming languages: WokeLang, Eclexia, Ephapax, AffineScript, Anvomidav, BetLang, and more. Arcvix papers in several.
ephapax

Region-linear fusion language. Use-once semantics meets region-based memory. 15 Rust crates. Two arcvix papers: Code as Matter + Dyadic Language Design.
wokelang

Consent-aware programming language where data access requires explicit consent declarations. Arcvix paper inside.
language-bridges

FFI bridges between 15 languages via Zig, implementing the Idris2 ABI / Zig FFI universal standard.
affinescript

OCaml-based language with affine types and formal verification integration.
vql-ut

10-level type-safe query language for VeriSimDB. Dependent types ensure query correctness at compile time. Arcvix paper inside.

Developer Infrastructure

6
boj-server MCP Server

Box of Justice MCP server. 70+ cartridges: GitHub, GitLab, Cloudflare, Vercel, Gmail, browser automation, ML, research. The central tool hub.
gitbot-fleet

Bot orchestration: rhodibot, echidnabot, sustainabot, glambot, seambot. Automated scanning, fixing, and PR creation across 300+ repos.
panic-attacker

Security audit tool with Patch Bridge CVE lifecycle management. Formal proofs for mitigation correctness. Arcvix paper inside.
reposystem

Repository management monorepo: contractiles (must/trust/dust/intend/k9), claim-forge, scaffoldia, git-seo, bitfuckit.
stapeln

Logic-driven container security. Chainguard base images, formal verification of container invariants. Arcvix paper inside.
seamstress

Architectural seams as first-class artifacts. Validate, graph, and report on module boundaries across projects.

Databases & Data

3
verisimdb Novel

Octad data model database: graph + vector + tensor + semantic + document + temporal + provenance + spatial. Rust core, Elixir OTP, 6 language SDKs. Arcvix paper inside.
feedback-o-tron

Upstream bug report routing and tracking. Ensures fixes flow back to the right places.
Cliodynamics.jl

Mathematical models of historical dynamics in Julia. Secular cycles, elite overproduction, structural-demographic theory.

Standards, Ethics & Consent

5
palimpsest-license PMPL

The Palimpsest License (PMPL-1.0). Emotional lineage licensing — honouring the history of code. Arcvix paper inside.
rhodium-standard-repositories

The RSR 2026 Standard for repository quality, governance, and compliance. consent-aware-http (HTTP 430) lives here too.
intsoc-transactor

Internet Society document pipeline: check, fix, submit across IETF/IRTF/IAB/IANA streams with consent-aware publication.
union-policy-parser

Labour agreements as executable contracts. Workers' rights need types.
maa-framework

Mutually Assured Accountability. Transparent governance with provable audit trails.

Science & Games

3
idaptik Game

Asymmetric epistemic co-op game. Jessica (platformer) + Q (CCTV/blueprints) never see the same view. ReScript + Rust. Arcvix paper inside.
Cliometrics.jl

Quantitative economic history in Julia. Growth decomposition, convergence analysis, institutional quality indices.
Cladistics.jl

Phylogenetic analysis in Julia. UPGMA, neighbor-joining, maximum parsimony, bootstrap, Newick I/O.