Plectis

Check what a change preserves and what it invalidates.

Plectis is a public Python toolkit for experiments in AI-assisted research. Its workflow operations use formally verified decision cores to plan reruns, check interface replacements and derive public-only reports. This research prototype also includes reference components for proof checking, agent reliability, forecasting and keeping documents consistent with their sources. A fourth verified core checks whether their replay evidence satisfies the declared source, input, claim-policy and receipt contract. Twelve component computations also have their own specifications and proofs.

Run the workflow example · Check component replays · Inspect the proofs · Browse the reference toolkit · Documentation · Source map

The current experiment asks a simple question: “I changed this workflow. Which results can I keep, and what must run again?” With Python 3.11+, try:

git clone --depth 1 https://github.com/wcook04/plectis && cd plectis
PYTHONPATH=src python3 examples/operations/evaluation.py --format text

The example changes a scoring rule: eight results are reused, three tasks rerun, and one external action stays blocked. An old worker cannot publish over the new result. Everything runs locally in a temporary directory, without model calls. Read the walkthrough, then import the operations you need:

The generated Python is the code these APIs call. The proofs cover the supplied graph, transition models and report language; Python adapters, SQLite and external services remain outside them. These are independently importable research prototypes. An ordinary cache makes the same reuse decisions in this example; practical benefits over that baseline still need evaluation.

To recheck the proofs with Dafny 4.11.0:

make verify-operations DAFNY=/path/to/dafny

This verifies the three workflow cores and replay admission, regenerates Python byte for byte and requires deliberately broken variants to fail. make check checks the saved hashes without running the prover. Read the assumptions and trusted tools or copy and install an operation.

For the broader reference toolkit, run this after cloning the repository as shown above:

PYTHONPATH=src python3 -m plectis tour --format text .

The tour lists project files and suggests a task. It does not run your tests or change your source.

Yes, for the four operation APIs above, the documented local commands and selected examples. Start with the workflow study or the quickstart, then check the chosen component's inputs, dependencies and stated limits before adapting it to your own project.

The 88-component catalogue lists individual replays, not an integrated public research platform; check each replay's requirements. The overview shows one command's input, output and limits. The larger private workbench is separate from this clone.

A component runs its checker on supplied inputs and saves a receipt. The shared replay host captures source and input identities, the declared claim policy, the returned result, the public payload sent to the receipt writer, and the saved receipt. A Dafny-verified admission rule then requires exactly one matching result for every selected component, with no missing or duplicate rows, changed identities, altered public payloads or missing required execution evidence. Replay commands call its generated Python.

make component-replays

This runs the current catalogue and writes new results under .microcosm/component-replays/; it needs the components' native tools, including Lean/Lake and Swift. The replay guide lists prerequisites and the study shows the failure cases behind the design.

To replay one exact component ID with its declared inputs, run:

plectis component-replay pattern_binding_contract --root .

The result covers that selected component only. It writes a fresh run below .microcosm/ and reports missing inputs or tools without passing them. Receipts mark runtime source identity as package_roots_v1: byte and mode hashes for microcosm_core and plectis, including generated kernels. Standard-library and third-party dependency behavior remains trusted; the receipt separately binds project source, routes, registry, core policy, standards and inputs. The shared replay host and isolated backend API keep receipt observation and admission in the existing execution path.

The component proof index identifies twelve computations with their own verified specifications and generated implementations. Their adapters supply normalized observations; the component writes a result and receipt, and the separate admission core checks the captured replay evidence. Hashing, file capture, host normalization and the producer's choice of public receipt fields remain tested Python boundaries. A replay cannot inherit a proof of component correctness from another core or from the number of components that passed.

AI-assisted research can span many sessions, files and failed approaches. Plectis explores how to preserve that work so another person can understand what was tried, check the results and choose a useful next step. Experts can contribute a correction or direction without operating the AI themselves.

This toolkit publishes selected parts of that effort. The mathematics repository contains the papers, proofs and open questions; the website explains both. The project overview relates these parts to other research tools.

A separate report-compilation experiment changes one mixed recipe, derives a public-only program and checks that a private condition cannot control whether a public line appears. An ordinary public-only renderer produces the same output; the value of maintaining one checked recipe still needs evaluation. Run it with:

PYTHONPATH=src python3 examples/operations/public_views_recipe_change.py

