VENTURE SYNAPTIC
ENES

PUBLIC RESEARCH INDEX

Research, Preprints & Reproducible Artifacts

Central index of publicly verifiable manuscripts, Zenodo DOIs, experiment protocols, and open-source artifact repositories from Venture Synaptic Labs.

METHODOLOGICAL NOTE:Transparency standard: Every manuscript listed on this page is clearly identified by its actual review state. At present, our Zenodo publications are archived draft manuscripts and reproducible artifact packages (not peer reviewed, not submitted to an academic journal).

Repository provenance: Active exploratory work takes place in venture-synaptic/efch-research (currently private). When an experimental study reaches a frozen milestone, an unmodified snapshot with SHA-256 digests and raw evaluation logs is exported to a dedicated public repository and archived on Zenodo.

RESEARCH CATALOG BY INVESTIGATION LINE

Preprints paired with their reproducible artifacts

Instead of listing four disconnected entries, Venture Synaptic Labs groups each research study so readers can inspect the preprint manuscript alongside the exact code, raw logs, and SHA-256 digests that back it.

Publication structure (dated 2026-11-02): 2 Public Draft Preprints + 2 Published Software/Data Artifact Packages. Negative and mixed experimental results are reported with the same visibility as positive findings.
[INVESTIGATION P1 · EXP-019]Experiment EXP-019 · 2026-11-02

Semantic Evidence Persistence, Full Reverification, and Strengthened Memoization

Erik Fisher Cueva Huari (VentureSynaptic Labs)ORCID: 0000-0001-7268-5510
Preprint P1 · Research ManuscriptPublic Draft (Not peer reviewed)

“Safe Reuse Is Not Enough: A Controlled Comparison of Semantic Evidence Persistence, Full Reverification, and Strengthened Memoization”

Draft manuscript (2026-11-01 / 2026-11-02) · 2026-11-02

Pre-specified and internally audited controlled experiment on a bounded bit-vector domain comparing three conditions across 64 software revision transitions (576 target obligations): full reverification (Condition A), strengthened SMT-query memoization (Condition B), and a semantic evidence store (Condition C).

I. Supported within scope

  • Condition C required 252 solver invocations vs. 576 for full reverification (56.25% reduction).
  • All 8 adversarial soundness controls passed for Condition C with zero confirmed invalid evidence reuse across all 576 decided obligations.
  • Outperformed strengthened memoization (Condition B) in the equivalent-change stratum (32 vs. 40 invocations).

II. Negative & mixed findings

  • Negative efficiency result vs. strong baseline: Condition C required 2.625× as many invocations (252) as strengthened SMT-query memoization (Condition B, 96 invocations) overall.
  • An exploratory hybrid follow-up (P0/P1) reduced some solver calls but increased wall-clock cost and exposed integrity defects D10–D13 and architectural limitation L-D14.

Preprint access: The standalone Preprint P1 upload in Zenodo is in draft state; the full compiled PDF (paper/main.pdf) and LaTeX source (paper/main.tex) are publicly available in the repository below and bundled inside Zenodo record v1.1-exp019 (10.5281/zenodo.23874125).

Manuscript PDF (paper/main.pdf)LaTeX (paper/main.tex)
Artifacts P1 · Software & DataPublished on Zenodo & GitHub

EFCH P1 Artifacts — Safe Reuse Is Not Enough (EXP-019)

Unmodified export from venture-synaptic/efch-research containing frozen protocol manifest (tag exp019-protocolo), instrument code (tag exp019-instrumento), raw evaluation logs (data/exp019-resultados.tar.gz), and internal audit trail.

Concept DOI (Zenodo):10.5281/zenodo.23873678 ↗
v1.1-exp019 (2026-11-02 · Latest)10.5281/zenodo.23874125 ↗

Includes updated manuscript draft PDF/LaTeX, frozen protocol, and raw evaluation archive (31.8 MB).

v1.0-exp019 (2026-11-02 · Initial)10.5281/zenodo.23873679 ↗

Initial published artifact release with deterministic evaluation tarball and SHA256SUMS.

SHA-256 verification & reproduction protocol:

