VeriClust: verifiable multi-agent reasoning with formal cross-checking

Key points

• Independent Proposers generate candidate solutions.
• Verifiers check them with formal tools: model checking, SMT solving and proof assistants.
• An Arbiter combines verdicts with a reputation-weighted threshold vote.
• An Auditor keeps a tamper-evident log and issues a proof certificate for each accepted result.
• The paper gives conditions under which the weighted vote cannot accept an invalid proposal and does accept a valid one, and sets out an experimental design on mathematical reasoning, software verification and fact-checking benchmarks.

Limitations

Abstract

Language-model agents are being used for tasks where a wrong answer is costly, yet their outputs are probabilistic and their reasoning is hard to audit. Other language models are often used to check their work, which makes the check as fallible as the thing it checks. We propose VeriClust, a multi-agent architecture in which independent Proposers generate candidate solutions, Verifiers check them with formal tools (model checking, SMT solving and proof assistants), an Arbiter combines the verdicts with a reputation-weighted threshold vote, and an Auditor keeps a tamper-evident log and issues a proof certificate for each accepted result. We state the protocol, give conditions under which a weighted vote cannot accept an invalid proposal and does accept a valid one, and set out an experimental design on mathematical reasoning, software verification and fact-checking benchmarks. This paper is a research proposal. We have not built the system or run any experiment, and it reports no empirical results. The experimental section describes what we plan to measure, and states no expected effect sizes.

Related research

• Agent Coupling Protocol: ACP is a ten-stage protocol that weighs provider reliability more heavily as an orchestrator’s context fills. In simulation, honest providers earn 4.8 to 7.6 times more than malicious ones.
• PrincipalBench v2: PrincipalBench v2 audits the v1 orchestrator benchmark, withdraws its model rankings, and replaces it with a sealed two-phase protocol with clean controls and chance-corrected detection.
• Inventing the Variable: The HiddenLaw benchmark tests whether AI can introduce a variable its vocabulary lacks. Passive data blocks every learner; with interventions, Claude Opus 5.5 succeeds in 9 of 9 worlds.

Cite this paper

@misc{chowdhury2026vericlust,
  title     = {{VeriClust: A multi-agent system for verifiable reasoning through formal cross-checking and consensus}},
  author    = {Chowdhury, Sayan},
  year      = {2026},
  publisher = {Zenodo},
  note      = {Preprint, Kalaris Labs},
  doi       = {10.5281/zenodo.24121359},
  url       = {https://doi.org/10.5281/zenodo.24121359}
}