uneffect

Uneffect adds gradual effect specifications, Hoare-style contracts, and temporal models to existing TypeScript without requiring an effect runtime. Specifications are ordinary block comments and do not change emitted JavaScript.

Install

Uneffect requires Node.js 24 or newer. Default uneffect check uses Corsa plus Oxc and does not construct a JavaScript TypeScript 6 Program. Unclassified calls are unknown, not empty inferred proofs. Pass --typescript-program for the full TypeScript effect, contract, and annotation path.

npm install --save-dev @mizchi/uneffect typescript
npx uneffect doctor

With pnpm:

pnpm add --save-dev @mizchi/uneffect typescript
pnpm exec uneffect doctor

Quickstart

Add an annotation to an existing TypeScript function:

/* uneffect:effect Console */
export function log(value: number): void {
  console.log(value)
}

/* uneffect:requires n >= 0 */
/* uneffect:ensures result === n */
export function count(n: number): number {
  let value = 0
  /* uneffect:loop_invariant value >= 0 && value <= n */
  while (value < n) value++
  return value
}

The numeric loop contract above currently uses the explicit Program path. Install its compatibility compiler and check the file:

npm install --save-dev @typescript/typescript6
npx uneffect check --typescript-program src/example.ts
npx uneffect check --typescript-program --infer --assurance no-unknown src/example.ts

Default check uses Corsa/Oxc for effect inference and bounded Boolean/constant-return contracts. Other contract bodies produce an explicit unsupported diagnostic during migration.

For a low-annotation CI rollout, commit an inferred-effect baseline and reject new effects or newly unknown calls on later changes:

npx uneffect check --project tsconfig.json \
  --write-effect-baseline .uneffect/effects.json
git add .uneffect/effects.json

# CI
npx uneffect check --project tsconfig.json \
  --effect-baseline .uneffect/effects.json

This catches capability expansion without requiring a matching annotation in advance. It does not detect behavior changes that stay within the same inferred effect set.

An effect declaration is an upper bound. Missing transitive effects are errors; declared but unused effects are warnings. Use /* uneffect:effect none */ for an explicit checked empty bound. An unannotated function is not declared pure.

See the Quickstart guide for project setup, CI, runtime instrumentation, and model generation. See Gradual annotations for the complete comment grammar.

Install the agent skill

The Uneffect agent skill teaches compatible coding agents how to choose annotations and report assurance boundaries.

Install it with the Skills CLI:

npx skills add mizchi/uneffect --skill uneffect

Or with APM:

apm install mizchi/uneffect/skills/uneffect

Add --global for the Skills CLI or -g for APM to install it for the current user. For reproducible APM project installs, add mizchi/uneffect/skills/uneffect to dependencies.apm in apm.yml and commit the generated apm.lock.yaml.

What Uneffect checks

• Capability effects such as filesystem, network, environment, Console, Fetch, DOM operations, mutation regions, typed Throw, and user-defined effects.
• Preconditions, postconditions, loop invariants, machine-number domains, and selected typed-array bounds.
• Promise rejection ownership, timers, supported Promise combinators, and explicit resource management. Async observations are inputs to the temporal model, not a separate formal-specification domain.
• User temporal specifications and supported JavaScript async observations lowered into one host-aware Quint model.
• Opt-in React functional-component and Trusted Types fragments.

Start with uneffect check --infer on a selected boundary, annotate leaf I/O and high-value invariants, then ratchet CI assurance only where the relevant fragment is supported.

Assurance boundary

Uneffect 0.3 is an experimental release. It is useful as an additional, fail-closed review and CI layer on explicitly selected TypeScript boundaries. A verified artifact applies only to its exact claim, source snapshot, configuration, supported syntax fragment, and recorded backend.

Within that pre-1.0 boundary, two bounded public integration contracts are supported: the versioned Corsa semantic-query API and the high-level temporal model/result facade covering its classified Promise/resource fragments. Low-level CFG, lowering, solver, and direct generator APIs remain experimental.

Uneffect is not a verifier for all of JavaScript. Do not use it as the sole security boundary, a replacement for runtime validation, a whole-program correctness claim, or proof of arbitrary third-party/native behavior. Exit code 0 without an assurance profile means the enabled checks passed; it is not a proof. assumed depends on its trust ledger, and unknown establishes nothing.

Before relying on a result, read:

• Feature overview
• Public API and compatibility
• Assurance boundaries
• Stability and safe adoption
• Feature matrix
• Implementation status

Annotation surface

Only block comments with an explicit uneffect: marker are interpreted. The token after the marker is the directive; users do not select an internal proof domain. Normal JSDoc is untouched.

Directive family	Purpose
uneffect:effect, module_effect	Effect and module-initialization upper bounds
uneffect:requires, ensures, loop_invariant	Hoare-style contracts
uneffect:state, action, always	State machines and temporal properties
ownership and resource directives	Promise and resource protocols in the temporal model

Detailed references:

• Effect system
• Deno-compatible permissions
• Async safety
• Persisted contract summaries
• Formal models
• React semantics
• Trusted Types
• Typed arrays and numeric domains

CLI

The package publishes the uneffect binary. Its main commands are check, doctor, spec, instrument, and evidence. Use spec temporal for the combined user/JavaScript async model:

npx uneffect check --project tsconfig.json --infer
npx uneffect check --project tsconfig.json \
  --assurance no-unknown --json > uneffect-check.json
npx uneffect spec temporal src/protocol.ts main --runtime web > protocol.qnt

See the CLI reference for all commands, options, exit codes, workspace-project behavior, and solver backend selection.

For in-process use, the package root exposes only numeric/runtime helpers and high-level checking facades such as checkFiles, verifyUneffectProject, and generateTemporalModel; stored temporal results can be validated with parseTemporalModelResult. The versioned direct Corsa semantic-query contract is available from @mizchi/uneffect/corsa/api. Solver adapters, lowering IRs, direct Quint generators, and optimizer experiments live under @mizchi/uneffect/experimental and have no compatibility guarantee. Raw Corsa/Oxlint checker-fact and parity integrations live under @mizchi/uneffect/experimental/corsa. See Public API and compatibility for the exact boundary.

The compiler-independent CFG core is available from @mizchi/uneffect/cfg. See CFG API and source layout. Workflow preflight with parallel barriers and dependency-impact analysis are supported through @mizchi/uneffect/workflow and @mizchi/uneffect/impact. See graph analysis for their input contracts and limits.

Development

The repository uses pnpm, Node.js 24+, and just.

just install
just check

Documentation and roadmap

• Documentation index
• Feature overview
• Public API and compatibility
• Adoption patterns guide
• Native integration
• TypeScript 7 / Corsa migration plan
• Roadmap and known gaps
• Implementation TODO
• GitHub Issues

GitHub Issues are the source of truth for unfinished roadmap work.

License

MIT