ProofScript Programming Language

Verified Software with ProofScript

What changes when software properties become theorems?

Home · Docs · Type Theory · Proofs · Verified Software · ProofScript → Lean + TypeScript · Reference · Examples · Download

Software correctness is not one property. A real system can be type-correct but logically wrong, logically verified against the wrong specification, correctly compiled but misconfigured at runtime, or perfectly implemented while depending on a broken external service.

ProofScript is useful because it lets you make selected correctness claims precise, executable as proof obligations, and machine-checkable.

It does not make the rest of engineering disappear.

1. Where proof fits beside ordinary engineering

Most TypeScript projects already use several correctness tools:

static types
unit tests
property tests
runtime validation
linting
code review
integration tests
monitoring

Proof adds another kind of evidence:

A theorem can establish a formally stated property for every value covered by its quantified variables and assumptions.

That is different from testing selected executions.

The strongest practice combines them.

2. The correctness ladder

Think of assurance as layers rather than one “verified” badge.

1. Parses / elaborates
      ↓
2. Type-correct
      ↓
3. Property stated
      ↓
4. Property proved
      ↓
5. Assumptions inspected
      ↓
6. Source ↔ generated artifacts connected
      ↓
7. Runtime boundaries modeled / identified
      ↓
8. Deployment actually runs the intended artifact

Each layer rules out different failure modes.

A theorem is most valuable when you know exactly which layers it covers.

3. Safe indexing

A familiar TypeScript API might accept:

function get<A>(xs: A[], i: number): A

The type does not encode that i lies inside this particular array.

A dependent interface can instead use:

i : Fin(xs.size)

Conceptually:

def get{A: Type}(xs: Array(A), i: Fin(xs.size)): A := {
  xs[i]
}

In English

“get accepts only an index carrying proof that it is smaller than the size of xs.”

What is gained?

The bounds relationship is no longer a comment or caller convention. It appears in the checked interface.

What is not automatically proved?

This pattern shows how dependent types can turn a runtime precondition into a compile/proof-time relationship.

4. Non-empty collections

Another common invariant:

0 < xs.size

A function can demand explicit evidence:

def first(xs: Array(Nat), h: 0 < xs.size): Nat := {
  xs[0]
}

The parameter:

h : 0 < xs.size

is a proof.

This is more precise than accepting an unchecked array and hoping the caller remembered the precondition.

But note the subtlety: this says the function is correct under the supplied proof and source model. If an effectful/foreign environment can mutate xs between checking the proof and reading the array, that runtime behavior must be modeled or ruled out by the verified subset.

5. Idempotent normalization

Many software systems normalize data:

A desirable property is idempotence:

normalize(normalize(x)) = normalize(x)

A theorem might be:

theorem normalizeIdempotent(x: Config):
    normalize(normalize(x)) = normalize(x) := by {
  ...
}

Why this matters

If normalization is idempotent, repeatedly running it does not keep changing already normalized data.

This can support reasoning about caches, serialization, configuration loading, and convergence.

What it does not prove

It does not prove normalization preserves every piece of information you care about.

You may also need a semantic-preservation theorem such as:

Meaning(normalize(x)) = Meaning(x)

The lesson is reusable:

A mathematically elegant property is not automatically a complete software specification.

6. Encode/decode round trip

Suppose:

encode : Message → Bytes
decode : Bytes → Option(Message)

A strong correctness property is:

decode(encode(x)) = some(x)

Read:

“If we encode any valid message and immediately decode the bytes, we recover exactly that message.”

This theorem covers all values x in the modeled Message domain.

But it does not establish:

Additional theorems can address those separately.

7. Canonical serialization

A second property might be:

encode(x) = encode(y) → x = y

for a serialization intended to be injective.

Or canonicality may be expressed through normalization of byte forms.

Combining properties gives a stronger story:

round trip
+
canonicality / injectivity
+
malformed-input handling
+
resource bounds

Formal verification encourages you to decompose “serializer is correct” into exact claims.

8. Sorting: why one theorem is not enough

A sorting algorithm should usually satisfy at least two core properties.

Orderedness

Ordered(sort(xs))

Element preservation

Permutation(xs, sort(xs))

Why both?

Because:

sort(xs) := []

is trivially ordered.

And returning the input preserves all elements but may not be ordered.

Together, the theorems approximate the ordinary mathematical specification of sorting.

You may also care about:

stability
complexity
comparator consistency

Those are separate properties.

9. Stable sorting

For applications where equal-key elements must retain original order, ordinary permutation preservation is not enough.

You need a property referring to original relative positions for equal keys.

This is a good example of why formal verification changes design conversations:

“Correct sorting” is not one theorem until you define what correct means for your application.

ProofScript cannot choose that policy for you. It can require evidence once you choose it.

10. Authorization soundness

Suppose a runtime decision function returns an authorization result:

authorize(user, action)

A soundness theorem might say:

authorize(user, action) = allowed
→
PolicyPermits(user, action)

Read:

“Whenever the executable authorization function says allowed, the formal policy also permits the action.”

This is valuable because it connects executable decision logic to a declarative policy.

But soundness alone may be too conservative: a function that always denies access satisfies the theorem.

You may also want a completeness theorem:

PolicyPermits(user, action)
→
authorize(user, action) = allowed

Together they establish closer correspondence between the implementation and policy.

11. Security properties need threat models

A theorem about authorization does not automatically prove “the system is secure.”

Questions still include:

Formal proof is strongest when paired with an explicit threat model and clear runtime boundary assumptions.

12. State-machine invariants

Many business workflows are state machines:

Pending → Authorized → Captured → Refunded

You may want to prove an invariant such as:

Captured(state) → PreviouslyAuthorized(state)

Or in transition-preservation form:

