Sigil

Sigil is a small language and compiler for concurrent, message-driven components. It exists because many serious service failures are not memory safety bugs or difficult algorithms. They are wiring bugs:

• state is updated after a message that depends on it has already been sent;
• a retry repeats an external side effect that was not safe to repeat;
• a remote queue wait has no deadline during a partition;
• one local path bypasses the durable ownership rules used by other inputs;
• a message reaches a process that cannot handle its type; or
• two individually reasonable components form a cycle that can deadlock.

Rust can make every line involved in these failures memory-safe. A library can provide channels, retries, and actors. Neither automatically sees the complete message graph, statement order, failure policy, placement boundary, and system invariant at the same time.

Sigil puts those facts in one checked program. Processes own private state, communication happens through typed sends, and timeout, retry, recovery, backpressure, routing, and placement decisions are explicit. The compiler can therefore reject invalid wiring before generating an ordinary Rust crate.

Within Sigil's documented model, several failure modes are unrepresentable in a checked program: cross-process state mutation, sends to incompatible handlers, cyclic bounded-channel topologies, unstable Float or Complex shard keys, remote sends with unbounded admission, and timed or retried work without a valid terminal failure path. When a specification requires an ordering or conservation property, a handler that violates it also cannot pass the requested assurance level.

This is the practical goal: make the safe wiring shorter to write, make common unsafe wiring fail at build time, and generate Rust that integrates with the rest of the system normally. Typical uses include order processing, audit pipelines, settlement, device control, telecom, and network automation.

The current production backend is Rust. The compiler also emits a checked, target-neutral Semantic IR (SIR), which is the foundation for planned client, worker, and WebAssembly targets. Node, Python, and WebAssembly backends are not available yet.

What Sigil provides

• Shared-nothing process state with message-based communication.
• Static type and name checking across schemas, transforms, handlers, and sends.
• Explicit timeout, retry, recovery, backpressure, and routing policies.
• Compile-time validation of process topology and remote placement boundaries.
• Checked integer, finite IEEE-754 binary64, exact fixed-scale decimal, and finite complex arithmetic.
• Assurance levels for local contracts, inductive invariants, and supported cross-process properties.
• Generated Rust crates with tests, machine-readable build metadata, and a residual-risk report.
• Native Rust function bindings for existing application and infrastructure code.

Sigil does not claim that a whole deployment cannot fail. Network drivers, storage engines, coordinators, operating systems, external services, and deployment configuration remain part of the engineering system. Generated artifacts record these assumptions instead of presenting them as compiler proofs.

Example

This handler records an audit result before forwarding the request:

process Audit {
  state recorded: Int = 0

  on request: Request {
    let logged = request
      ~> write_audit
        @timeout(60.ms)
        @retry(2)
        @backoff(initial: 5.ms, max: 20.ms)
        @recover(with: deny_unaudited)

    recorded := recorded + 1
    send logged to Vault @deadline(5.ms)
  }
}

spec ZeroTrust {
  hold Vault.served <= Audit.recorded
  require path_latency <= 700.ms
}

At assurance level 4, moving the recorded update below the send is rejected because Vault could receive a message before Audit.recorded reflects it. The check uses the typed handler bodies and verified process topology; it is not a text-pattern check.

The provable action gateway is the flagship end-to-end example: a typed identity, policy, risk, budget, approval, audit, capability, execution, and outcome boundary around autonomous tool use. It includes native Rust adapters, concurrent load and fault experiments, eight Level-4 system invariants, and six unsafe variants that the compiler must reject.

Complete runnable examples are under examples/.

Quick start

Build a Level-4 example and run its generated demo:

cargo run -p sigilc -- \
  examples/security/vault.sigil \
  generated/vault \
  --emit-main \
  --level 4

cd generated/vault
cargo run --bin demo

The output directory is a normal Rust crate with a Cargo.toml, generated source, tests, and Sigil metadata. It can be built and integrated with the usual Rust tools.

To exercise the generated fault-injection paths:

SIGIL_CHAOS_FAIL_PCT=20 \
SIGIL_CHAOS_LATENCY_MS=120 \
cargo run --bin demo

Language model

A Sigil program is built from a few concepts:

• A schema defines a typed value.
• A transform performs a calculation or calls a declared native function.
• A process owns private state and handles typed messages.
• send connects one process to another.
• Tags such as @timeout, @retry, @recover, @deadline, and @shed define failure and queue behavior.
• A placement declares which processes run together.
• A spec declares properties for the selected assurance level.

Handlers may use local bindings, state updates, pipelines, and statement-level branches. Branch-local names are lexically scoped. The generated Rust executes only the selected branch, while topology and worst-case timing analysis cover every possible branch.

The complete syntax and type rules are in docs/LANGUAGE.md.

Assurance levels

The compiler has five assurance levels:

Level	Name	Purpose
0	sketch	Parse and generate exploratory code. No safety claim or semantic digest is produced.
1	safe	Check names, types, numeric rules, failure paths, topology, routing, and transactional-handler restrictions. This is the default.
2	contracts	Check supported contract obligations and temporal budgets on a Level-1-valid program.
3	proofs	Prove supported inductive state invariants with explicit runtime-guarded input assumptions.
4	system	Prove supported ordering, reachability, multiplicity, and conservation properties across processes.

Higher levels include the checks from lower levels. Unsupported proof shapes fail closed instead of being treated as established.

