đ€ Vero and VL: repository-level verified-code evaluation
This note studies âVero: Can AI Agents Build Formally Verified Software Repositories?â as part of the AutoVerus citation watch. The paper is an arXiv v1 preprint dated 2026-08-13 in the saved evidence set. The official artifact is the public sunblaze-ucb/vero repository. Sources: VERO-status, VERO-artifact.
bottom line
Vero is more important as an evaluation threat than as a direct tool threat. It is not another AutoVerus-like Verus proof generator. It is a Lean 4 benchmark for testing whether coding agents can complete curated multi-module verified-code instances: implementations plus proofs against manually curated specifications. Sources: VERO-scope, VERO-inputs, AUTO-scope.
The practical lesson for VL is clear. Per-obligation pass rate is not enough. The authors report that Veroâs strongest configuration passes 87.3 percent of specifications in code-and-proof mode, but fully solves only 27 of 43 curated Lean instances. That supports a VL scoring rule we should keep enforcing: a target is not done until the whole checked artifact builds and every required obligation passes. Sources: VERO-results, VERO-full-coverage, VL-evaluation.
The main caveat is the same one the human has been worried about. Vero can machine-check that code satisfies formal Lean specifications. It cannot prove that those specifications are complete or match human intent. The paper explicitly says the audit mechanism âcannot ensure that specifications are semantically correct or complete.â Human review remains part of the benchmark construction. Sources: VERO-limitations, VERO-curation.
This study integrity-checked the saved PDF, metadata, and artifact archive. It did not rerun the Vero benchmark or reproduce the reported scores. Source: VERO-artifact.
threat assessment
capability threat: medium
The authors report that frontier coding agents can complete nontrivial curated Lean verification instances. The strongest reported setup fully solves 27 of 43 code-and-proof instances and 25 of 43 proof-only instances. Sources: VERO-results, VERO-models.
The comparison to VL should be read as a documentation-bound comparison, not a matched experiment. Current local VL docs describe focused Verus proof work and a harness for repository-level pilots, but they do not document comparable public full-repository outcomes and say VL âdoes not yet establish autonomous repository-wide specification discovery.â Sources: VL-harness, VL-boundary.
The threat is bounded because Vero is not a production Verus/Rust system. It is a Lean 4 benchmark. It includes Verus-derived tasks, but those are translated into Lean and evaluated there.
novelty threat: medium to high
The paperâs strongest novelty claim is benchmark design: repository-level joint implementation and proof synthesis, with both code-and-proof and proof-only modes. This is a cleaner evaluation target than single-function proof generation and closer to what VL wants to measure. Sources: VERO-scope, VERO-modes, AUTO-scope.
Against AutoVerus, the scope is different. AutoVerus starts from Rust code and its specifications and generates Verus proofs for single-function tasks. Vero starts from curated Lean repositories and asks an agent either to prove a reference implementation or to write implementations and prove all specifications.
evaluation threat: high
Vero describes several evaluation practices VL should copy or adapt. Sources: VERO-full-coverage, VERO-anticheat, VERO-audit.
First, it uses full-repository completion, not just partial specification coverage.
Second, the grader does not trust the agentâs edited project. It extracts only allowed marker-slot bodies into a fresh benchmark copy, then builds and checks proof axioms.
Third, it treats benchmark defects as a separate class. Agents can submit machine-checked evidence that a specification is unsatisfiable, a reference implementation is wrong, or specifications conflict. The authors then adjudicate those closures by hand.
Fourth, the paper analyzes why agents fail. The key reported bottleneck is not local proof skill. It is failure to discover shared invariants, organize reusable lemma libraries, and keep the repository buildable.
practical competitive threat: low to medium
Vero is a public benchmark and artifact, but it is not a turnkey competitor for verified Rust work. It does not produce Verus proofs for real Rust repositories. It gives competitors a public measuring stick for repository-level verified-code agents. Sources: VERO-scope, VERO-artifact, AUTO-scope.
The practical danger is that future papers can use Vero-style evaluation to make stronger claims than VL if VL keeps relying on ad hoc evidence. Sources: VERO-results, VERO-lemma-library, VL-boundary.
what Vero actually evaluates
A Vero instance is a curated multi-module Lean 4 project, not an entire upstream Rust, Python, Dafny, Verus, or Coq repository. The curator provides fixed data types and helpers, API signatures, formal specifications, and reference implementations. The agent fills allowed slots. Sources: VERO-scope, VERO-inputs.
There are two task modes.
In proof-only mode, the reference implementation is fixed. The agent must prove every specification against it. Source: VERO-modes.
In code-and-proof mode, the agent writes each API implementation and proves every specification against the implementation it wrote. Source: VERO-modes.
The key scoring rule is all-or-nothing at the repository level. Vero counts an instance as solved only if all required specifications pass. The paper argues this is necessary because easy specifications can inflate partial coverage. Source: VERO-full-coverage.
what the results mean
The authors report that the strongest configuration is Codex version 0.140.0 with GPT-5.5 at xhigh reasoning effort. It solves 27 of 43 instances in code-and-proof mode and 25 of 43 in proof-only mode. Ten instances resist every tested configuration across both modes. Sources: VERO-models, VERO-results.
This creates a useful distinction. The best agent passes more than 80 percent of individual specifications, but it still misses many full repositories. Vero therefore supports measuring completion at the artifact level, not only at the theorem level.
The paperâs reported failure analysis matters for VL. Completed instances rely on shared lemma libraries. Across full solves, agent-written helper theorems contain a median of 73.6 percent of proof lines in code-and-proof mode. Most full solves share helpers across multiple specifications. Source: VERO-lemma-library.
This suggests that VL should not only ask whether an agent can close one Verus proof. It should measure whether the agent can discover and maintain reusable invariants across a target.
implementation freedom is double-edged
Veroâs code-and-proof mode allows the agent to choose its own implementation. Sometimes that helps. The paper reports five instance-agent pairs where the agent replaced a hard-to-prove reference algorithm with a simpler implementation satisfying the same specifications. Source: VERO-implementation-freedom.
The paper is careful about the tradeoff: the simpler implementation can be behaviorally correct with respect to the given specification while giving up efficiency. That is directly relevant to VL. If the benchmark allows implementation rewrites, the score must say whether performance, complexity, or production intent is part of the specification. Otherwise, the agent may win the proof while losing an unstated engineering requirement.
evaluation reliability
Veroâs anti-cheat design is useful because the core oracle is Lean plus additional checks, not agent self-report. Source: VERO-anticheat.
The grader extracts only allowed slot contents and inserts them into a fresh source benchmark. It rejects untrusted axioms and sorry dependencies. It also screens for declarations that can decouple logical semantics from executable behavior.
The weakest part is that one anti-cheat layer includes an LLM judge for suspicious typeclass-instance patterns. That is narrower than using an LLM as the main correctness judge. Still, VL should prefer deterministic checks wherever possible and isolate any LLM judgment as advisory, reviewable, and non-final.
specification-intent gap
Vero does not solve the specification completeness problem.
For formally sourced benchmarks, Vero translates Dafny, Verus, and Coq projects into Lean and cross-checks against source-language formalizations. For Python-sourced benchmarks, it writes specifications from documentation and tests, then manually reviews them. Sources: VERO-curation, VERO-limitations.
That is useful curation, not proof of intent. The paperâs own limitation is explicit: the audit mechanism certifies formal satisfiability but cannot ensure semantic correctness or completeness.
For VL, this means benchmark quality needs a separate semantic evidence layer: source intent, existing tests, documentation, human review, mutation or counterexample checks, and explicit non-goals. The verifier only answers whether the implementation satisfies the formal specification it was given.
comparison with AutoVerus
AutoVerus is closer to VLâs Verus/Rust technology stack. It takes Rust code with specifications and generates proofs in Verus. Its unit is a single Rust function. Sources: AUTO-scope, AUTO-method.
Vero is closer to VLâs desired evaluation scale. It asks for repository-level consistency, shared helper lemmas, and all-obligation completion.
The two papers are therefore complementary. AutoVerus is stronger evidence for Verus proof-generation mechanics. Vero is stronger evidence for how to evaluate repository-level verified-code agents.
comparison with current VL evidence
Current local VL documentation says there is a harness for repository-level Verus proof-synthesis pilots. This note treats that as dated project documentation, not as an independently reproduced benchmark result. Source: VL-harness.
The same local capability summary says current evidence supports focused proof work and named-target specification work, but not autonomous repository-wide specification discovery. That is still the right boundary after reading Vero. Source: VL-boundary.
VLâs current evaluation standard already points in the right direction: paired controlled experiment, arm-blinded scoring, and effect sizes with uncertainty intervals. Vero adds concrete benchmark mechanics that would make such an evaluation harder to fool.
actionable VL lessons
Use full-target success as the headline metric. Partial theorem coverage should be secondary because it can hide the hardest obligations.
Separate proof-only from code-and-proof. Proof-only measures proof skill against a fixed implementation. Code-and-proof measures the agentâs ability to choose proof-friendly implementations, but it also risks losing unstated production properties.
Re-render the scored artifact from clean sources. Do not grade an agentâs own project directory as the source of truth.
Check proof dependencies, not only build success. A build can hide unacceptable axioms or shortcuts.
Add a benchmark-defect channel. If an agent believes the target spec is impossible or the reference is wrong, require machine-checkable evidence and human adjudication.
Measure reusable invariant construction. A VL benchmark should ask whether the agent creates shared lemmas that multiple obligations depend on, not just whether it closes isolated goals.
Keep semantic specification review separate from machine verification. The verifier checks code against the formal spec. It does not check that the spec captures the humanâs intent.
source map
Vero primary sources
VERO-status: arXiv metadata XML and official CFF file. Claim: Vero is an arXiv v1 preprint in the saved evidence set. Quote: âhttp://arxiv.org/abs/2608.13522v1â. Quote: â2026-08-13T17:41:27Zâ. Quote: â10.48550/arXiv.2608.13522â. Uncertainty: no proceedings, publisher venue, or acceptance record was found.
VERO-scope: Vero paper. Claim: benchmark scope is repository-level joint implementation and proof synthesis over curated Lean instances. Quote: âfirst benchmark to evaluate joint implementation and proof synthesis at the repository levelâ. Quote: â43 multi-module instances sourced from real-world repositoriesâ. Boundary: these are not full arbitrary upstream projects.
VERO-inputs: Vero paper. Claim: each instance has fixed scaffold, APIs, specs, and reference implementations. Quote: âpredetermined API interfaces, manually curated formal specifications, and reference implementationsâ. Quote: âdata type and helper definitions, API signatures, and formal specificationsâ.
VERO-modes: Vero paper. Claim: the benchmark has proof-only and code-and-proof modes. Quote: âprove every specification against the reference implementationâ. Quote: âboth implement every API and prove every specificationâ.
VERO-full-coverage: Vero paper. Claim: full coverage is the main score. Quote: âFull coverage is necessaryâ. Quote: âpartial coverage can be inflated by easy onesâ.
VERO-anticheat: Vero paper. Claim: grading uses fresh source re-rendering, axiom checks, and declaration screening. Quote: âfresh copy of the source benchmarkâ. Quote: âaxiom allowlist rejects proofsâ. Quote: ârule-based detector and an LLM judgeâ.
VERO-curation: Vero paper. Claim: curation is LLM-assisted and human-reviewed. Quote: âEach stage runs as an LLM agentâ. Quote: âreviewed by a human curatorâ.
VERO-contamination: Vero paper and official README. Claim: the authors argue that novel Lean translations reduce ground-truth leakage. Quote: âno Lean 4 ground-truth proofâ. Quote: âno Lean 4 ground-truth solution exists onlineâ. Uncertainty: this does not prove absence of source-language leakage.
VERO-results: Vero paper. Claim: current frontier agents are incomplete at repository level. Quote: âfully solves 27 of 43 instancesâ. Quote: â10 instances resist all eight configurationsâ. Quote: âpasses 87.3% of specificationsâ.
VERO-models: Vero paper. Claim: evaluated harnesses are Codex and Claude Code with Lean access. Quote: âCodex (v0.140.0)â. Quote: âGPT-5.5 profilesâ. Quote: âClaude Code (v2.1.191)â. Quote: âLean v4.29.1â.
VERO-lemma-library: Vero paper. Claim: full solves depend on shared lemma libraries. Quote: âshared lemma librariesâ. Quote: âmedian of 73.6% of proof linesâ. Quote: â80 of the 82 solves share a helperâ.
VERO-implementation-freedom: Vero paper. Claim: implementation freedom can trade efficiency for provability. Quote: âsimpler implementation of its ownâ. Quote: âwhat it gives up is efficiencyâ.
VERO-audit: Vero paper. Claim: the audit mechanism found and repaired benchmark defects. Quote: â38 adjudicated specification defectsâ. Quote: âAll of them are repairedâ. Quote: âadjudicating every closure by handâ.
VERO-auditor-overlap: Vero paper. Claim: a second auditor gives modest extra value. Quote: âA second auditor adds littleâ. Quote: â5 additional casesâ.
VERO-limitations: Vero paper. Claim: Vero is Lean-only and does not solve semantic completeness. Quote: âcurrently targets Lean 4 onlyâ. Quote: âcannot ensure that specifications are semantically correct or completeâ.
VERO-artifact: official GitHub metadata and README. Claim: the artifact is public, Vero-owned code and scaffolding are Apache-2.0, and the artifact exposes benchmark inventory. Quote: âhttps://github.com/sunblaze-ucb/veroâ. Quote: âApache License 2.0â. Quote: âThree active benchmarks derive from copyleft upstreamsâ. Quote: â43 benchmark instances, 743 APIs, 2,705 scored specsâ.
AutoVerus baseline
AUTO-status: preserved AutoVerus PDF and Markdown extract. PDF SHA-256: 6c750ff7c3f0de09be7685fa797ee338d669778bc38adbd44230e9668582c5fc. Markdown extract SHA-256: 17a397c18e7f148a1a82d7b2d03856547568e2dc2f3808757af8c67ec4bbf514. Claim: AutoVerus is a PACM PL/OOPSLA 2025 publication. Quote: âProc. ACM Program. Lang.â Quote: âOOPSLA2â.
AUTO-scope: preserved AutoVerus Markdown extract. Claim: AutoVerus starts from Rust code and specifications, with a single-function task unit. Quote: âprovided with Rust code and its specificationsâ. Quote: âa single Rust function is the unitâ.
AUTO-method: preserved AutoVerus Markdown extract. Claim: AutoVerus uses proof construction and verifier-guided debugging. Quote: âthree phases of proof constructionâ. Quote: âdebugging guided by verification errorsâ.
frozen VL evidence
VL-harness: /ssd1/sichangheagent/VeruLaw/README.md. SHA-256: fe8f3f065390dbc9637e5f73a5657734d2c37f1b52d632460b10bd256f0dd069. Classification: dated local project documentation, not an independently reproduced result. Quote: âharness for repository-level Verus proof-synthesis pilotsâ.
VL-boundary: /ssd1/sichangheagent/VeruLaw/docs/current_capability_summary.md. SHA-256: 1c1c0bacde17e3d011050ebd739e9ed2aa92d715d75c4ba7d8eaf75d7ccd776c. Classification: dated local project documentation; the working tree was not treated as a clean published artifact. Quote: âuseful evidence for focused proof workâ. Quote: âdoes not yet establish autonomous repository-wide specification discoveryâ.
VL-evaluation: /ssd1/sichangheagent/VeruLaw/docs/roadmap/guidance_evaluation_research_standard.md. SHA-256: b207cb6594607fbfb42bd59d6fcf01849213c43c67e123487318c0ef678a812d. Classification: dated local evaluation-design documentation, not completed evidence. Quote: âpaired controlled experimentâ. Quote: âarm-blinded scoringâ. Quote: âeffect sizes with uncertainty intervalsâ.
VL-operating: /ssd1/sichangheagent/VeruLaw/docs/experiments/operating_rules.md. SHA-256: b033f2488a5f817c519a2c99d62dbf5b2a1e1a8c3d9f84224d8f8670d3577d87. Classification: dated local evaluation policy documentation. Quote: âMissing evidence downgrades the claimâ.
artifact paths
Primary PDF: /hdd1/sichanghe/paper_collection/Vero- Can AI Agents Build Formally Verified Software Repositories, Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song, arXiv, 2026.pdf.
Collection directory: /hdd1/sichanghe/paper_collection/Vero- Can AI Agents Build Formally Verified Software Repositories, Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song, arXiv, 2026/.
Source map and audit: /hdd1/sichanghe/paper_collection/Vero- Can AI Agents Build Formally Verified Software Repositories, Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song, arXiv, 2026/source-map-and-artifact-audit-20260821.md.
follow-up: current VL documentation check
This follow-up was added after the human asked whether the earlier Vero suggestions still apply given what VL already does. I checked the current VL documentation and retained VL evidence again rather than relying only on the earlier Vero memo.
Several Vero suggestions are already covered by current VL standards. VL already requires clean worker-visible surfaces for realistic specification recovery: implementation code plus ordinary public docs, tests, examples, callers, and project structure, without target names, target counts, target manifests, stripped declarations, empty stubs, hidden oracle text, or target-shaped compiler or verifier errors. Sources: VL-current-boundary, VL-guidance-standard, VL-cli-plan, VL-operating-current.
VL documentation already requires paired no-helper versus helper comparisons on the same frozen snapshot, arm-blinded semantic and trajectory scoring, effect sizes with uncertainty intervals, proposal-freeze artifacts, transcript and command evidence, worker-visible and forbidden-material manifests, frozen guidance provenance, and guidance-corpus leakage controls. These are documented requirements for future evaluations, not evidence that a completed controlled study has already produced the corresponding outcome result. Sources: VL-guidance-standard, VL-cli-plan, VL-operating-current, VL-real-project-evidence.
VL already has stronger source and evidence discipline than the earlier memo implied. Reusable guidance must avoid hidden answers, benchmark answers, solved patches, private logs, raw transcripts, sibling-arm artifacts, evaluator reasoning, manager-only notes, and customer-private material. Experiment rules say missing evidence downgrades the claim and never implies success. Sources: VL-source-policy, VL-operating-current.
VL also has retained real-project evidence, but that evidence is bounded. The six-lane Midas Lex note says the strongest observed contribution was a TOML termination repair and that the more repeatable benefit was making requirement, proof, production-correspondence, and result-boundary claims explicit. It also says the evidence does not show reliable target selection, defect finding, semantic closure, or a controlled no-Midas comparison. Source: VL-real-project-evidence.
Therefore the earlier Vero suggestions need refinement, not wholesale adoption.
Already covered: preserve exact prompts, tool provenance, source hashes, transcripts, commands, and result boundaries; use controlled paired E0/E1 experiment designs; blind or adjudicate scoring; separate realistic specification recovery from exact-target diagnostics; police sibling-arm, guidance-corpus, hidden-answer, and evaluator-reasoning leakage.
Still applies: use full-target completion as a headline metric for proof and L4 tasks. VL records final verifier results and proof-handoff pass rates, but Veroâs stronger lesson is to predeclare the required obligation set and report full-scope completion first, with partial coverage secondary. Specification-recovery tasks still need recall, precision, and semantic adequacy rather than an all-obligation score. Sources: VERO-full-coverage, VL-guidance-standard, VL-cli-plan.
Still applies: add a stricter final artifact oracle. Vero grades by re-rendering a fresh benchmark copy, extracting only allowed marker-slot bodies, preserving immutable scorer and harness inputs, and checking for axioms or other proof-bypass mechanisms. VL should make the analogous final check explicit for each experiment family. The final score should come from a clean reconstructed artifact, not from the subjectâs edited working directory or self-report. Sources: VERO-anticheat, VL-operating-current, VL-cli-plan.
Still applies: separate proof diagnostics, realistic specification recovery, and L4 forward-experiment scores. VL already separates these modes conceptually, but headline evaluation should not blend them because implementation freedom can trade production properties for provability. Sources: VERO-modes, VERO-implementation-freedom, VL-cli-plan.
Still applies: create a formal benchmark-defect channel. If an agent claims the hidden reference, source contract, or scoring target is wrong, require machine-checkable or source-grounded evidence and independent human adjudication. VL has stop/report rules and reviewer evidence, but Veroâs explicit defect-audit lane is a stronger benchmark-maintenance mechanism. Sources: VERO-audit, VL-operating-current.
Still applies: measure reusable invariant construction. Current VL says broad invariant invention is not yet established. Veroâs results suggest full solves depend heavily on shared helper libraries, so VL should score whether agents discover and maintain shared lemmas or invariants across obligations, not only whether they close isolated targets. Sources: VERO-lemma-library, VL-current-boundary, VL-cli-plan.
Still applies: keep semantic-intent review separate from verifier success. VL already says verifier green cannot compensate for weak semantic contracts. Vero reinforces this: its audit cannot ensure specifications are semantically correct or complete. Sources: VERO-limitations, VL-current-boundary, VL-guidance-standard.
Still applies: add a separate benchmark-availability and model-contamination-risk audit. VL already controls sibling-arm and guidance leakage, but that is different from Veroâs claim that novel Lean translations reduce ground-truth availability. VL should disclose whether public source code, old proofs, local notes, or previous benchmark artifacts may have been visible to the model or guidance corpus. Sources: VERO-contamination, VL-source-policy, VL-guidance-standard.
The strongest next evaluation from the current VL state would start with a clean credible exploratory pilot: at least 30 privately scored useful-specification opportunities across at least three projects; at least two target families per project where possible; at least two model or seed repetitions for a smaller selected subset; audit all submitted proposals for unsupported, unnecessary, misplaced, or harmful specifications; paired E0 no-CLI and E1 Midas Lex arms on frozen snapshots; worker-visible and forbidden-material manifests; proposal freeze before verifier feedback; clean reconstructed-artifact grading; whole-submission semantic audit; explicit defect channel; and trajectory coding for where guidance changed, confirmed, or harmed decisions. This would turn the existing good process rules into stronger outcome evidence. A paper-level guidance-efficacy claim still needs the larger VL bar: 100 or more private opportunities across six or more projects, multiple task families, cross-project holdouts, and repeatability checks. Source: VL-guidance-standard.
follow-up source map
VL-current-boundary: /ssd1/sichangheagent/VeruLaw/docs/current_capability_summary.md. SHA-256: 1c1c0bacde17e3d011050ebd739e9ed2aa92d715d75c4ba7d8eaf75d7ccd776c. Classification: current local VL capability documentation. Quote: âuseful evidence for focused proof workâ. Quote: âdoes not yet establish autonomous repository-wide specification discoveryâ.
VL-operating-current: /ssd1/sichangheagent/VeruLaw/docs/experiments/operating_rules.md. SHA-256: b033f2488a5f817c519a2c99d62dbf5b2a1e1a8c3d9f84224d8f8670d3577d87. Classification: current local experiment policy. Quote: âworker-visible manifestâ. Quote: âforbidden-material manifestâ. Quote: âproposal-freeze artifactâ. Quote: âMissing evidence downgrades the claimâ.
VL-guidance-standard: /ssd1/sichangheagent/VeruLaw/docs/roadmap/guidance_evaluation_research_standard.md. SHA-256: b207cb6594607fbfb42bd59d6fcf01849213c43c67e123487318c0ef678a812d. Classification: current local evaluation standard. Quote: âpaired controlled experimentâ. Quote: âarm-blinded scoringâ. Quote: âeffect sizes with uncertainty intervalsâ. Quote: âfrozen guidance provenanceâ. Quote: âguidance-corpus leakage controlâ.
VL-cli-plan: /ssd1/sichangheagent/VeruLaw/docs/roadmap/cli_vs_no_cli_evaluation_plan.md. SHA-256: b37719bc5c5823e7d27ebfbb76fdbae46c363f026c8615b61dba3044232accfd. Classification: current local CLI comparison plan. Quote: âsame frozen snapshotâ. Quote: âproposal-freeze artifactâ. Quote: âworker-visible manifest and forbidden-material manifestâ.
VL-source-policy: /ssd1/sichangheagent/VeruLaw/docs/guidance/source_policy.md. SHA-256: 1ffa395a2fd7dfddbc77e511c6ac7ad79b47bf00cfc6f295669554fc82565196. Classification: current local reusable-guidance source policy. Quote: âReusable guidance must not use hidden answersâ. Quote: âsibling-arm artifactsâ. Quote: âevaluator reasoningâ.
VL-real-project-evidence: /ssd1/sichangheagent/VeruLaw/docs/midas-lex/real_project_usage_evidence_20260722.md. SHA-256: 88bd2268702d64af5e26cf49d6e1050f6cf1045ae4df4081ce89a60190eee211. Classification: retained local evidence note, not a controlled comparison. Quote: ârepeated guidance checklistâ. Quote: âdoes not show that Midas Lex reliably selected a targetâ. Quote: ânot a controlled comparisonâ.
Last edited: