Coming soon: the official stable ProofScript npm/CLI distribution.
Current status: the stable installation workflow documented on this page is not yet generally available. Treat every npm/CLI command below as a preview of the intended interface until a production release explicitly marks it available. When this page was last checked, npm exposed the pre-release
proofscript@0.1.0-alpha.1; this documentation does not treat that alpha as the stable toolchain described below. Re-check package version, dist-tags, CLI behavior, and release notes before publishing or following these commands.
Home · Docs · Type Theory · Proofs · Verified Software · ProofScript → Lean + TypeScript · Reference · Examples · Download
The full v0.1 language reference specifies psc as a proposed normative interface at the behavior level; the reference explicitly does not claim that a command is implemented merely because its behavior is specified.
This page therefore documents the intended mature npm-based workflow without presenting it as currently stable or production-ready. Exact commands, flags, package versions, generated paths, and verification guarantees must be validated against the actual release before use.
Status reviewed for this documentation revision: 7 September 2026.
| Item | Website status |
|---|---|
| Official stable npm package | Coming soon / not yet treated as generally available |
| Pre-release npm package | proofscript@0.1.0-alpha.1 was discoverable when last checked; do not treat it as the stable release |
Stable psc CLI contract |
Coming soon / release-dependent |
psc check |
Specified as intended behavior; re-check implementation status |
psc build |
Specified as intended behavior; re-check implementation status |
psc emit-lean |
Specified as intended behavior; re-check implementation status |
psc certify |
Specified as intended behavior; re-check implementation status |
psc verify |
Specified as intended behavior; re-check implementation status |
This table is deliberately conservative. The npm registry snapshot can change at any time. Re-check it before publishing a release website or giving users installation instructions.
Coming soon — preview, not a current stable installation instruction.
Once an official stable npm release is published, the intended project-local form is:
# Planned stable workflow — re-check availability first.
npm install --save-dev proofscript
A project-local dependency is preferred for reproducibility because the ProofScript version can be pinned in the lockfile.
The intended invocation is:
# Planned stable workflow — not guaranteed available yet.
npx psc --version
Coming soon. For interactive use, the intended stable global installation is:
# Planned stable workflow — re-check availability first.
npm install --global proofscript
Then:
psc --version
Do not rely on this until the official stable release documents the package and executable. For CI and reproducible projects, a local pinned dependency should remain preferable.
Create:
proof/hello.ps
with:
const answer: Nat := {
42
}
theorem answerCorrect: answer = 42 := by {
rfl
}
consthere is the TypeScript-oriented top-level alias for canonicaldef.
For a beginner, think of the workflow as four increasingly strong questions:
1. Can ProofScript parse and elaborate this source?
2. Do the program definitions type-check?
3. Do the theorem/proof obligations check?
4. If target correspondence is claimed, does the release provide the required artifact evidence?
A successful syntax/type check is not automatically the same as a proof of every desired property. Likewise, generated TypeScript is not automatically covered by a source theorem unless the selected correspondence profile establishes that connection.
Planned psc interface — coming soon / release-dependent.
Conceptual command:
npx psc check proof/hello.ps
Checking should distinguish at least:
accepted
rejected
unsupported
resource exhausted
implementation error
A missing implementation feature should not be reported as though the theorem were mathematically false.
Planned psc interface — coming soon / release-dependent.
Generate an inspectable Lean artifact:
npx psc emit-lean proof/hello.ps
A generated Lean view may look like:
def answer : Nat := 42
theorem answerCorrect : answer = 42 := by
rfl
The generated artifact is useful for:
Lean replay checks the generated Lean declarations. It is not, by itself, proof of source-to-Lean fidelity or TypeScript execution correspondence.
Planned psc interface — coming soon / release-dependent.
For the supported TypeScript compilation profile:
npx psc build proof/hello.ps
or the release’s equivalent command.
The build may produce:
build/
hello.ts
hello.lean
hello.pscert
The exact output layout is release-specific.
Planned psc interface — coming soon / release-dependent.
A mature workflow verifies a certificate/manifest:
npx psc verify build/hello.pscert
The verifier should report what was actually checked:
source identity
exact theorem statement
assumptions
Lean replay/check outcome
TypeScript artifact identity
correspondence profile and outcome
A certificate hash is not semantic proof by itself; it identifies the artifact to which proof/validation evidence applies.
{
"scripts": {
"proof:check": "psc check proof",
"proof:build": "psc build proof",
"proof:verify": "psc verify build"
},
"devDependencies": {
"proofscript": "<pinned-version>"
}
}
Pin the actual release version according to your package policy rather than leaving <pinned-version> in a published project.
A typical CI sequence is:
install exact dependencies
↓
check .ps sources
↓
build generated artifacts
↓
replay/check Lean artifact if profile requires
↓
verify TypeScript correspondence certificate
↓
run ordinary tests/integration tests
Formal verification and ordinary CI tests are complementary.
For high-assurance builds, record:
“Latest” is convenient for experimentation but weak for reproducible proof claims.
Even if ProofScript has a standalone checker, generated Lean is valuable because it gives an independently inspectable logical view in a mature proof ecosystem.
You can ask:
What exact theorem did the frontend generate?
Which definitions does it use?
Which assumptions are present?
Does the pinned Lean toolchain accept it?
That is useful evidence independent of the TypeScript execution path.
TypeScript is the JavaScript-ecosystem execution artifact.
Keeping it inspectable supports:
ProofScript’s value is not to hide TypeScript. It is to connect executable TypeScript to a stronger source-level semantic and proof story for the supported subset.
npm provenance/attestations can help establish where a package artifact came from and which source/build workflow produced it.
That is valuable supply-chain evidence, but do not confuse provenance with semantic correctness.
A provenance statement can answer:
“Where did this package come from?”
Proof/correspondence evidence answers a different question:
“What semantic property was checked about these artifacts?”
Use both where appropriate.
Before changing a ProofScript version in a high-assurance project:
Proof artifacts are versioned engineering outputs, not timeless green checkmarks.
Once a stable package is available, the normal npm uninstall forms are expected to be:
Local package:
npm uninstall proofscript
Global package:
npm uninstall --global proofscript
Because package availability is time-sensitive, check the official ProofScript release/package status again before using these commands. This page intentionally prefers a conservative message—coming soon—over implying that a pre-release or experimental package is a stable toolchain.
Back to: Home