$ sha256sum -c SHA256SUMS
$ sha256sum -c experimentos/exp019/MANIFIESTO.sha256
$ mkdir -p datos && tar -xzf data/exp019-resultados.tar.gz -C datos
$ scripts/vendor_z3.sh && python3 experimentos/exp019/ejecutar.py --preparacion
GitHub: venture-synaptic/efch-artifacts-p1-evidence-persistence
[INVESTIGATION P2 · EXP-004 TO EXP-015]Experiments EXP-004, EXP-005, EXP-007, EXP-008, EXP-009, EXP-010, and EXP-015 · 2026-11-02

Verified Binary Decoding with EFCH Lang against C, Rust-Kani, and Dafny

Erik Fisher Cueva Huari (VentureSynaptic Labs)ORCID: 0000-0001-7268-5510
Preprint P2 · Research ManuscriptPublic Draft (Not peer reviewed)

“Verified Binary Decoding with a Domain-Specific Language: An Empirical Study of EFCH Lang against C, Rust-Kani, and Dafny”

Draft manuscript v0.2 (2026-11-02) · 2026-11-02

Empirical evaluation of EFCH Lang 0.1 — a narrow domain-specific language translating bounded binary-processing programs into C and checking equivalence against functional specifications in Z3 — compared against handwritten C, Rust with Kani, Go, and Dafny.

I. Supported within scope

  • EXP-005 (8-function benchmark): all 8 bounded binary functions verified under protocol; generated C achieved a 0.90 geometric mean runtime ratio vs. handwritten C.
  • EXP-015 & EXP-004: IPv4 options and unsigned varint decoders passed all differential tests and bounded proofs with runtime ratios of 1.027 and 0.966 vs. C (re-executed Nov 2, 2026 at 1.030 and 0.965).

II. Negative & mixed findings

  • Adversarial review of EXP-005 showed specification-effort comparisons against Rust-Kani and Dafny were representation-sensitive; a specification-only Dafny baseline erased the purported effort advantage.
  • EXP-007 & EXP-008 (Negative): DNS hostname decoder written as a state machine timed out at 900 s in SMT and ran 5.6× slower than handwritten C.
  • EXP-009 & EXP-010 (Mixed): Adding bounded fold made DNS verifiable in 16.9 s (1.02× C runtime), but Dafny verified it in 2.95 s with fewer lines; TCP options parser passed registered criteria only on verification time.

Preprint access: The standalone Preprint P2 upload in Zenodo is in draft state; the full compiled PDF (paper/main.pdf) and LaTeX source (paper/main.tex) are publicly available in the repository below and bundled inside Zenodo record v1.0-lang (10.5281/zenodo.23874420).

Manuscript PDF (paper/main.pdf)LaTeX (paper/main.tex)
Artifacts P2 · Software & DataPublished on Zenodo & GitHub

EFCH P2 Artifacts — Verified Binary Decoding with EFCH Lang (EXP-004 to EXP-015)

Contains preregistered protocols and recorded results for EXP-004, EXP-005, EXP-007, EXP-008, EXP-009, EXP-010, and EXP-015, 178 unit tests, and Nov 2, 2026 re-execution archive.

Concept DOI (Zenodo):10.5281/zenodo.23874419 ↗
v1.0-lang (2026-11-02 · Latest)10.5281/zenodo.23874420 ↗

Published 68.5 MB archive with EFCH Lang 0.1 code, comparator corpus (C, Rust-Kani, Go, Dafny), negative experiments, Nov 2 re-execution, and manuscript v0.2.

SHA-256 verification & reproduction protocol:

$ sha256sum -c SHA256SUMS
$ tar -xzf data/efch-lang-resultados.tar.gz
$ scripts/vendor_z3.sh && python3 -m unittest discover -s tests
$ python3 experimentos/lang01.py --salida /tmp/exp004
GitHub: venture-synaptic/efch-artifacts-p2-lang-binary-decoding

SCIENTIFIC TRACEABILITY ARCHITECTURE

How we integrate Zenodo, GitHub, ORCID, and Venture Synaptic Labs

Each platform fulfills a distinct, verifiable role so external researchers can move seamlessly from a manuscript claim to its raw experimental logs and reproduction scripts.

01 / ZenodoArchive & DOI

Primary archival registry providing immutable versioned DOIs, timestamps, and downloadable artifact snapshots.

Archival on Zenodo guarantees permanence and version traceability; it does not imply journal peer review.

Zenodo Record 23873679
02 / GitHubCode & Versions

