jsCoq: the Coq proof assistant running in a browser tab

What a Coq port to WebAssembly actually buys you

The repository description is plain: a port of Coq to JavaScript, run Coq in your browser. The README frames jsCoq as an Online Integrated Development Environment for the Coq proof assistant, and states two aims, to enable new UI and interaction possibilities and to improve the accessibility of the Coq platform itself.

The accessibility point is the one that matters most in practice. Coq is a program with a demanding dependency chain: an OCaml toolchain, opam, dune, and a build of the proof assistant itself. The Makefile in this repository shows how deep that goes, with a vendor path for the Coq sources, separate dune workspaces for 32-bit and 64-bit builds, a list of Coq packages to install including coq, coq-core and coq-stdlib, and a switch-based dune invocation that switches between build contexts.

jsCoq removes all of it. The README states that no servers or external programs are needed and that jsCoq is written to conform to ES2017, so any recent standard-compliant browser should be able to run it. A student opens a URL and is in a working Coq environment with a proof assistant that actually checks their proofs.

The mechanism is visible in the package manifest. The runtime dependencies are the OCaml WebAssembly compiler output, ocaml-wasm at 4.12, with janestreet-base, num and zarith packages built for that same OCaml version, plus wasi-kernel for the system interface. The Coq kernel is OCaml code, so porting Coq to the browser means compiling that kernel to WebAssembly and shipping it as a JavaScript package, which is exactly what these dependencies are. The build tooling follows the same shape, with esbuild for bundling, CodeMirror for the editor, react and react-dom for the UI layer, and cypress for the end to end tests.

The tree is organised around that split, with a backend/ directory for the proof engine, a frontend/ for the interface, a lib/ and etc/ for shared pieces, a vendor/ directory, and a separate cli entry point.

The stable build versus the development build

Two versions exist at once, and confusing them is the most common way to misjudge this project.

The stable version is jsCoq 0.17.1, supporting Coq 8.17.1, and it is the one served at coq.vercel.app. The recent releases list confirms it: v0.17.1, tagged as Night Slip, was published on 2023-10-02, with v0.16.0 from 2022-09-22 and v0.15.1 from 2022-05-05 before it. So the newest published artifact is more than two years old as of October 2026.

The development version is jsCoq 1.99.1, targeting Coq 8.17 to Coq 8.21, and it is based on the new Flèche document manager, which the README links to the coq-lsp project. The README says the development version has significant changes and asks people who want to help with this effort to get in touch.

The version numbers encode this. 0.x is the old numbering scheme and 1.99.x is the pre-release convention where 99 signals something not yet stable. The package.json in the repository is at version 1.99.2, while the Makefile pins COQ_VERSION := v8.20, which is the branch the build targets. The default branch of the repository is v8.20, so the working trunk is named after the Coq version it tracks.

The licence is worth flagging. The repository metadata classifies it as Other, a custom licence GitHub cannot classify, and a LICENSE file is present at the root. The README text shown does not name a licence, so anyone planning to redistribute a jsCoq-derived teaching artefact should read the LICENSE file directly rather than assume a permissive one.

Maintenance is mixed in the same way. The last push was on 2026-06-15, so the repository is not dormant, but the published release has not moved since 2023, and the README says the project is fully run by unpaid volunteers and is in need of funding, in particular with documentation and fine tuning the project.

Proof stepping, the scratchpad and local storage

The interaction model is the part that differs most from a terminal Coq session, and it is where the IDE framing earns its place.

Once jsCoq finishes loading, you step through the proof using the arrow buttons on the toolbar, or with keyboard shortcuts. The table gives three: Alt-N or Alt-Down goes to next, Alt-P or Alt-Up goes to previous, and Alt-Enter or Alt-Right goes to cursor. The main page showcases jsCoq with a variety of proofs available from an Examples drop-down menu.

The scratchpad is the other half. You can open a blank editor and experiment with your own Coq developments there, and the same keyboard shortcuts apply. The important detail is persistence: the scratchpad's contents are saved in your browser's local storage, IndexedDB specifically, so they are not lost if you close the browser window or refresh the page. That is a real difference from the terminal, where losing a window loses the buffer, and for a student experimenting it removes a whole class of frustration.

File handling is also built in rather than bolted on. Ctrl-S saves the file with the last name provided, or untitled.v. Ctrl-Shift-S saves file as, which prompts for a file name and also has options to download or share the content. Ctrl-Alt-S saves the file to disk using the browser's Save dialog or a preset destination. Ctrl-O opens a file, with a prompt for the file name and tab completion support, and Ctrl-Alt-O opens a file from disk using the browser's Open dialog. On Mac, the README notes you replace Ctrl with the command key and Alt with the option key.

Dragging .v files from your local drive onto the scratchpad opens them, and dragging multiple files opens a project pane to the left of the editor so you can switch between them. The README marks that multi-file pane as still experimental, which is worth knowing before you build a course workflow around it.

The file chooser is the browser's, not a native dialog, so it cannot browse arbitrary paths the way a native application can. That is a boundary of the platform approach rather than a defect in the project.

Embedding jsCoq in your own document pages

The path for people who want to publish proofs rather than just use them is documented on a dedicated embedding page, docs/embedding.md, and the quick setup is short.