Invariant(s)
→
ValidTransition(s, s')
→
Invariant(s')

This theorem says:

“If the invariant holds before a valid transition, it also holds afterward.”

Combined with an initial-state proof, induction over transition sequences can establish the invariant for all reachable modeled states.

This is a powerful fit for formal methods because many application bugs are illegal-state-transition bugs.

13. Financial invariants

Consider a modeled account balance.

A property might be:

amount ≤ balance
→
withdraw(balance, amount) ≤ balance

or stronger:

withdraw(balance, amount) = balance - amount

for Nat balances.

But real financial software needs much more precision:

The theorem is only about the model actually written.

A good formal system makes that limitation visible rather than hiding it behind the word “verified.”

14. Invariants inside loops

For iterative algorithms, a loop invariant states a property that must remain true across iterations.

Conceptually:

initially: invariant holds
step:      invariant + loop body → invariant still holds
exit:      invariant + exit condition → desired postcondition

ProofScript’s verification vocabulary includes invariant for modeled loops where a sound lowering/proof-obligation framework exists.

An invariant is not a runtime assertion by default. It is a proof obligation in the verification model.

15. requires and ensures

A contract can make preconditions and postconditions explicit.

def pred(n: Nat): Nat
  contract value {
    requires hPositive: 0 < n;
    ensures (result) => result < n := by {
      omega
    };
  }
:= {
  n - 1
}

requires

Read:

“The verified guarantee assumes this proposition.”

ensures

Read:

“The returned value must satisfy this proposition.”

result

A name for the returned value inside the postcondition.

Why the proof matters

A failed postcondition proof is not repaired by silently inserting an assumption. The verification layer must produce ordinary valid proof obligations under the same logical foundation.

16. Preconditions should be satisfiable

Suppose:

requires n < 0

for n : Nat.

That precondition is impossible.

A postcondition can then be logically true under the impossible assumption while giving no useful behavior for real callers.

So high-assurance specifications may also prove domain/satisfiability facts:

∃ input, Precondition(input)

or prove that real construction paths can establish the precondition.

Again: validity and usefulness are related but distinct.

17. old(...) and pre-state reasoning

For stateful specifications you often need to compare the result with the state at function entry.

Conceptually:

old(balance)

means:

“The value of balance in the formally defined entry/pre-state.”

This is not a magical snapshot of arbitrary JavaScript memory.

A sound meaning requires a state model that says what the pre-state is, which values can be referenced, and how effects relate entry and exit states.

Without that model, old is just suggestive syntax, not a guarantee.

18. Ghost state

Verification sometimes needs information used only for specification/proof.

That is the role of ghost data.

Examples:

If ghost data is erased from runtime execution, a sound system needs a non-interference discipline: runtime-relevant behavior must not secretly depend on erased proof-only information in an invalid way.

Proof erasure is a theorem/design property, not merely deleting fields from generated TypeScript.

19. Pure functions are the easiest correspondence boundary

For a pure total function:

f : A → B

an execution-correspondence claim can often be stated relatively cleanly:

for corresponding input a,
source evaluation f(a)
corresponds to
target evaluation f_ts(a)

The meaning of “corresponds” still needs representations and observations, but there are fewer external effects to account for.

This is why verified subsets often begin with pure computation.

20. Effects make correspondence harder

Once software interacts with:

“same behavior” requires a more detailed observation model.

For example, should two programs count as equivalent if they return the same result but perform network requests in a different order?

There is no universal answer. The semantic specification must say which observations matter.

21. Numeric semantics are part of correctness

A theorem over:

Nat

uses natural-number semantics.

If a TypeScript emitter compiled that to ordinary JS number without preserving large integer behavior, the theorem would not automatically apply to large runtime values.

A correct backend must either:

Silently changing mathematics to match JavaScript convenience would break the meaning of the source program.

22. Refusal can be a correctness feature

A compiler does not need to translate every valid ProofScript construct into every executable form.

For a verified TypeScript subset, this can be the correct behavior:

valid ProofScript program
+
construct not faithfully supported by verified TS profile
      ↓
explicit unsupported / refusal

That is better than generating code whose semantics only approximately resemble the source.

Verified compiler work such as CompCert makes the same broad point: successful compilation is conditional, and the compiler is allowed to reject rather than emit semantically untrusted output.

22A. Use case: money transfer should conserve value

A transfer function can accidentally debit one account without crediting the other, double-credit after a retry, or apply a fee incorrectly.

A pure model might look like:

function transfer(state: Ledger, from: AccountId, to: AccountId, amount: Nat): Ledger := {
  ...
}

A central theorem could state:

TotalBalance(transfer(state, from, to, amount))
=
TotalBalance(state)

In English

“The modeled transfer moves value between accounts but does not create or destroy total value.”

Why this matters

Accounting systems often have many branches: insufficient funds, fees, reversals, refunds, and retries. A conservation theorem constrains every branch covered by the formal definition.

What it does not prove

It does not automatically establish database transaction isolation, that an external payment processor behaves correctly, or that TotalBalance matches your legal/accounting definition. Those are separate model and environment questions.

22B. Use case: inventory should never become negative

Imagine an inventory reducer:

function applyInventory(state: Inventory, event: InventoryEvent): Inventory := {
  ...
}

A property can say:

ValidInventory(state)
→
Accepted(event, state)
→
ValidInventory(applyInventory(state, event))

where ValidInventory includes the invariant that every stock quantity is nonnegative.

Why proof helps

An inventory bug may occur only after a rare sequence such as:

reserve
→ cancel
→ retry shipment
→ process late return

A state invariant is about all modeled legal transitions, not merely sequences anticipated by test authors.

22C. Use case: retry-safe request processing

Distributed systems retry operations because clients cannot always distinguish “the server failed” from “the server succeeded but the response was lost.”

For an operation intended to be idempotent:

function applyRequest(req: Request, state: State): State := {
  ...
}

state:

applyRequest(req, applyRequest(req, state))
=
applyRequest(req, state)

In English

“Processing the same request twice has the same modeled state result as processing it once.”

This can be crucial for payment initiation, job scheduling, webhook handling, provisioning, and message consumers.

It still does not prove that an external side effect was executed exactly once unless that side effect is part of the formal model/correspondence boundary.

22D. Use case: authorization should have no accidental allow path

A function can have dozens of policy branches:

function authorize(user: User, resource: Resource, action: Action): Decision := {
  ...
}

A soundness theorem:

authorize(user, resource, action) = .allowed
→
PolicyPermits(user, resource, action)

rules out a modeled execution where the implementation says allowed but the formal policy says forbidden.

For stronger correspondence, also consider completeness:

PolicyPermits(user, resource, action)
→
authorize(user, resource, action) = .allowed

The two theorems answer different questions:

soundness    → no unauthorized allow
completeness → no policy-approved request is incorrectly denied

22E. Use case: parsers should not manufacture invalid internal state

Parsers often stand between hostile/untrusted input and trusted internal code.

function parseConfig(text: String): Option(Config) := {
  ...
}

Useful theorem:

parseConfig(text) = .some(config)
→
ValidConfig(config)

A separate round-trip theorem may say:

parseConfig(renderConfig(config)) = .some(config)

These prove different things: validity of successful parsing versus round-trip behavior for rendered valid values.

22F. Use case: schema migration should preserve an invariant

Suppose an application migrates data:

function migrate(old: SchemaV1): SchemaV2 := {
  ...
}

Possible theorem:

ValidV1(old)
→
ValidV2(migrate(old))

If there is a compatibility projection:

projectV1(migrate(old)) = old

may express a stronger round-trip-style property.

This is valuable when migrations touch every stored record: the cost of one semantic mistake can be much larger than a localized UI bug.

22G. Use case: state-machine protocols should reject impossible histories

Consider an order lifecycle:

Pending → Authorized → Captured → Shipped
                    ↘ Refunded
Pending → Cancelled

A transition function can carry an invariant such as:

Shipped(order) → PreviouslyCaptured(order)

or, more directly, prove preservation of a state predicate across every accepted transition.

The value of proof is not that state machines are complicated mathematics. It is that rare event orderings cause real bugs, and induction over transition sequences can reason beyond a finite set of scripted scenarios.

22H. Use case: normalization and canonicalization

Security-sensitive software frequently normalizes identifiers, paths, headers, URLs, or policy input. If two subsystems normalize differently, validation may inspect one representation while execution uses another.

A fundamental law is idempotence:

normalize(normalize(x)) = normalize(x)

Another is preservation of meaning:

Meaning(normalize(x)) = Meaning(x)

when the intended normalization is semantics-preserving.

The first theorem alone does not imply the second. Again, precise theorem choice matters.

23. What does “proved TypeScript” really mean?

The phrase should be used carefully.

A defensible strong claim is:

“This generated TypeScript artifact is connected to the checked ProofScript source by the declared execution-correspondence evidence for this supported subset and toolchain.”

That is much better than:

“Lean proved the JavaScript.”

The first statement names the bridge. The second hides it.

24. Tests still matter after proof

Even a highly verified pure core can be surrounded by unverified integration code.

Tests are still valuable for:

Formal proof lets you spend testing effort differently, not eliminate empirical engineering.

25. Code review changes too

With theorem-backed code, review can focus on new questions:

Formal proof can move review from “does this branch look right?” toward “is this the right mathematical contract?”

26. Proof is most economical for high-value invariants

Not every line deserves a theorem.

High-return targets include:

A practical project can mix ordinary programming and deep proof rather than insisting on maximal proof density everywhere.

27. A good verification report answers five questions

For any “verified” declaration, report:

  1. What program/definition was checked?
  2. What exact proposition was proved?
  3. What assumptions/axioms does it depend on?
  4. What generated artifacts are bound to the claim?
  5. What runtime/compiler correspondence level applies?

A single green badge without these details is weak communication.

28. The final correctness picture

Think of correctness as a chain:

informal requirement
      ↓ specification design
formal proposition
      ↓ theorem proof
checked logical result
      ↓ source / artifact binding
generated Lean / TypeScript
      ↓ semantic correspondence
runtime artifact
      ↓ environment assumptions
real execution

ProofScript’s purpose is to make the middle of this chain dramatically stronger and more explicit, while refusing to pretend that the other links do not exist.

Sources

Next: ProofScript → Lean + TypeScript →