Technical source hosting experiment protocols, comparator suites, SHA-256 manifests, and manuscript LaTeX/PDF sources.

Active exploration occurs in venture-synaptic/efch-research; frozen milestone exports are published in dedicated artifact repositories.

venture-synaptic/efch-research
03 / ORCIDAuthor Identity

Persistent researcher identifier (Erik Fisher Cueva Huari · 0000-0001-7268-5510) linking authorship across preprints and DOIs.

ORCID verifies persistent author attribution and metadata linkage, not external certification of scientific quality.

ORCID 0000-0001-7268-5510
04 / Venture Synaptic LabsPublic Catalog

Institutional portal organizing research by investigation line, pairing every preprint with its reproducible artifacts and negative findings.

Separates hypotheses, bounded empirical results, and open limitations from commercial products.

@venture-synaptic Catalog
Verified institutional baseline records
EFCH Research Repository (venture-synaptic/efch-research)

Primary research repository (currently private; frozen unmodified exports are publicly auditable in the P1 and P2 artifact repositories).

Academic Author Identity (ORCID: 0000-0001-7268-5510)

Erik Fisher Cueva Huari — VentureSynaptic Labs author profile.

Zenodo Reference Record (10.5281/zenodo.23873679)

Published P1 artifact archive (v1.0-exp019; updated in v1.1-exp019 at 10.5281/zenodo.23874125).

EXPERIMENTAL LEDGER // PROTOCOLS & OUTCOMES

Publicly audited experiments & results

Negative, inconclusive, and refuted experiments are published with the same visibility as supported results.

EXP-019
[SUP]Supported within scope

EXP-019 — Semantic Evidence Persistence vs. Full Reverification & Strengthened Memoization

Demonstrates controlled trade-offs between reuse and sound invalidation within the tested corpus; documented in the draft manuscript 'Safe Reuse Is Not Enough'.

Limits: Integrity defects D10–D13 and architectural limitation L-D14 remain open; internal audit was conducted by an AI agent (Codex) rather than an independent external human lab.

EXP-004 / EXP-015
[SUP]Supported within scope

EXP-004 & EXP-015 — Bounded Binary Decoding & Equivalence Verification in EFCH Lang

Both programs proved equivalent in SMT, passed all differential vectors, and reproduced M9 runtime ratios (1.030 and 0.965 vs 1.027 and 0.966 in archived runs).

Limits: Restricted to small loop-free / bounded-input domains (bytes <= 64); the C code generator itself is tested differentially, not formally verified.

EXP-005 / EXP-010
[INC]Inconclusive (Domain-dependent trade-offs)

EXP-005 & EXP-010 — Multi-Language Comparator Study (C, Rust-Kani, Go, Dafny)

Shows domain-specific ergonomics for bounded packet decoding, alongside clear expressiveness boundaries compared to general-purpose verification systems like Dafny and Kani.

Limits: Code snapshot in the P2 package reflects Nov 1, 2026 state rather than exact Oct 21–24 commit hashes for 8 evolved core files; documented transparently in repository provenance.

EXP-007 / EXP-008 / EXP-009
[REF]Refuted / Negative results preserved

EXP-007, EXP-008 & EXP-009 — Negative & Boundary Evaluations in EFCH Lang

Archived in full inside the P2 artifact repository to document where current domain restrictions, solver timeouts, or abstraction overhead prevent success.

Limits: Highlights structural limits of loop-free bounded slices when facing variable-length pointer compression and richer stateful protocols.

EXP-001 / EXP-002 (Gate G4)
[REF]Refuted (Gate G4 not passed)

EXP-001 & EXP-002 — Performance Optimization vs. Standard Compiler Baselines (Gate G4)

No performance advantage demonstrated over gcc -O2 baselines; Gate G4 ('Structural research advantage') is explicitly recorded as not passed in EFCH v0.1.

Limits: Single-machine timing; complex bit-vector equivalences (such as two 64-bit adder trees) can also hit SMT 'unknown' timeouts.

RFC-LIVE-0.1
[PRP]Proposed (RFC / Design stage)

EFCH Live Engineering & Contract Conformance Pack 0.1

Recommends reformulating scope before authorizing P0 implementation; schema trace checks do not certify authentication, atomicity, or semantic correctness.

Limits: Documentary and synthetic schema stage only; no empirical hypothesis validated.