NOUS (Nous) -- The Living Language

An agentic programming language with end-to-end formal cost-bound verification, in any currency the pricing table declares, with cryptographically signed dossiers anchored to a public transparency log and verifiable by anyone offline.

  _   _  ___  _   _ ____
 | \ | |/ _ \| | | / ___|
 |  \| | | | | | | \___ \
 | |\  | |_| | |_| |___) |
 |_| \_|\___/ \___/|____/   v8.0.0

Author: Hlias Staurou (Hlia) | Project: Noosphere | GitHub: contrario/nous | Website: nous-lang.org

What is NOUS?

NOUS is a programming language for agentic AI systems where every program is:

• Verifiable -- declare a cost_cap in USD or EUR and Z3 proves at compile time that the declared cost envelope (each soul's declared tokens at the pinned prices, over max_ticks) cannot exceed it. The proof covers what the program declares; it does not meter or stop spend at runtime.
• Auditable -- every verified program emits an Ed25519-signed manifest with full provenance (source SHA-256, AST SHA-256, pricing SHA-256, SMT obligations SHA-256, solver name+version, verdict, timestamp).
• Annex IV-ready -- nous dossier emits an EU AI Act Annex IV-aligned compliance bundle directly from the AST plus the signed manifest plus the pricing table.
• Rekor-anchored -- since v5.3.0, optional --anchor rekor anchors emitted manifests into the public Sigstore Rekor transparency log via Path-beta dual signing (per-submission ECDSA-P-256 leaf, long-lived Ed25519 manifest signature preserved). Since v5.10.0 a Rekor v2 path (--anchor rekor_v2) targets the tile-backed Sigstore log with an RFC 3161 trusted timestamp over the leaf signature, all re-verifiable offline. External, third-party-auditable durability, with no NOUS-side trust assumption on the offline verification path. See docs/REKOR_ANCHOR.md and docs/REKOR_V2_MIGRATION.md.
• Publicly verifiable -- since v5.4.0, any signed dossier can be verified by anyone via three independent paths: POST /api/v1/verify-dossier (browser convenience, no API key, rate-limited), verify_offline.py (canonical, single cryptography dependency), or the toolchain (nous dossier <source> --manifest <manifest> checks the manifest's Ed25519 signature under the key it carries and re-derives the SMT spec from source; the digest matches only when run with the NOUS version recorded in the manifest, pip install nous-lang==<nous_version>). See docs/VERIFY_DOSSIER.md.
• Governable -- first-class policy { on ... signal ... action ... } declarations, statically lintable (13 rule codes) and live-simulatable.
• Deterministically replayable -- every agent run produces a SHA-256-chained JSONL event log. nous replay verify validates chain integrity offline.
• Self-evolving (opt-in) -- nous evolve mutates a program's declared DNA genes within their declared ranges on a shadow copy of the AST, re-validates each candidate against the constitutional law checker, and keeps a mutation only if a measured fitness score improves -- otherwise it rolls back atomically. Optimization within declared bounds; it records each mutation and proves nothing.
• Governed and evidenced -- beyond cost proofs, NOUS emits a lineage of signed, offline-verifiable evidence artifacts: runtime-conformance certificates, materiality classification, gated-action authorization, an append-only continuity and envelope ledger with witness cosignatures, per-interval closure attestations, a SLSA Verification Summary Attestation with published conformance vectors, and consume-only adapters for third-party governance frameworks. Each EVIDENCES within a declared boundary (see Documentation); none is a runtime guard.

NOUS transpiles to Python 3.11+ asyncio. The toolchain is a single PyPI package -- no Java, no Docker, no LangChain / LlamaIndex / CrewAI dependencies.

The honest boundary

Evidence collection and conformance verification are observational: they record and attest, they do not enforce. Runtime intervention is performed by a distinct runtime policy engine, which gates when a policy declares a blocking action (ADR-0010). The word proves is reserved strictly for the Z3/Farkas legs -- the cost-cap bound, policy-coverage, and sequence-ordering. Everything else -- Ed25519/ML-DSA signatures, Rekor v2 inclusion, RFC 3161 timestamps, continuity/envelope/witness cosignatures, closure attestations, and every interop adapter -- evidences, it does not prove. Name-to-key binding is operator-asserted; NOUS runs no CA and certifies no identity. Independent witnessing is staging, genesis-only. The interop adapters (Santander mech-gov, Guardrails AI, LLM Guard) are consume-only over synthetic/benchmark inputs, not production usage. Each artifact's exact claim class and boundary is stated in the Documentation section.

Why this matters

Runtime budget caps abort only after the spend has already happened. NOUS instead proves before execution that the declared cost envelope (declared tokens at pinned prices, over max_ticks) cannot exceed the declared cap -- a Z3/Farkas result, not a runtime check. The proof is over the declarations; it does not meter or cap what a run actually spends. The cost model is auditable (signed pricing TOML with SHA-256), and the artefact (signed manifest) is verifiable by anyone holding your public key -- making it directly useful for EU AI Act Annex IV / Article 11(1) technical documentation.

With v5.3.0 Rekor anchoring and v5.4.0 public verification surface, the trust model is closed end-to-end: third-party auditors no longer need the NOUS CLI to validate a dossier. A regulator, journalist, or compliance officer can drag a manifest into nous-lang.org/verify and see three independent PASS/FAIL pills in their browser, or run verify_offline.py on an air-gapped machine. The cryptographic chain extends from your build pipeline to a public transparency log to anyone holding a copy of the dossier.

Install

# Core toolchain (cryptography is base, not optional)
pip install nous-lang

# With SMT cost-bound verification (adds Z3)
pip install 'nous-lang[smt]'

# With LSP server (VS Code / editor diagnostics)
pip install 'nous-lang[lsp]'

# Everything
pip install 'nous-lang[all]'

Requirements: Python 3.11+. The [smt] extra pulls z3-solver. cryptography (used for Ed25519 signing) is a base dependency since v4.17.0.

60-second quick start

# 1. Initialise a project
mkdir my_world && cd my_world
nous prices init                       # writes ./nous_prices.toml from defaults
nous templates extract cost_cap_basic  # copies a working .nous program

# 2. Verify formally
nous verify cost_cap_basic.nous --smt
# -> Verdict: PROVEN. Manifest written to cost_cap_basic.manifest.json.

# 3. Emit an Annex IV compliance dossier
nous dossier cost_cap_basic.nous
# -> bundles source, AST, manifest, pricing table, and Annex IV mapping

# 4. (Optional) Anchor the dossier into the public Sigstore Rekor log
nous dossier cost_cap_basic.nous --anchor rekor
# -> manifest gains a transparency_log block with log_index + integrated time

# 5. (Optional) Verify a dossier offline (no NOUS install required for the verifier)
cd <dossier> && python3 -I verify_offline.py --expect-signer <publisher key, base64>
# -> exit 0 PASS, 1 INTEGRITY, 2 ENVIRONMENT, 3 OUTSIDE; the last line names the class
#    (the key comes from the publisher, out of band; no PASS without it)

For EUR end-to-end verification, point --prices at an EUR pricing table:

nous verify --smt my_eur_agent.nous \
    --prices /path/to/eur_prices.toml

The shipped pricing/eur_example.toml declares four illustrative Mistral models priced in EUR per 1 000 000 tokens. Values are explicitly marked illustrative; verify against the provider before any production use.

Core CLI

nous run file.nous              # compile + execute
nous compile file.nous          # -> Python file
nous verify file.nous           # governance lint as build gate
nous verify file.nous --smt     # SMT cost proof + signed manifest
nous verify file.nous --smt --smt-margin 10
                                # prove total_cost <= cap * 90/100
nous verify-cost cost.farkas.json
                                # offline re-check of the cost-cap Farkas cert (no solver)
nous emit-smt file.nous         # SMT-LIB 2.6 source (re-usable across solvers)
nous dossier file.nous          # EU AI Act Annex IV compliance bundle
nous dossier file.nous --anchor rekor
                                # also anchor manifest into Sigstore Rekor
nous dossier source.nous --manifest manifest.json --prices pricing.toml
                                # check a dossier's signature, re-derive its spec (run the version the manifest records)

nous prices show                # active layered pricing table + SHA-256
nous prices init                # write nous_prices.toml in cwd
nous prices verify <model>      # detailed cost breakdown for one model
nous prices age                 # staleness report across all entries
nous prices upgrade <file>      # migrate v1.0 -> v2.0 schema (preserves comments)

nous governance lint file.nous  # static analysis (13 rule codes)
nous governance simulate ...    # what-if policy evaluation

nous replay verify <log>        # validate JSONL chain integrity
nous replay diff a.jsonl b.jsonl
                                # lockstep event-level diff

nous templates list             # list bundled templates (12 shipped)
nous templates show <name>      # print template source to stdout
nous templates extract <name>   # copy template into a directory

nous skill export file.nous     # emit agentskills.io-compatible skill folder
nous dossier-spec ./my-skill/   # emit signed Annex IV dossier from SKILL.md

nous lsp                        # start LSP server (stdio)
nous version

The full nous --help lists 62 top-level subcommands; the above covers the most-used surface.

Language at a glance

world ExampleWorld {
    cost_cap: 1.00 USD              // formal SMT bound, USD or EUR
    max_ticks: 10                   // bound on heartbeat cycles
    law CostCeiling = $0.10 per cycle
    law MaxLatency = 30s
    law NoLiveTrading = true
}

soul Sentinel {
    mind: claude-opus-4-7 @ Tier1
    tokens: input=1000 output=400   // SMT input
    senses: market_feed, risk_oracle
    speaks: AlertChannel
    remembers: last_signal
}

policy on llm.response signal contains_phrase("absolutely") action log_only weight 0.3

Architecture

Layer	Implementation
Grammar	Lark LALR (nous.lark), bilingual EN+GR
AST	Pydantic V2 strict models
Validator	Constitutional law checker on AST
Pricing	Layered TOML (CLI > project > user > package), SHA-256 audit, schema v2.0, currency-agnostic
SMT emit	Deterministic SMT-LIB 2.6, exact rationals (no floats)
SMT solve	Z3 wrapper + counterexample extraction + fix suggestions
Manifests	Ed25519-signed JSON, manifest schema v1.0, offline-verifiable
Rekor anchor	Optional Path-beta dual signing (ECDSA-P-256 leaf + Ed25519 manifest)
Verify API	POST /v1/verify-dossier public endpoint, granular three-path response
Dossier	EU AI Act Annex IV-aligned compliance bundle from AST + manifest
CodeGen	AST -> Python 3.11+ asyncio
Replay	SHA-256-chained JSONL event log, integrity-verifiable offline
Runtime	asyncio event loop + Noosphere integration
LSP	stdio JSON-RPC, lint diagnostics with source="nous.lint"

The signed-manifest contract

When nous verify --smt returns PROVEN, it writes a JSON manifest:

{
  "schema_version": "1.0",
  "nous_version": "5.11.0",
  "smt_emit_version": "...",
  "source_path": "trading.nous",
  "source_sha256": "...",
  "ast_sha256": "...",
  "pricing_sha256": "...",
  "smt_obligations_sha256": "...",
  "solver": "z3",
  "solver_version": "...",
  "verdict": "proven",
  "cost_cap": "0.50",
  "currency": "USD",
  "timestamp": "2026-05-17T12:34:56Z",
  "signature": "<base64 ed25519>",
  "public_key": "<base64 ed25519 pubkey>",
  "transparency_log": {
    "rekor_log_index": 1554376230,
    "rekor_integrated_at": "2026-05-16T20:08:25Z",
    "rekor_log_id": "...",
    "submitter_public_key_b64": "...",
    "submitter_signature_b64": "..."
  }
}

The transparency_log block is present only when the dossier was emitted with --anchor rekor. Anyone with the manifest and the publisher's public key can re-verify offline. Tamper-detection is built in. If the manifest is Rekor-anchored, the inclusion proof and SignedEntryTimestamp can be re-validated independently against the public Sigstore log.

The verifier signing key lives at $XDG_DATA_HOME/nous/keys/signing.key (mode 0600, auto-generated; falls back to ~/.local/share/nous/keys/signing.key if XDG is unset; override with --key-path).

Public verification (v5.4.0+)

Three independent paths for third parties to verify a NOUS dossier without installing the NOUS toolchain:

1. Browser convenience: drag-drop the manifest into https://nous-lang.org/verify. Behind the scenes calls the public POST /v1/verify-dossier endpoint (no API key, rate-limited 30 req/min, 256 KiB body cap). Useful for compliance officers and journalists.
2. Offline canonical: run the verify_offline.py inside the dossier directory, cd <dossier> && python3 -I verify_offline.py --expect-signer <publisher key, base64>. The key is the publisher's raw Ed25519 public key, taken out of band, not from the dossier; without it the verifier gives no PASS (exit 2). Exit codes: 0 PASS, 1 INTEGRITY, 2 ENVIRONMENT, 3 OUTSIDE (the manifest is authentic and its solver verdict is not proven); the last line of stdout names the class. -I keeps Python from importing modules from the dossier directory, which its sender controls. The standalone download is withdrawn (docs/adr/ADR-0009-standalone-verifier-withdrawal.md). Runs locally; only dependency is cryptography>=42. No NOUS install, no internet required for non-Rekor checks, no network round-trip to NOUS infrastructure. This is the canonical trust path.
3. Full CLI: pip install nous-lang==<nous_version> (the version the manifest records), then in the dossier directory: nous dossier source.nous --manifest manifest.json --prices pricing.toml --output <dir> checks the manifest's Ed25519 signature under the key the manifest carries and the source sha, re-derives the SMT spec from source, and refuses on any mismatch; it writes a new dossier directory; --anchor defaults to none. nous verify-cost cost.farkas.json --manifest manifest.json re-checks the cost-cap Farkas certificate by exact arithmetic and, with --manifest, that it is the certificate the manifest names (a sha match only; the manifest signature is checked by verify_offline.py and by nous dossier). Who holds the signing key is established out of band.

Verification returns granular per-check results:

• signature_ok -- Ed25519 author signature over canonical manifest body
• rekor_set_ok -- Sigstore SignedEntryTimestamp + log-key allowlist
• rekor_inclusion_ok -- leaf body hash + ECDSA-P-256 submitter signature

See docs/VERIFY_DOSSIER.md for the full API reference, trust model, and failure-mode table.

EU AI Act compliance

NOUS targets EU AI Act conformity for the high-risk AI system requirements of Regulation (EU) 2024/1689. The compliance matrix lives in docs/EU_AI_ACT_COMPLIANCE.md: it states, article by article, what NOUS does -- proves, evidences, gates, maps, or nothing -- and does not assert that any article is satisfied.

Key article alignments:

• Article 11 (Technical Documentation) -- nous dossier emits an Annex IV-aligned bundle directly from the AST.
• Article 12 (Record-Keeping) -- SHA-256-chained JSONL replay logs, integrity-verifiable via nous replay verify.
• Article 13 (Transparency) -- public verification endpoint and standalone nous-lang.org/verify page give downstream users a no-install path to independently audit any dossier.
• Article 14 (Human Oversight) -- intervene, inject_message, block policy actions plus governance simulator.
• Article 15 (Accuracy / Robustness / Cybersecurity) -- Z3 SMT proofs on every cost_cap declaration, currency-aware (USD + EUR), with Ed25519-signed manifests and optional Sigstore Rekor anchoring for tamper-evident durability.

Annex IV dossiers from existing SKILL.md skills (v5.1.0+)

NOUS can produce signed Annex IV dossiers directly from skill folders that follow the agentskills.io SKILL.md spec, without modifying the skill itself. Add a nous.yaml sidecar declaring cost_cap, default_model, and per-tool max_calls / input_tokens / output_tokens, then:

nous dossier-spec ./my-skill/

The resulting bundle contains the verbatim SKILL.md and nous.yaml, a deterministic source envelope (source.nous), the signed manifest.json, the resolved pricing TOML, the public key, a human-readable README, and an offline verify_offline.py. SKILL.md is left byte-identical, so strict spec validators continue to pass. See docs/SKILL_MD_SIDECAR.md for the schema reference and CLI flag documentation. For the inverse direction -- emitting an agentskills.io skill from a .nous program via CLI, HTTP API, or IDE button -- see docs/SKILL_EXPORT.md.

Documentation

• Cost Verification Guide -- end-to-end walkthrough for USD and EUR
• SMT Verification Design -- soundness contract, Z3 pin rationale
• One Price Source Design -- arc B, every dollar figure from pricing.py: P0 findings and P1 (the live dispatch cascade) shipped, P2-P5 open
• Coverage Proof -- policy-coverage SMT obligation, Farkas certificate, stdlib-only offline verification
• VSA Conformance Vectors -- published frozen input/expected-output bundle; implementation-independent offline verification of the manifest canon, signatures, and cost/coverage Farkas verdicts (cryptography + stdlib, no solver)
• Memory Evidence Design -- signed per-soul memory, Phase 0 freeze
• Memory CLI -- nous memory init/append/verify/reindex reference
• Memory Phase 1 Design -- NAME-BOUND identity, drop-when-None write-path invariant, single-soul (Option c) freeze
• Memory Consultation -- consult per-(world,soul) memory inside the signed trace; offline-verifiable chain-head commitment
• EU AI Act Compliance -- Annex IV / Article 11 mapping
• Annex IV Mapping -- per-section Annex IV crosswalk to NOUS evidence artifacts

Contributing

NOUS is developed under a non-standard model: single maintainer, chat-driven, idempotent patch scripts, 10-phase release pipeline. External contributions are welcome but follow an "issue first, PR after we agree on shape" intake. See CONTRIBUTING.md and CODE_OF_CONDUCT.md.

Security issues should be reported via GitHub Security Advisories, not public issues.

Stats (v8.0.0)

Metric	Value
Tests	3913 passing, floor 3912 (PYTEST_FLOOR enforced)
Regression	byte-identical harness, 0 baseline drift
Shipped templates	12 (nous templates list)
Grammar	Lark LALR, bilingual EN+GR
AST nodes	Pydantic V2 strict models
Lint rule codes	13 (L000-L004, L006-L012, L100)
CLI subcommands	62 (nous --help)
Pricing schema	v2.0 (currency-agnostic, per-table _currency)
Manifest schema	v1.0 (Ed25519-signed, offline-verifiable, optional Rekor transparency_log)
Verification surfaces	3 (browser endpoint, offline Python, full CLI)
Latest changes	See CHANGELOG.md for per-release detail

Status

NOUS is free and open source under the MIT License. It is built and maintained by one person, a researcher, not a company -- no team, no funding, no reference deployments. It is research and infrastructure, offered as-is. If you want to discuss the work, I am on LinkedIn (https://www.linkedin.com/in/hlias-staurou-a632a197). Security issues via GitHub Security Advisories.

License

MIT. See LICENSE.

The MIT License covers the source code. Trademark rights over "NOUS", "Noosphere AI", "AetherProof", and "Asklepios" are reserved separately; see TRADEMARK.md.

Changelog

See CHANGELOG.md. Latest release: v8.0.0.