An AI says: “I committed the fix and the tests passed.” The completion-checking guide shows how one component checks those claims using a sample Git repository and actual pytest runs. It verifies three supplied claims and rejects four deliberately incorrect ones. You can follow the result back to the code that checked it.

Two more worked guides show different uses:

• Change a prompt-injection example and see a checker reject an inconsistent permission in saved records.
• Prepare a research question with a tentative answer, alternatives and proposed observations for an expert.

Try the second example from the clone, without installing anything:

PYTHONPATH=src python3 -m plectis hypothesis-handoff \
  --input examples/hypothesis_handoff/independent_evaluation.json --format text

It validates the supplied file and prints the question and proposed investigation. It does not answer the question, contact an expert or call a model. Each guide explains what its example tests and what remains untested.

There are 88 components, grouped into seven areas. A component is a named program or group of related programs, with its own instructions and stated limits. Some run a computation or an external tool; others compare supplied records against rules. An entry in the catalogue is not a promise that every example can run in every environment: its page lists required tools and source files, and the runner reports unavailable requirements.

Explore the system map →
_{Select a component or rule on the website to follow its connections.}

Browse the live component pages, papers and films on the Plectis website. For text indexes and source links, use the agent navigation guide. For mathematical papers, Lean proofs and open questions, follow the Plectis Erdős reader's guide or the mathematics map.

To search component descriptions from the terminal:

PYTHONPATH=src python3 -m plectis comprehend --slice mechanism --format text
PYTHONPATH=src python3 -m plectis comprehend --first-action "prompt injection" --format text

The search uses phrase and word matching to suggest a command and relevant files. It neither calls an AI model nor executes the suggested command.

Most components run independently. They share command handling, file formats and a catalogue that names each component's code, inputs, checks and saved results. The catalogue also supplies the generated documentation and maps. The connections between components are recorded where they exist; the seven areas are a browsing aid, not seven stages that every run executes.

To understand a component, open its example input, the source function that processes it and the output it produces. Compare that output with the test or expected result. Then change an input in a disposable copy and check whether the result changes as expected. The worked guide follows this path through one component.

The project tour is a separate orientation command. It mostly classifies filenames and paths, with limited inspection of Python entry points. It writes a file inventory, suggested tasks and a simulated task record under .microcosm/, an ignored directory retained from the project's former name. A saved run result is called a receipt in the source. It records what ran and which inputs and results it refers to; it does not by itself prove a claim. To see the tour's structured output:

PYTHONPATH=src python3 -m plectis tour --card .

Architecture maps the implementation. The maintainer guides explain command dispatch, data ownership and how to regenerate the maps.

A coding agent is an AI assistant that can read files, run commands and edit code. You can use your own to explore this repository. Open a current clone and ask, for example:

Read AGENTS.override.md. I want to understand how this project checks an agent's claim that a task is finished. Find the relevant example, explain its inputs, run it, and show me the result and the code that checks it. Explain what this run establishes and what it leaves untested. Include the checkout commit and commands so I can repeat it.

The agent quickstart explains where to save results. AGENTS.md contains the editing instructions. The toolkit's local examples do not require a model API key; your chosen coding agent has its own account and provider requirements.

The basic commands run from a clone with Python 3.11 or newer, without third-party runtime dependencies. The shell examples above work on macOS, Linux and WSL. In Windows PowerShell, first set $env:PYTHONPATH = 'src', then use python -m plectis in place of PYTHONPATH=src python3 -m plectis. Individual examples may require Git, pytest, Lean or other tools; follow the selected example's instructions.

To install the shorter plectis command on macOS or Linux:

python3 -m venv .venv
.venv/bin/python -m pip install .
.venv/bin/plectis tour --format text .

Use the virtual environment if your system Python reports externally-managed-environment. For development dependencies, Windows installation commands and other options, see Quickstart, Contributing and troubleshooting. The older microcosm command remains an alias.

The component HTTP API serves the validated public component index as read-only JSON for component, claim, proof, coverage and graph queries. Run plectis serve-components for a loopback listener; its retained evidence remains separate from current byte checks and fresh proof or replay results.

Component descriptions are read from capsule compression through component_descriptions.py. The atlas owns structure and commands; the registry retains normative claims.

For the verified operations, start with formal/, src/plectis/ and examples/operations/. The broader component catalogue, generated indexes and recorded experiments remain available separately; they are not prerequisites for using these APIs.

