Formal verification framework for distributed mathematical proof validation
Status: experimental — DO NOT USE IN PRODUCTION. No external security audit has been performed.
Website · Spec · Architecture
Contract: 0x877d2f72E4Dc4770bDa62b65245649Dc679CEa02
Nomos is a distributed protocol for collaborative verification of mathematical proofs, with initial focus on computational approaches to the Strong Goldbach Conjecture. Validators run proof-checking nodes that verify submitted proofs against formal specifications and reach consensus on proof validity through a BFT protocol.
The protocol incentivizes honest verification through staking and slashing (RFC-0007) and funds ongoing research via Protocol Tax.
Submitter → P2P Gossip → Validators → BFT Consensus → State Trie
See docs/architecture.md for the full diagram.
| RFC | Title | Status |
|---|---|---|
| 0001 | Protocol Overview | Accepted |
| 0004 | Consensus Mechanism | Accepted |
| 0007 | Slashing Protocol | Accepted |
| 0009 | Proof Sharding | Draft |
| 0011 | State Layout | Accepted |
# requires Rust nightly (pinned in rust-toolchain.toml)
cargo build
cargo test
cargo bench --no-runcargo run -p nomos-cli -- run --config config.tomlNode implementation is WIP. See the CLI for available commands.
| Language | Package | Status |
|---|---|---|
| Rust | sdk/rust |
Types + client stub |
| TypeScript | sdk/ts |
Types + client stub |
| Python | sdk/py |
Types + client stub |
Status: Experimental — opt-in via
ENABLE_ZK=true
| Component | Status |
|---|---|
| Groth16 prover | WIP |
| Proof verification | WIP |
| PLONK backend | Planned |
| Recursive proofs | Planned |
ENABLE_ZK=true cargo run -p nomos-cli -- runNomos assumes ≤1/3 Byzantine validators by stake. See docs/security-model.md for the full threat model.
| Component | Audited |
|---|---|
| Consensus (BFT) | Internal review |
| Slashing engine | Internal review |
| State trie | Not yet |
| ZK module | N/A (WIP) |
External audit planned for Q4 2026.
See CONTRIBUTING.md. Protocol changes require an RFC in spec/.
Dual-licensed under MIT and Apache 2.0.