Preamble
Covenant is a smart contract language. Version 0.9 reached General Availability in April 2026, bringing the helper-contract bridge live on Sepolia for the first time. V0.9 introduces helper contracts (CeremonyHelper with a real four-phase state machine; MockedFHEHelper, MockedPQVerifier, MockedZKVerifier with deterministic stubs guarded by an onlyTestnet modifier), ERC-721 auto-synthesis (nft keyword), PQ key registry auto-synthesis (registry keyword), cross-contract calls via interface declarations, a Foundry-class CLI (test, fmt, doctor, coverage, init), and a 6-rule linter with one-click fixes for Solidity-isms. The compiler ships with 22 crates, 1206 passing tests, and zero clippy warnings. Source-level compatibility is preserved across V0.7, V0.8, and V0.9. OMEGA V5 self-audit cleared (independent third-party audit deferred to V1.0). The cryptographic primitives advertised throughout this document — TFHE, Dilithium, Halo2, Wesolowski VDF, Shamir SSS — are designed and integrated at the language and bridge layers in V0.9, with real implementations swapping in at V1.0 alongside mainnet helpers. This document describes the language design, its cryptographic substrate, and the trajectory toward V1.0. The specifications herein are published under CC0-1.0; the compiler is Apache-2.0. We write in the present tense where implementations exist, and in the conditional where they are planned. The reader is invited to distinguish the two.
Why a declarative language for cryptography
A senior Solidity engineer who wishes to deploy a contract with fully homomorphic computation, post-quantum signature verification, and selective disclosure of state must, today, assemble four or more independent libraries, each with its own ABI conventions, gas models, and key serialization formats. The integration code is not checked by any compiler. The bugs live at the joints.
This is not merely inconvenient. It is a structural failure of the toolchain. When a developer writes fhe.decrypt(pk, ciphertext) after a zkVerify(proof, publicInputs), the compiler does not know whether the key used for FHE encryption is the same key identity that the ZK proof asserts. It cannot know, because these primitives are not part of the language; they are external calls. The composition is the developer's responsibility, and the developer is fallible.
Covenant treats FHE, post-quantum signatures, ZK proofs, and cryptographic amnesia as first-class language primitives. The compiler reasons about key identities, data flows, and privacy invariants across all four layers simultaneously. An operation that would violate a privacy guarantee fails at compile time, not at runtime — not in production, not in an audit, not in a postmortem.
"The class of integration bugs that arise from composing independent cryptographic libraries does not exist in Covenant. These bugs cannot be written, because the composition is expressed in the type system."
fn process_private_vote( vote: fhe<u256>, // FHE-encrypted ballot voter: identity<pq> // post-quantum identity ) -> amnesia { // @non_reentrant auto-injected by compiler // privacy flow verified: fhe → pq → zk consistent // compiled to 2,847 bytes let cleartext = decrypt(vote, voter.key); // key identity enforced self.tally(cleartext); } // scope exit: amnesia auto-triggered, ciphertext destroyed, proven on-chain
Architecture: four cryptographic layers
Styx Protocol is Covenant's native standard library — the substrate on which every Covenant contract runs. It is not a dependency to be imported. It is the runtime. Styx defines four named cryptographic layers, each responsible for a distinct class of guarantee. A Covenant contract may use any subset; the compiler verifies that compositions are sound.
The four layers are not independent modules. OBLIVION can trigger termination of keys held by FORTRESS. VEIL's homomorphic computations may be verified by PRISM without decrypting. FORTRESS provides the identity substrate for all three. These interactions are the reason a language-level approach is necessary: no library-level API can express them.
CRYSTALS-Kyber-1024 key encapsulation · Dilithium-5 signatures
TFHE via tfhe-rs · operate on encrypted data without decryption
Nova IVC folding · Halo2 SNARK · selective state disclosure
Shamir SSS · Wesolowski VDF · ZK destruction proofs (real impls V1.0; commitment placeholder V0.9)
What ships today
Version 0.8.2 (V0.8 GA) shipped 25 April 2026. Three targets (EVM default, Aster Chain, WebAssembly), cryptographic amnesia ceremony state machine complete (real cryptography deferred to V1.0), cross-chain bridges functional, and a 15–30 % pGas reduction on FHE-heavy contracts. Source-level compatibility with V0.7 is preserved; OMEGA V4 audit findings remain resolved.
810+ tests · 21+ detectors · VS Code extension · gas-regression baseline
OMEGA V4 V0.6: 41 findings, all resolved. OMEGA V4 V0.8: 9 findings, 8 verified + 1 mitigated. OMEGA V5 V0.9: 10-point self-audit, all GO. Helper-bridge verified end-to-end on Sepolia. 1206 tests, 0 clippy warnings. External third-party audit gates V1.0 mainnet.
Specs CC0-1.0; compiler Apache-2.0; FHE backends are pluggable to avoid scheme lock-in.
--target-chain wasm · deterministic · wasmparser-clean
SHIPPED · V0.9
Same .cov source compiles to EVM, Aster Chain, and WebAssembly. Browser and server-side sandboxes (wasmtime, wasmer) run Covenant contracts with an auditable output.
bridge … anchored_on [...] synthesizes four canonical functions per chain and emits one artifact per anchored chain with the correct local_chain() baked in.
Playground
Covenant ships a complete in-browser development environment at playground.covenant-lang.org. The playground loads in any modern browser — no Rust, no PATH setup, no toolchain. Compile to real EVM bytecode, deploy to MockChain (deterministic, instant) or Sepolia (real testnet, ~12–24 s block confirmation), interact with deployed contracts in a typed UI, persist state across reloads via IndexedDB, and follow a guided 20-lesson tour (4 modules: basics, privacy, advanced, V0.9 features) from record Hello to amnesia ceremony, NFT auto-synthesis, and Sepolia deploy.
record Hello through encrypted ballot, ceremony destruction, NFT mint.
State persists across page reloads (IndexedDB) and syncs across tabs (BroadcastChannel). Events display as human-readable names, not raw hex topics. The playground is the fastest way to evaluate Covenant — and the recommended on-ramp for anyone considering adoption.
Trajectory
What follows is the public roadmap. Shipped phases are marked accordingly. The current phase is distinguished by a live indicator on the left margin.
The Covenant compiler ships in Rust. Core language semantics are implemented and tested. The first public contract deploys on Ethereum Sepolia.
The Codex establishes the Covenant idiom across Basics, Intermediate, Advanced, and Edge Cases. Each example is tested and annotated.
The CLI provides compile, check, deploy, and test subcommands. 810+ tests cover the full language surface. Minimal and composable by design.
LSP v1 brings Covenant to VS Code and any LSP-compatible editor (hover, go-to-definition, completion, formatting). The security linter ships with 21+ detectors covering the most common classes of cryptographic misuse.
The 0.7.x language spec is frozen. OMEGA V4 self-audit complete with all critical/high findings resolved (independent third-party audit deferred to V1.0). Styx Protocol ERC drafts (PQ Registry, FHE primitives, ZK selective disclosure, Amnesia ceremony) normative — note that EIP-8228 has since been officially assigned to the unrelated Styx Encrypted Token Standard; the Covenant ceremony is no longer attached to that EIP number. Documentation, 30 cookbook recipes (auth, integration, privacy, testing, tokens, upgrades), and Solidity migration guide are production-ready.
Deterministic WASM codegen for browser and server-side sandboxes. Wesolowski VDF, Shamir secret sharing, and keccak-bound destruction proofs — all externally verifiable without the Covenant toolchain. Rolled into V0.8 GA.
Per-pair nonce anti-replay, validator-set Merkle commitments, threshold ECDSA attestations, and one artifact per anchored chain. FHE coalescing plus compile-time hash precomputation deliver 15–30 % pGas reduction on FHE-heavy contracts. Rolled into V0.8 GA.
V0.8 consolidated V0.7.1 and V0.7.2 into a single GA milestone. Three targets (EVM, Aster Chain, WebAssembly). Cryptographic amnesia complete via dedicated precompiles at 0x124–0x127. Bridge module synthesizes per-chain artifacts. Fully backward compatible at the source level; OMEGA V4 audit findings remain resolved.
V0.9 is the helper-bridge release. The helper-contract bridge brings Covenant constructs to live Sepolia execution: CeremonyHelper ships a real four-phase state machine; MockedFHEHelper, MockedPQVerifier, MockedZKVerifier ship deterministic stubs guarded by an onlyTestnet modifier (real cryptography lands in V1.0). Three new top-level constructs: nft (ERC-721 auto-synthesis, 11 functions from 5 lines of source), registry (PQ key registry, 5 functions), interface (typed cross-contract calls). Foundry-class CLI: covenant test/fmt/doctor/lint/init/explain with per-test isolation and name-heuristic coverage (IR-instrumented coverage in V0.9.x). 6-rule linter for Solidity-isms. OMEGA V5 self-audit cleared (10-point internal audit, all GO; independent third-party audit deferred to V1.0). 1206 tests passing. M0 (record Hello), M1 (ceremony destruction commitment), M2 (auto-synth ERC-721 NFT, full 5-tx lifecycle) all verifiable on Sepolia Etherscan. This is the current active phase.
--strict doctor, LSP debounce on incremental edits, IR-level coverage, and continuous fuzz campaigns. Aster M2 (live deployment) gated on Aster Chain factory verification — codegen ready, deploy waits.
V1.0 lights up real cryptographic primitives — Zama TFHE in CeremonyHelper, real Dilithium-5 verifier in PQHelper, Halo2 on-chain in ZKHelper. External audit by a third-party firm (Trail of Bits, OpenZeppelin, or equivalent) covers the WASM backend, helper bridge, and async action semantics. Mainnet helper deployment. Partial formal verification (privacy flow soundness in Coq/Lean). Semantic versioning guarantee takes effect: no breaking changes without a major version increment. 3+ production protocol deployments validate the model.
Coq and Lean proofs of the Covenant type system's key invariants. A mechanically verified proof that the privacy flow checker is sound relative to the operational semantics. We state the goal here as a public commitment.
Why Covenant is not another smart contract language
The question arises. A number of projects have occupied adjacent positions. The distinctions are not trivial.
Not another Solidity fork. Solidity is the runtime we target. Covenant compiles to EVM bytecode via the same backend. But Covenant is not a dialect of Solidity, nor a superset, nor a compatibility layer. It is a different language with a different type system and different compiler semantics.
Not an FHE-specific DSL. fhEVM and its contemporaries specialize in fully homomorphic computation. They solve one problem well. Covenant treats FHE as one primitive among four: post-quantum key infrastructure, fully homomorphic computation, zero-knowledge verification, and cryptographic amnesia. The integration between these four layers is where the most dangerous bugs live.
Not a research toy. A contract runs on Sepolia today. The CLI accepts input and produces bytecode. The linter catches bugs in real Covenant code. The VS Code extension syntax-highlights and autocompletes. This is not a paper describing a language that might one day be implemented. It is working infrastructure.
How to read this document
This site is both a project document and a living specification. The sections on language design and architecture are normative: any deviation between the compiler and this document is a compiler bug. The roadmap sections are informative: they describe our intentions, which are subject to revision.
We distinguish two kinds of sections explicitly, via badges next to each section number:
- Foundational — the permanent argument: what Covenant is, why a language-level approach, the four-layer architecture of Styx Protocol. These sections change only when the philosophy changes, which is rarely.
- Living · V0.9 — the current state: what has shipped, what is in flight, what is planned. These sections update with each release. The pulsing indicator marks the active version.
When you read this manifesto, the Foundational sections describe what we are building and why. The Living sections describe where we are on the road to V1.0. Together they form a single document — but they evolve on different timescales.
The specifications published here are released under CC0-1.0. You may use them, fork them, implement them independently, and publish derivative work without attribution. The compiler implementation is released under Apache-2.0.
Invitation to contribute
Covenant is early. We have a working compiler, a deployed contract, a test suite, and a roadmap. We are selectively seeking collaborators in four areas.
Rust engineers with experience in type systems, compiler backends, or formal semantics. Particularly interested in MIR-style intermediate representations or incremental compilation.
Cryptographers with depth in lattice-based post-quantum constructions, FHE schemes, or recursive SNARK proof systems. The Styx Protocol interface definitions are open; formal critique is welcome.
Smart contract auditors who can stress-test the language semantics — the privacy flow checker, the reentrancy model, the amnesia scope rules. Break it before it ships.
Mathematicians working in Coq, Lean, or Isabelle interested in mechanizing the Covenant type system soundness proof. The longest-horizon contribution; also the most consequential.
On compensation
Covenant has no venture funding and no token. There is currently no paid position available for contributors. We acknowledge this openly — the project cannot pay competitive market rates today, and we do not ask collaborators to pretend otherwise.
What we can offer
- Authorship — every technical contribution is credited publicly in release notes, documentation, and academic publications produced from this work.
- Research visibility — Covenant operates in the open. Contributors build a verifiable portfolio on a project of non-trivial technical ambition.
- Priority consideration for future paid roles — when funding becomes available (whether via grants, foundation support, or consulting revenue), contributors who shipped meaningful work receive first refusal on paid positions.
- Reference letters — for academic and industrial applications, we provide detailed reference letters documenting the specific technical work completed.
- Access to the production codebase — vetted contributors receive read/write access to the private V0.9 working branches of the 22-crate compiler workspace, the WASM and Aster backends, the helper-contract bridge, and unreleased protocol drafts, ahead of public publication. The signal of seriousness is access.
What we cannot offer
- Competitive salaries or hourly rates.
- Equity, revenue share, or token allocation.
- Guarantees about future paid work.
If this arrangement doesn't align with your constraints, we understand. Covenant is not for everyone at this stage, and we would rather you commit your time to work that compensates you properly than contribute with unvoiced expectations.
For contributors whose interest is fundamentally in the work itself — the research, the systems design, the opportunity to shape a language from first principles — we welcome you. The road from V0.1 to V1.0 is long and technically substantive. Every serious contribution will be acknowledged as such.
Reach out: covenant@kairos-lab.org
Contact
Watch this space. Private until V1.0.