plectis/
├── formal/               Workflow, replay and component proofs with negative mutants
├── src/
│   ├── plectis/           Operation APIs, component kernels and CLI entry points
│   └── microcosm_core/    Python implementation; components in organs/
├── docs/                 Guides, reference, maintainer notes and paper guide
├── examples/             Runnable examples and checked source bundles
├── fixtures/             Prepared inputs and expected results
├── tests/                Executable checks
├── core/                 Component registry and configuration
├── atlas/                Generated maps and indexes
├── standards/            Requirements checked by the tools
├── skills/               Procedures for agents
├── paper_modules/        Component explanations
├── paper/                Toolkit paper source
├── receipts/             Recorded example results
├── assets/               README and social preview images
└── scripts/
    ├── build/            Documentation and map generators
    ├── check/            Source, projection and boundary checks
    ├── release/          Packaging and release verification
    ├── inspect/          Compact inspection cards
    └── papers/           Publication corpus tools

Start with the examples; use the fixtures and recorded results to understand their checks. Your own runs go in the ignored .microcosm/ directory. The paper guide distinguishes the toolkit paper's source from the main research papers.

The root ORGANS.md, ARCHITECTURE.md and AGENT_ROUTES.md are generated indexes. AXIOMS.md, PRINCIPLES.md and ANTI_PRINCIPLES.md contain the doctrine shown in the map. Makefile and .github/workflows/ run the checks. The maintainer architecture guide identifies which files to edit and which builders to run. The script guide explains each maintenance role; make check enforces their placement in Git and CI.

The source_modules/ directories inside exported examples contain copied implementations with provenance manifests. Component replays and installed examples depend on them. Older receipts retain the inputs and limits of their original runs; a new replay writes a new result. A historical receipt or catalogue entry does not itself prove a component; follow its source and, where available, its component proof.

The documentation index separates human guides, reference maps and maintainer instructions. Directory READMEs explain the examples and reference collections. The terminology guide translates older names you may encounter in source files.

A pass is about a particular input and check. The component records classify the result: a computation run now, a replay of supplied data, or a comparison of files. That is why the source, test and stated limits are published together.

This is a research prototype containing selected public source files and examples. It does not contain enough code or data to reconstruct the private system. It is not a hosted service or a production security product, and has no model-provider affiliation or endorsement. Public examples do not establish the reliability of the unseen private workbench.

A useful contribution can be small: an input that exposes a mistaken check, a clearer explanation, an easier first command or an improvement to one tool. Contributing explains how to report a reproducible mismatch, try an entry-route experiment or propose an infrastructure change. Mathematical contributions belong in the companion repository.

From the clone root:

make check   # fast registry and Lean-source checks; no installation
make ci      # tests, command smoke tests and a fresh package installation

make ci creates temporary environments and installs build and test dependencies, so it may need network access. make help lists narrower checks. Maintainers can run every registered public example with make component-replays and recheck the workflow and replay cores with make verify-operations DAFNY=/path/to/dafny. Run make verify-components DAFNY=/path/to/dafny for the twelve component kernels. The validation guide explains dependencies, release records and generated files. Edit their source and run the owning builder rather than changing generated maps or recorded results by hand. The release review records the candidate’s checks; source status explains which source material is included.

The project videos page describes the recordings and their subjects. In the introduction, Will explains the wider programme: AI produces much of the research and code, and he uses it to prepare papers, maps and explanations that other people can inspect. The toolkit in this clone is one part of that work.

The Python components and experiments in this clone are one part of Plectis. The related repositories have different jobs, with their own setup instructions and evidence. Follow the project that matches what you want to read or run.

Code Map and Demo Take, also shown in the films, are private tools. The Plectis website links the public projects and demonstrations; this clone does not install the private workbench.

How this was built. William Cook sets the direction and is responsible for the public claims; AI coding agents write and maintain most of the code. PROVENANCE.md records authorship and third-party sources.

The project was called Microcosm until 21 June 2026. It became Plectis to avoid confusion with Southampton's earlier Microcosm hypermedia system, without implying endorsement or affiliation. Old names remain in package imports, output paths and historical records for compatibility with existing tools.

For private security reports, see SECURITY.md. To cite the software, use CITATION.cff. Copyright 2026 William Cook; licensed under Apache 2.0, with details in LICENSE and NOTICE.

The companion's current results guide owns its mathematical claims. This toolkit's recorded source and release links are preserved in the companion reference.