the provable
language

hello, proof

program hello_proof

fn main() -> Field {
    let a: Field = divine()
    let b: Field = divine()
    a + b
}

$ trident build hello.tri --costs
  Compiled -> hello.nox
  reductions: 32..=96 (branch-dependent)
$ trident prove hello.tri --secret 7,13
  Proved private execution (Triton ZK) in 1621 ms:
  32 reductions, 817612 bytes
  Output: [20]
$ trident verify hello.zheng
  Verification: PASS (private execution; Triton ZK)
  public input: []  ·  public output: [20]  ·  reductions: 32
$ trident prove pub.tri --input-values 7,13
  Proved public execution in 3 ms: 26 reductions, 2219 bytes
$ trident prove hello.tri --target triton --secret 7,13
  Proof generated (9 cycles) · 29 ms · trisha, Triton 7 STARK

three proof modes, each with an explicit guarantee

neither mode can silently fall back to a legacy statement or a different checker. earlier trace statements are no longer accepted as proof of execution or output — they require an explicit inspection opt-in and are labelled as such.

audit: SAFE, UNSAFE, or UNKNOWN — never a guess

module safe_add

#[requires(x == 3)]
#[ensures(result == 4)]
pub fn bump(x: Field) -> Field {
    x + 1
}

$ trident audit safe_add.tri --z3
  bump: SAFE (1 obligations) · 70 ms
$ trident audit safe_add.tri      # no solver installed
  bump: UNKNOWN (1 obligations)
$ trident audit bad.tri --z3       # ensures(result == 5)
  bump: UNSAFE (1 obligations)

0.3 · what changed

trident 0.3.0, trisha 0.3.0 and joy 0.5.0 are one coordinated release on compiler API 3. the full notes are on github; the shape of it:

1. the compiler and the warriors have clear owners. trident keeps parsing, types, typed IR, nox lowering and the shared extension interfaces. Triton code generation, costs, Neptune libraries and all 43 hand-written Triton baselines now live in trisha, beside the runtime that executes and proves them.
2. build, run, prove and verify select the same target. explicit targets, project settings and the nox default resolve consistently; trident discovers installed warriors, checks their capabilities and preserves program identity across the process boundary. stale API 1/2 warriors are rejected.
3. compiled programs preserve their intended values. early returns, selected branches, shadowing, simultaneous assignment, aggregate layouts, dynamic array bounds and spilled RAM values are fixed. entry signatures enforce arity and Bool/U32 ranges — inside proofs too.
4. nox verification binds computation, inputs, output and state. joy derives the zheng execution relation from the canonical program and checks the public result against it. public certificates, private proofs and authenticated state reads have distinct formats and explicit guarantees.
5. Triton and Neptune use the warrior's proof pipeline. trisha upgrades to pinned Triton 7, recursive proofs bind the complete inner claim, and a compiled lock becomes a validated SingleProof transaction intent submitted through an authenticated gateway — admission checked against a pinned Neptune node.
6. formal auditing distinguishes complete checks from unsupported analysis. SAFE · UNSAFE · UNKNOWN, as above.
7. the toolchain is packaged for native use. six archives, four executables each, runtime resources embedded; the source archive captures the exact locked dependency closure of all eleven sibling repositories.

four binaries, one archive

validated before it shipped

receipts bind validation to the released source and binary hashes: validation summary · logs, receipts, proof corpora · SHA256SUMS · native builds · cross-platform verification · source commit 531e93c

why a new language

provable VMs are not CPUs. the machine word is a field element, not a byte — Rust compiled to RISC-V wraps every field operation in byte-level emulation. trident's word is the field element itself. on nox, the default target, a program is a formula over 18 reduction patterns: every field operation is one reduction, the execution trace is the zheng witness, and the cost report before you run equals the reduction count after. on Triton VM the same source compiles to TASM, and the gap to byte-emulating zkVMs is not marginal:

units are the machine's own: a nox reduction is one trace row — one CCS step the prover folds (a hash is 24 Poseidon2 rounds + 1 squeeze row; the Merkle path is 33 of them plus limb plumbing); a Triton cycle is one instruction across six tables. both are exact and static, from trident build --costs. the zkVM columns are cycle counts of RISC-V code emulating field arithmetic.

built different

one source, 21 targets

a trident program is written once against field elements; the target is a config, not a rewrite. 21 engines are declared in the catalog; the compiler resolves a target once, and only an installed owner can authorize compilation. trident build --target <engine> picks one; a catalog entry does not provide a backend or a working deployment.

above the engines sit 25 unions — the operating systems and chains a program can be deployed into, each binding an engine: neptune (trisha-owned SDK and validated transaction flow, on triton) · linux macos android browser wasi on native and wasm engines · ethereum arbitrum solana polkadot ton near cosmwasm icp sui aptos starknet aztec aleo miden nervos nockchain succinct boundless openvm-network — declared and documented, awaiting bindings. the honest map is reference/targets.md.

the same formula, on silicon — sketches, not warriors

a nox formula is a tree over 18 patterns — small enough to hand-emit for any machine. silicon — an in-repo, unpublished crate at trident/silicon — turns the very formula joy proves into native code for 25 backends: every one below emits real output for hello.nox. honest scope: the emitters cover the atom-level patterns (axis, quote, branch, field arithmetic, bitwise) — programs using hash, divine, structs or state reads are refused with UnsupportedPattern — and they emit code, not traces: execution and proving on this hardware are not wired. the point is that one program already speaks to all of it; making it run and prove there is the next tier, one warrior per machine — which is exactly the shape 0.3 gave trisha.

where it runs today

soft3 — the default. trident build emits a nox formula; the joy warrior executes it on nox, proves it with zheng (SuperSpartan + Brakedown + HyperNova folding — hash-based, post-quantum, no trusted setup), reads state from bbg with authenticated openings. one algebra (strata), one hash (hemera), one field, from source to proof.

Neptune Cash — --target triton / neptune. the blockchain with recursive STARK proofs in production. trisha owns the bindings: proposed coin and card standards, lock and type scripts are written in trident, compile to TASM, prove on Triton 7, and a compiled lock becomes a validated SingleProof transaction intent. admission was checked against an isolated pinned Neptune node — not claimed as a public-network confirmation.

scope, honestly. this is the default CPU release. public certificates are transparent and linear. private proofs cover the documented bounded relation; private query coordinates do not make the database private. full GPU proving, dynamic nox continuations, variable branch shapes and live node/database integration are separate work. Z3 is an optional install for trident audit --z3.