The proof fragments and their limits are documented in docs/ASSURANCE.md and docs/SOUNDNESS.md.

Generated Rust

Sigil-generated process code uses isolated actor state and bounded channels. It does not emit Mutex or RwLock around Sigil-owned process state. This is not a claim that the complete runtime or linked dependencies are lock-free.

Generated crates:

• forbid unsafe in generated source;
• enable integer overflow checks in development and release profiles;
• validate finite Float and Complex values at generated boundaries;
• use checked arithmetic for language numeric operations;
• include generated tests for the emitted module;
• expose actor snapshots, terminal reports, and optional tracing; and
• include versioned build, effect, placement, SIR, and residual-risk artifacts where applicable.

Existing Rust functions can be imported as typed transforms. Bindings declare how they execute and their cancellation, idempotency, and side-effect contracts. See docs/PRODUCTION.md for integration details.

Distributed components

Placement declarations make local and remote process boundaries explicit. For remote edges, the compiler checks message codecs, bounded admission, handler dispatch, placement ownership, and transactional restrictions. Generated support includes versioned wire schemas, durable outbox interfaces, deduplication identities, lease and epoch fencing, placement-local startup, receiver permits, replay workers, and checked resharding contracts.

A deployment must still provide conforming transport, storage, discovery, coordinator, checkpoint, and repartition adapters. Sigil distinguishes an atomic durable state transition and initial outbox publication from exactly-once network delivery or external effects.

The runtime and deployment contracts are described in docs/RUNTIME.md, docs/PRODUCTION.md, and docs/RUNBOOKS.md.

Compiler architecture

The checked compilation path is:

Sigil source
  -> parsed AST
  -> typed and name-resolved HIR
  -> canonical Semantic IR
  -> analyses and proofs
  -> generated Rust

During the current migration, source and HIR/SIR analyses are compared at explicit equivalence gates. Topology and assurance levels 2 through 4 select the typed-HIR result only after the established and new paths agree. The Rust backend still consumes the checked AST, so additional backend cutover work is required before another execution language can be supported safely.

See docs/architecture/README.md for the multi-language architecture, target profiles, compatibility model, and backend conformance requirements.

Examples

Directory	Focus
examples/agent_gateway/	Provable autonomous-action boundary, native adapters, chaos, and rejected attacks
examples/branching/	Conditional routing and branch-local process wiring
examples/pipelines/	Payment, telemetry, and content-delivery pipelines
examples/distributed/	Placement, durable delivery, transactional handlers, and handoff
examples/security/	Audit and authorization ordering
examples/finance/	Decimal accounting and risk calculations
examples/trading/	Multi-handler order and cancellation flow
examples/telecom/	Complex signal values and chained rating flow
examples/networking/	Affinity routing and bounded network programming
examples/avionics/	Native device bindings and attitude control
examples/level3/	Inductive state invariants
examples/level4/	Cross-process system properties
examples/proofs/	Negative programs that must be rejected

Testing

Run the repository checks with:

cargo fmt --all -- --check
cargo clippy --workspace --all-targets --all-features -- -D warnings
cargo test --workspace --all-targets

The suite covers the parser and CLI, type and numeric rules, topology, assurance levels, the AST/SIR reference interpreters, property tests, generated crates, ABI fixtures, distributed fault cases, Loom concurrency models, and chaos regressions. The bounded soak test is intentionally manual:

cargo test -p sigil_rt --test soak -- --ignored --nocapture

GitHub Actions workflows are manually dispatched for selected commits and release candidates; pushes do not automatically start the full matrix.

Production status and limits

Sigil-generated Rust is used in production as ordinary Rust components. This means the generated code is exercised in real systems; it does not make every deployment configuration or external adapter correct by definition.

Each checked build records what the compiler established and what remains an assumption. Teams should review RESIDUAL_RISK.md together with the generated effect, placement, build, and wire metadata before deployment.

Current version: v0.7, generated ABI 17.

Important current limits:

• Rust is the only supported execution backend.
• Proofs cover documented fragments rather than arbitrary programs.
• External functions and infrastructure keep their declared residual risk.
• Remote correctness depends on conforming deployment adapters.
• Level 0 is for exploration and establishes no safety guarantees.

The detailed readiness checklist and release gates are in docs/PRODUCTION_READINESS.md.

Documentation

Document	Contents
docs/LANGUAGE.md	Language syntax and semantics
docs/ASSURANCE.md	Assurance levels and proof obligations
docs/RUNTIME.md	Runtime and generated actor behavior
docs/PRODUCTION.md	Integration, capacity, observability, and operations
docs/PRODUCTION_READINESS.md	Maturity checklist and release gates
docs/SOUNDNESS.md	Proof premises and preservation arguments
docs/RUNBOOKS.md	Operational response procedures
docs/ABI.md	Generated artifact versions and compatibility
docs/RESIDUAL_RISK_PROCESS.md	Residual-risk review process
docs/VERSIONING.md	Language, proof, runtime, and ABI versioning
docs/architecture/README.md	Multi-language semantic architecture

Project layout

sigilc/src/
  frontend/       parser and source AST
  analysis/       typed HIR/SIR, checks, proofs, topology, and residual risk
  backend/        Rust code generation
sigil_rt/         actor, routing, retry, numeric, and distributed runtime
examples/         runnable examples and negative proof cases
docs/             language, assurance, runtime, operations, and architecture

License

MIT. See LICENSE.