npm install jscoq

After that, you copy and adapt the template page, with the README pointing at examples/npm-template.html in the repository as the starting point, and refer to docs/embedding.md for the advanced options and the jsCoq HTML embedding API. The examples directory in the tree holds several of these, including npm-template.html, a scratchpad.html page and an sdk-demo directory.

The template-based approach is the one the project recommends for classes. The README names the coqdoc template, a separate repository, as the easiest way to use jsCoq 0.17.1 for classes, and the package.json exposes a second binary, jscoqdoc pointing at frontend/classic/js/jscoqdoc.cjs, which is the document generator side of that.

That coqdoc workflow is the interesting part for anyone teaching. A course then becomes a set of web pages where each proof is embedded and interactive, the reader can step through the tactic script themselves, and the entire course is served as static files with no server to maintain. It is the same model as the Software Foundations, which the README lists among the examples with the LF and PLF volumes available at jscoq.github.io/ext/sf.

The developer information section points at CONTRIBUTING.md, and the tree shows the supporting material a real project has: cypress/ for end to end tests with a cypress.config.ts, a tests/ directory, a dune/ directory and dune-project for the OCaml side, a jscoq.opam file for the opam package, and esbuild.mjs, esbuild-cli.mjs and esbuild-pkg.mjs as separate bundling entry points.

A CLI binary is also published, jscoq pointing at ./dist-cli/cli.cjs, which means the same engine can be driven outside the browser. The README does not document that path in detail, so treat it as an existence claim rather than a documented workflow.

Sharing a proof, and its expiry date

The sharing feature is simple and has a limitation you should know about before you rely on it for coursework.

A small pastebin-like server based on Hastebin is available for sharing .v files between users. You open the save dialog with Ctrl-Shift-S and click Share, then share the URL from the browser's location bar. The semantics are spelled out: the URL represents the state of the document at the moment it was shared, this state is read-only, and every time you click Share, a fresh URL is generated.

The limitation is the lifetime. Shared content is not saved forever, though documents are typically available for a period of around 30 days. For a shared link that a student clicks once, that is plenty. For a link you put in a course syllabus and expect to still work next term, it is not, and the fix is to embed the document rather than share it.

The read-only aspect is the other constraint worth internalising. A shared URL is a snapshot, so a reader cannot step through and modify it, only inspect. That is the right default for a link you paste into a chat, but it means sharing is not a substitute for embedding.

There is no account system described and no server of your own is required, since the sharing server is provided and the main deployment at coq.vercel.app is a static site. The privacy consequence follows from the architecture: a shared document is a URL on someone else's server, so anything you share is readable by anyone with the link for as long as it lives.

Where jsCoq is the wrong choice

There are three limits, and the first is version-bound.

The first is that the stable build is pinned to Coq 8.17.1 while the Coq line has moved on to 8.20 and 8.21. If your material, your course or your research depends on a library that only exists for a recent Coq release, the stable jsCoq cannot carry it. The development branch targeting Coq 8.17 to Coq 8.21 is where that work is happening, but the README itself says it has significant changes and is based on the new Flèche document manager, so it is a moving target rather than a drop-in replacement.

The second is that jsCoq is the Coq frontend and kernel, not the package ecosystem. Coq users depend heavily on libraries, from the Software Foundations to Coq Equations, and jsCoq ships the kernel and the standard library as Coq would, but the standard route for adding a package in Coq is opam and dune with a version pin. That route is exactly what the browser distribution does not offer. The examples list shows what is possible, including an introduction to the Coq Equations package taken from the official documentation, and the IRIS program logic by Robbert Krebbers and colleagues, but these are curated examples hosted as pages, not a package manager.

The third is that the browser is a distribution choice with its own constraints. Compilation and evaluation happen in the tab, so a heavy proof or a large file will feel it, and the IDE features are the browser's own file dialogs, which cannot reach arbitrary paths. The multi-file project pane is marked experimental. And the project states plainly that it is community-developed by a team of contributors, in need of help in particular with documentation, funding and fine tuning, and fully run by unpaid volunteers. That is not a disqualification, but it is a signal about the support you should expect for a course dependency.

The honest alternative depends on what you are doing. For teaching, the alternative to jsCoq is a locally installed Coq plus an editor such as Proof General or VS Code with the Coq extension, which gives you current Coq versions, the full package manager and real filesystem access, at the cost of every student having to install an OCaml toolchain before the first lesson. For publishing, the alternative is a static build of your .v files with coqc and coqdoc on a build server, which produces the same static output but from the real Coq toolchain and with no browser kernel involved. jsCoq's case is the interactive one: a live proof environment inside a page, reachable by anyone with a link, which neither of the alternatives gives you.

Editorial conclusion

Adopt jsCoq if you teach Coq, want a zero-install link for students, or need to publish a proof that people can click and step through, since the browser distribution removes every install barrier. Do not adopt it if you need the current Coq release or a package ecosystem, because the stable build is pinned to Coq 8.17.1 and the newest published release is from 2023. Before committing, check the default branch v8.20 and the Flèche-based development build, and note the last push was on 2026-06-15.

Frequently asked questions

Official sources

1. Issues
2. jscoq/jscoq on GitHub
3. Project website
4. README
5. Releases