0.1.0 · Developer preview

Pactern

Delegate the code.
Keep the contract.

A programming language for AI-written backend components. You define the requirements. Agents change the implementation. The toolchain checks the agreement.

Run the quota example See a repair

The requirement you keepcontracts/quota.pact.ptn

module quota;

pact reserve_safety for reserve {
    requires available >= 0;
    ensures match (result) {
        Result::Ok(remaining) =>
            amount > 0 &&
            amount <= available &&
            remaining ==
                available - amount &&
            remaining >= 0,
        Result::Err(
            ReserveError::InvalidAmount
        ) => amount <= 0,
        Result::Err(
            ReserveError::InsufficientQuota
        ) => amount > 0 &&
            amount > available,
    };
}

Repaired quota fixture · Z3 verification

Consistent premises. Valid postconditions.
No arithmetic traps. Terminates.

A repair with a fixed target

Fix the code.
Preserve what it must do.

A green build means less if an agent also rewrites the expected result. A pact states acceptable behavior separately, so the implementation can change while the requirement stays put.

Reserve quota

src/quota.ptn · function excerpt

pub fn reserve(
    available: I64,
    amount: I64
) -> Result<I64, ReserveError> {
    if (amount <= 0) {
        return Result::Err(
            ReserveError::InvalidAmount
        );
    }
    if (amount > available) {
        return Result::Err(
            ReserveError::InsufficientQuota
        );
    }
    return Result::Ok(available - amount);
}

Check before subtracting.

The repair rejects invalid amounts and insufficient quota. A valid reservation still has to succeed: returning an error for every request would also violate the pact.

Available: 3
Requested: 4
Candidate result: Err(InsufficientQuota)
Guarded Wasm: Returns the specified error
Postcondition proof: Proved

Same pact in both cases. The verifier also checks arithmetic safety and termination separately.

Conformance fixtures · interpreter and compiled WasmRead the source

Write the rule at a boundary that matters.

A useful pact describes acceptable results independently of the algorithm. For quotas, worker allocation, or validation, a few stable properties can constrain many implementations. The pact itself still needs human review.

Beyond a function contract

Keep the agreement
through the whole change.

The executable quota workflow connects inspection, verification, protected edits, sandboxed execution, and replay.

Requirements survive edits.

An external baseline protects pacts and their meaning-defining helpers. Both text edits and semantic requests face the acceptance gate. Changing a requirement needs approval tied to the exact diff.

Protected changes

Changes name their target.

Inspect signatures, callers, effects, and affected pacts through the semantic API. Stage an edit against persistent symbol IDs and a workspace revision. Managed snapshots commit atomically; stale proposals are rejected.

Semantic CLI

Authority comes from the host.

Effect declarations expose requested operations. Host-issued, noncopyable handles grant tenant-scoped access. The Wasm host bounds memory and execution; the quota adapter enforces transactions, budgets, and cleanup.

Host boundaries

Evidence follows the artifact.

Proofs, runtime guards, and executed tests have separate results bound to source, tools, policy, and artifact hashes. Quota traces replay against their recorded revision with zero live writes. Unknown and unsupported remain explicit.

Verification and replay

Run the complete repair workflow.

Expose the defect, reject a weakened pact, apply a proof-gated repair, reject a stale change, and replay the original failure.

cargo run -p pactern --locked \
  --example quota_workflow -- target/quota-workflow

A scripted demonstration. Outputs include generated C/Wasm, traces, repair receipts, and artifact-linked evidence.

Where to use it first

Small components.
Consequential rules.

Start with business rules, validation, data transformations, and bounded jobs called by an existing application.

Functions, records, enums, generics, Option and Result. Immutable values by default. Explicit local mutation. Checked signed 64-bit arithmetic.

.ptn sourceRust toolchainGenerated CWebAssembly

The interpreter, C backend, and verifier consume the same typed core representation.

Working in the preview

Source checking and formatting, effect and handle checks, guarded C/Wasm execution, seeded property tests, narrow Z3 verification, semantic queries, managed edits, and the transactional quota/replay host.

Implementation status

Know the current limits

Static proof covers a loop-free pure fragment; loops and recursion remain unsupported by the verifier. Invocation arguments are specialized into each Wasm artifact. Storage is in-memory. A complete LSP extension and external CI activation remain open.

Agent productivity gains have not been measured. This is an experimental developer preview.

Read the evaluation

Build it. Check it. Run it.

Try a rule
you can verify.

Build from source, then reserve two units from a balance of three. The CLI compiles the quota function and its pact to guarded Wasm and runs it in the bounded host.

Use the pinned Rust toolchain via rustup. Compiled execution needs Clang and wasm-ld; verification also needs Z3. Exact versions and setup are in the candidate guide.

Build prerequisites

From a source checkout

git clone https://github.com/andrewarrow/pactern.git
cd pactern
cargo build --workspace --locked

cd fixtures/conformance
../../target/debug/pactern run \
  --entry quota::reserve --args '["3","2"]' \
  src/quota.ptn contracts/quota.pact.ptn --json

ResultResult::Ok(1)One unit remains.

Verify the same contract across all supported inputs:

../../target/debug/pactern verify \
  src/quota.ptn contracts/quota.pact.ptn --json

I64 arguments use JSON decimal strings to preserve their exact value.

Candidate guide Build and install ↗ Language specification Semantics and grammar ↗ CLI reference Commands and JSON ↗