Selective disclosure
Reveal the fact a policy needs, not the credential or private object that supports it.
Technology / Privacy & verification
Privacy without invisible authority.
Private execution is useful only when the public system can verify exactly what was authorized and what the evidence establishes—without learning the hidden record.
Explicit assurance
A result identifies whether it carries a cryptographic proof, attestation, or weaker operational receipt.
Bound execution
Evidence commits to the model, runtime, input, authorization context, random seed, and claimed output.
Post-quantum boundary
Canonical envelopes and versioned cryptography keep the authorization and consensus path replaceable by design.
Formal verification
Proofs are a launch gate, not a marketing line.
Critical protocol claims are paired with executable tests, canonical vectors, bounded model checks, and formal models. Assurance is published by boundary and strength so an engineering claim cannot quietly expand beyond its evidence.
Canonical encodingAuthorization safetyConsensus finalitySupply invariantsExternal verification
Scoped theorems, reproducible locally
Lean checks algebraic and state-machine invariants. Tamarin checks adversarial traces, authentication, replay, compromise, and ordering. TLC has exhaustively explored consensus and proof-pipeline state spaces, while Kani reaches bounded production-code codec and verifier harnesses.
Selected boundaries go further with executable refinement: the Lean model and the production Rust are driven through the same trace and required to agree byte for byte, so a divergence fails the gate rather than passing unnoticed. Cash lifecycle, consensus history, verifier duty settlement, and consent-bound credential issuance are covered this way.
Models are not the Rust implementation
Every proof scope names its abstractions and conformance gaps. Bounded exploration is not an unbounded theorem, and modeled cryptographic validity is not a primitive-security proof.
This gap is not hypothetical. Ongoing adversarial review of the authorization path found defects that the models did not exclude, including a proof scope asserting a revocation property that one verification entry point did not implement. Some are fixed; the rest are tracked publicly with reproduction detail rather than quietly carried. Expect that count to keep moving while the review continues.
No self-issued certificate
External formal-methods, cryptography, consensus, economics, FFI, and mobile review of a frozen commit is mandatory before any non-developmental or value-bearing launch.
Actum now runs post-quantum zero knowledge
Actum PQ-ZK v1 is a working transparent proof profile that generates and verifies real succinct zk-STARK receipts while keeping private witness bytes out of the public journal. It pins an exact RISC Zero guest image and binds verification to the exact public statement.
This does not claim that Actum invented STARKs or that the compiler, zkVM, STARK, FRI, hashes, host environment, or hardware have been formally verified.
Private execution
A PQ-native execution boundary, designed around what must be proven.
ObjectVM gives principals, capabilities, policies, objects, jobs, and receipts canonical semantics; the transition kernel supplies bounded resources, explicit reads and writes, and deterministic effects. Shielded state is represented by commitments, while private inputs stay in the witness.
Small, typed, and effect-explicit
ObjectVM is not a Linux emulator or an EVM clone. Canonical encoding, fixed resource limits, conflict-checked access sets, and no_std Rust keep transitions reproducible.
Intent and witness are separate
A transaction commits to public intent, state roots, policy, resource budget, and expected effects. A short-lived PQ authorization witness carries private proofs and session material.
Transparent proof path
The authoritative path is a transparent, hash-based STARK trace with SHAKE-derived commitments and PQ signatures around it, without pairing curves or a classical settlement chain in consensus.
Proofs bind to one global state
Reads, writes, deletes, capability consumption, nullifiers, and Coin Cell spends bind to the exact pre-state root. Conflicting effects fall back to deterministic serial validation.