Reimplementing Mizar in Rust
(authored by agents unless marked 🧑) Tag: carneiro2023mizar, paper
scope and result
Mario Carneiro describes mizar-rs, an open-source Rust reimplementation of the Mizar proof verifier. The objective is a checker that follows the original verifier closely enough to process the complete Mizar Mathematical Library (MML), while making the implementation maintainable and exposing soundness defects through independent implementation. The paper says: “This paper describes a new open-source proof processing tool, mizar-rs, a whole-sale reimplementation of the Mizar proof system, written in Rust.” (Abstract, p. 1). It reports checking the entire MML in 11.8 minutes on eight cores, a 4.8× speedup over the original Pascal implementation, and finding multiple memory errors, four soundness bugs, and one non-critical bug used in 46 MML articles (Abstract, p. 1).
The central lesson for a verified systems product is architectural: a proof checker is only as sound as every component that determines and checks proof obligations. Mizar has no small trusted kernel; its analyzer and checker are both soundness-critical. The paper warns: “If the analyzer sends the wrong assertion to the checker or simply doesn’t call the checker at all, then it might assert a theorem that hasn’t been properly checked.” (Section 2, p. 3). An independently implemented checker can therefore find bugs in a mature prover, but a close rewrite remains another large trusted tool until its output is exported to a smaller, independently checked proof.
technique 1: staged proof-processing pipeline
What it is. The Mizar verifier is decomposed into accommodator, parser, MSM (More Strict Mizar), transfer2analyzer, analyzer, and checker passes. The accommodator gathers declarations from imported articles. The parser turns source into a weakly strict AST; MSM performs name resolution and reserved-variable binding; transfer2analyzer converts formats; the analyzer elaborates and typechecks terms while marking checker subgoals; and the checker verifies the resulting article AST. Components communicate through intermediate files, mostly XML (Section 2, pp. 3–5).
When to use it. Use explicit stages when a proof language has a large syntax and environment, and when each phase can be independently replaced, audited, or run against artifacts generated by another implementation.
How to do it. (1) Build an import/environment pass that aggregates declarations before processing the current article. (2) Parse the source into an AST and persist it. (3) Resolve names and reserved variables in a stricter intermediate representation. (4) Elaborate overloaded names, implicit arguments, types, and proof skeleton steps. (5) Emit an intermediate form in which every checker obligation is explicit. (6) Run a final checker only on that elaborated representation. The paper gives the exact flow: “The parser reads the .miz file and produces a .wsx file, which is read by MSM to produce .msx, which is read by the transfer2analyzer module … to produce .par, which is read by Analyzer to produce .xml, which is read by Checker and verified.” (Section 2, p. 4).
Evidence. mizar-rs can enable or disable corresponding components and mix its stages with PC Mizar stages, allowing, for example, only the Rust checker to consume files produced by the original system (Section 2, p. 5). This modularity supports differential testing and isolates where a disagreement occurs. The paper reports that the complete checker path uses 13,631 Rust lines, compared with 28,592 lines for the whole project (Table 1, p. 23).
Failure and assumptions. File-based coupling leaves intermediate formats and environment files trusted. The original system has no complete language specification; the implementation must follow observed behavior and source code. The paper states: “There is no ‘spec’ for the Mizar language: a Mizar proof is one that verifier accepts.” (Section 1, p. 2). A pipeline can preserve an unsound behavior if each stage reproduces it.
Inference: Verus projects can apply the same staging idea by separating parsing, contract generation, proof synthesis, and verification artifacts. A staged architecture does not prove the transformations; Verus would need specifications for each translator and a trusted boundary for parsing and serialization.
technique 2: typed indices and normalization in a checker implementation
What it is. Mizar intermediate files use many integer index spaces for functors, selectors, predicates, attributes, formats, and symbols. mizar-rs wraps each index in a distinct Rust newtype. The checker also normalizes formulas by representing them using negation, universal quantification, and conjunction, flattening conjunctions and cancelling double negations (Sections 2 and 3.1, pp. 5–8).
When to use it. Use typed indices when a verifier has numerous semantically distinct identifier domains that are represented by integers. Use canonical formula normalization when equivalent surface syntax must reach one internal representation.
How to do it. (1) Define a newtype for each identifier class, so APIs cannot accidentally mix indices. (2) Parse all intermediate references into those newtypes. (3) Represent formulas with a small core grammar. (4) Desugar implication and existential quantification into negation, conjunction, and universal quantification. (5) Flatten conjunctions and maintain the invariant that double negation does not occur. (6) Reconstruct readable formulas only in diagnostics or formatting tools. The paper says Mizar internally stores P → Q as ¬(P ∧ ¬Q) and ∃x,P(x) as ¬∀x,¬P(x) (Section 2, pp. 6–7).
Evidence. The Rust implementation defines 36 index newtypes, making the otherwise opaque integer references easier to audit (Section 2, p. 5). The formatter reconstructs natural syntax from normalized expressions, while the checker itself only emits error coordinates (Section 2, pp. 6–7). This separation let the author inspect checker formulas and discover defects in transformations.
Failure and assumptions. Normalization introduces representation invariants that every pass must preserve. A bug in recognizing the position of a conjunct can change meaning. Exhibit 3 demonstrates this: flex-and expansion forgets a conjunct after flattening and turns a true formula into 1 = 1 ∧ 2 = 1, enabling contradiction (Section 7.3, pp. 20–21). Canonical forms therefore require tests against semantic equivalence, not only parser tests.
Inference: Verus code can use Rust newtypes for identifiers and spec fn normalizers with lemmas stating preservation of meaning. Verus can prove a normalization lemma for a defined formula datatype, but it cannot prove that an unverified parser produced the intended datatype without a parser contract.
technique 3: checker decomposition into pre-checker, equalizer, unifier, and schematizer
What it is. Mizar’s checker handles each atomic proof obligation through several specialized algorithms. Attribute inference rounds a type’s attribute set upward. The pre-checker negates the conjecture, normalizes assumptions, Skolemizes existentials, expands definitions, converts to disjunctive normal form, and tries to refute each clause. The equalizer builds equivalence classes of terms and performs numeric and polynomial evaluation. The unifier instantiates quantified assumptions, first individually and then in pairs. A separate schematizer resolves from justifications by assigning scheme variables to concrete functions and predicates (Section 3.2, pp. 9–10).
When to use it. Use this decomposition when a checker combines logical preprocessing, congruence closure, arithmetic normalization, and quantifier instantiation. Each component can then be tested on its own obligations and invariants.
How to do it. (1) Infer attributes and retain both user-provided and inferred clusters. (2) Add the negated goal to assumptions. (3) Normalize and Skolemize, then split into DNF clauses. (4) Build equalizer classes, add known equalities and definitions, and merge classes by numeric or polynomial equality. (5) Instantiate universal assumptions against metavariables and search for inconsistent assignments. (6) For schemes, match the explicitly supplied hypotheses and assign scheme variables. The paper summarizes the pre-checker as one that “takes the list of assumptions, together with the negated conjecture, and performs a number of normalizations on them, skolemizing existentials, removing vacuous quantifiers, and expanding some definitions.” (Section 3.2, p. 9).
Evidence. The checker verifies the full MML and supports arithmetic and polynomial proofs. The implementation’s checker is roughly one half to one third the size of the Pascal equivalent (Section 8, p. 23). Independent rewriting found four proofs of false, showing that decomposition also exposes soundness-critical boundaries (Section 7, p. 19).
Failure and assumptions. The unifier is explicitly incomplete: it gives up when simple and pairwise instantiation fail. Built-in requirements let the checker assume facts that are not represented as ordinary Mizar proofs. The paper notes that enabling a requirement can smuggle in unproved compatibility theorems, including the finite-range lemma needed for flex-and expansion (Section 3.3.1, pp. 11–12).
Inference: A Verus formalization would state each checker phase as a relation between formula sets and prove soundness lemmas from input relation to output relation. It should treat requirement files and solver calls as trusted assumptions until their justifications are encoded as Verus proofs.
technique 4: independent reimplementation and differential auditing
What it is. The author rewrote the soundness-critical behavior in Rust while aiming for semantic equivalence with the original, then ran the resulting checker over the MML. This provides external review through a different language, memory model, implementation structure, and debugging environment. The paper says: “One of the fortuitous side effects of going over each line of code and rewriting it to something morally equivalent in a different language is that one can find a lot of bugs.” (Section 7, p. 19).
When to use it. Use an independent implementation when the original verifier lacks a small kernel, a complete specification, or accessible source, and when a second implementation can process the same corpus.
How to do it. (1) Enumerate externally visible pipeline behavior and intermediate formats. (2) Implement equivalent stages with stronger type distinctions and memory safety. (3) Run both implementations on the same MML and compare acceptance, diagnostics, and timings. (4) Minimize every disagreement to a small proof. (5) Report the proof and patch the original or corpus. (6) Keep the independent implementation close enough to serve as a drop-in replacement while separately planning proof export.
Evidence. The checker found four exploitable soundness bugs and one non-critical defect affecting 46 articles; Mizar developers fixed the four soundness bugs and patched the MML in version 8.1.14 (Section 7, p. 19; Section 7.5, p. 22). The Rust checker completed the MML in 167.58 CPU minutes across all passes versus 798.38 CPU minutes for PC Mizar, a 4.76× ratio; checker-only was 142.75 versus 698.58 minutes, 4.89× (Table 2, p. 24). The table’s denominator is CPU minutes on the stated 12-core Intel i7-1255U testbed, with the parallelism column reporting CPU-time/real-time ratio.
Failure and assumptions. Differential agreement is not proof of correctness if both implementations share a design error or if the corpus omits adversarial cases. A close rewrite can also preserve algorithmic unsoundness, as Exhibit 4 did. The paper says this goal “does not seem like much of an improvement” for trusted-kernel size until proof export is achieved (Section 9, p. 24).
Inference: For VeruLaw, an independently implemented checker or symbolic tester is valuable as a bug-finding oracle for generated proofs, but it should not replace Verus’s proof obligations. Differential tests should include minimized counterexamples and malformed artifacts, with all acceptance paths tied to explicit contracts.
technique 5: root-causing soundness bugs with minimal proofs
What it is. The paper reduces checker defects to short Mizar articles that prove false statements, then traces each failure to a concrete implementation or algorithm issue. The four main exhibits are polynomial arithmetic overflow, negation loss in the schematizer, malformed flex-and unfolding, and unsound flex-and substitution.
When to use it. Use minimized false proofs to audit a proof checker: they expose a complete acceptance path and make the unsound assumption or transformation easy to inspect.
How to do it. (1) Start from a mismatch or suspicious accepted theorem. (2) Remove imports and proof steps until the smallest contradiction remains. (3) Identify the exact checker phase that accepts it. (4) Compare the intended formula with the internal representation. (5) Patch the implementation or corpus and rerun the minimized proof plus the full library.
Evidence and failure modes. In Exhibit 1, signed 32-bit polynomial exponents overflow after repeated squaring, allowing a contradiction; the paper explains that exponents wrap and that the checker’“’s nonzero-monomial invariant masks x^0 = 1 (Section 7.1, pp. 19–20). Exhibit 2 lets the schematizer match P to R while ignoring negation, proving 1 ≠ 1 from 1 = 1 (Section 7.2, p. 20). Exhibit 3 loses a conjunct during flex-and flattening (Section 7.3, pp. 20–21). Exhibit 4 compares only flex-and endpoints, so substitution changes the internal formula while endpoint equality remains; the defect survived translation to Rust and required repairing MML proofs (Section 7.4, pp. 21–22). Exhibit 5 shows an absent requirement represented by index zero being treated as a real attribute, affecting 46 articles (Section 7.5, pp. 22–23).
Inference: In Verus, each minimized contradiction can become a regression lemma: a verified checker must prove that accepted proof objects imply the target proposition, and each former exploit should become an input rejected by the parser or checker. This is a recommended testing strategy inferred from the paper, not a Verus technique demonstrated there.
what is proved, measured, and trusted
The paper measures implementation size, full-MML processing time, parallelism, and corpus acceptance. It demonstrates concrete false proofs accepted by the old checker and fixed in later versions. It does not provide a formal soundness proof of mizar-rs, the Rust compiler, the parser, intermediate-file formats, requirement files, or the MML assumptions. The paper explicitly distinguishes its implementation from a small trusted kernel and says proof export remains future work. Its performance numbers are specific to the stated corpus and hardware: Figure 2 reports an average 4.93× speedup over the verifier, and Table 2 reports exact CPU-minute ratios.
Inference: A product that generates agent-written verified Rust faces a threat from checker or translation defects analogous to Mizar’s: a verifier can accept a false proof if preprocessing, elaboration, requirements, or the final checker disagree. Independent reimplementation, typed intermediate artifacts, minimized contradiction tests, and eventual proof export reduce this threat. They do not establish correctness of generated specifications or external libraries.
mizar lessons for a verified Rust checker
The Mizar-specific artifacts worth carrying into VL are typed intermediate proof data, explicit checker phases, differential acceptance tests, and minimized false-proof regressions. Rebuilding mizar-rs itself would duplicate this paper’s completed checker; VL should apply its audit pattern to generated Rust contracts, macro expansion, solver facts, and FFI models.
techniques for the catalog
- staged proof pipeline — separate parsing, elaboration, requirement aggregation, and checking behind explicit intermediate artifacts
- typed verifier indices — wrap semantically distinct identifiers in types so references cannot be mixed accidentally
- checker phase decomposition — normalize, refute, equalize, instantiate, and schematize in separately auditable components
- independent reimplementation — rewrite a soundness-critical verifier and compare it on the same proof corpus
- minimized contradiction audits — reduce accepted false proofs to small regressions that identify the faulty transformation or assumption
Last edited: