src/rust/corpus/isabelle.rs — Isabelle/HOL AFP .thy

src/rust/corpus/metamath.rs — set.mm

src/rust/corpus/mizar.rs — MML .miz / .abs

src/rust/corpus/hol_light.rs — Multivariate / Core

src/rust/corpus/hol4.rs — HOL4 Script files

src/rust/corpus/dafny.rs — .dfy

src/rust/corpus/why3.rs — TOCCATA gallery .mlw

src/rust/corpus/fstar.rs — F* examples .fst

src/rust/corpus/tptp.rs — TPTP problem library

src/rust/corpus/smtlib.rs — SMT-LIB benchmarks

src/rust/corpus/acl2_books.rs — ACL2 community books

src/rust/corpus/proofnet.rs — ProofNet

src/rust/corpus/minif2f.rs — MiniF2F

src/rust/corpus/naproche.rs — Naproche libraries

src/rust/corpus/mathcomp.rs — Coq MathComp (separate from coq.rs heuristic)

src/rust/corpus/iris.rs — Coq Iris

src/rust/corpus/cubical_agda.rs — Cubical Agda stdlib

src/rust/corpus/mod.rs — append pub mod isabelle; etc. No reordering of existing pub mod lines. No edits to existing functions.

data/synonyms/hol_light.toml

data/synonyms/hol4.toml

data/synonyms/metamath.toml

data/synonyms/mizar.toml

data/synonyms/dafny.toml

data/synonyms/fstar.toml

data/synonyms/why3.toml

data/synonyms/acl2.toml

data/synonyms/pvs.toml

data/synonyms/tlaps.toml

data/synonyms/imandra.toml

data/synonyms/_msc2020.toml — MSC2020 cross-prover dictionary

data/synonyms/_wordnet_math.toml — WordNet math entries

data/synonyms/_conceptnet_seed.toml — pre-fetched ConceptNet seeds (offline-resilient)

src/rust/exchange/tptp.rs — universal first-order ATP exchange

src/rust/exchange/smtlib.rs — SMT-LIB exchange / round-trip

src/rust/exchange/smtcoq.rs — SMT proofs into Coq

src/rust/exchange/lambdapi.rs — Dedukti’s successor

src/rust/verification/portfolio.rs — extend default() to include DReal, OpenSmt, SmtRat, MathSat, SPASS, Princess, iProver, Twee, Princess in their respective tiers. Pure additive — no semantic changes to existing solver entries.

src/rust/verification/bayesian_arbiter.rs — posterior over verdict given evidence stream

src/rust/verification/dempster_shafer.rs — belief mass combination

src/rust/verification/pareto_arbiter.rs — multi-objective Pareto frontier voting

src/rust/suggest/synonyms.rs — add SynonymTable::with_msc2020() method; add merge_external() for cross-prover dictionaries. Existing load() / alternatives() UNCHANGED.

src/rust/integrations/conceptnet.rs — add prefetch_to_cache() method using _conceptnet_seed.toml. Existing related_concepts() UNCHANGED.

docs/architecture/VERISIM-ER-SCHEMA.adoc — formal entity
relationship definitions

crates/echidna-wire/schemas/verisim_er.capnp — Cap’n Proto schema (if compatible)

docs/decisions/2026-06-01-saturation-campaign.adoc — ADR

docs/CORPUS-ADAPTERS.adoc — index of all corpus adapters with their parsing strategy + canonical source URL

docs/handover/PROVER-CORPUS-SATURATION-LANE.adoc — this file