01 / VENTURE SYNAPTIC LABS

Labs — Evidencia antes que afirmaciones

Labs investiga modelos computacionales, especificaciones formales y flujos de verificación mediante experimentos controlados y artefactos públicos auditables.

Secuencia Metodológica de Evaluación Científica

1. Pregunta

2. Hipótesis

3. Método

4. Evidencia

5. Límites

6. Siguientes pasos

§ 01 — PROGRAMA DE INVESTIGACIÓN DESTACADO[INV]Prototipo 0.1.0a1 · En investigación

EFCH — Computación Orientada a Propiedades (Prototipo 0.1.0a1)

“EFCH explora si los sistemas de software pueden construirse a partir de propiedades y restricciones explícitas, organizando la síntesis, la verificación y la ejecución en torno a dichas especificaciones.”

[AVISO DE ALCANCE CIENTÍFICO]

Aclaración metodológica fundamental: La viabilidad general y la superioridad de EFCH frente a los paradigmas o lenguajes existentes no están demostradas. Los resultados obtenidos en experimentos acotados (como funciones sin bucles sobre vectores de bits o decodificadores de paquetes con límite fijo) no se extrapolan a todas las aplicaciones de software.

Leer ficha completa de investigación EFCH

§ 02 — Campos investigados

01Especificación orientada a propiedades

Especificación formal

Definición de computaciones mediante semántica matemática explícita, restricciones de dominio, precondiciones y presupuestos de ejecución (.efch).

02Síntesis de programas bajo restricciones

Generación de candidatas

Evaluación de implementaciones candidatas propuestas por personas, búsqueda enumerativa (SyGuS) o LLMs tratadas estrictamente como propuestas no confiables sujetas a prueba formal.

03Verificación formal mediante SMT

Verificación formal

Resolución de obligaciones de buena definición y equivalencia semántica con solucionadores SMT (Z3) en dominios acotados de vectores de bits y secuencias de bytes.

04Persistencia y revaluación de evidencia semántica

Custodia de evidencia

Estudio del comportamiento de identidades semánticas direccionadas por contenido ante cambios de especificación, actualizaciones del solucionador y auditorías (EXP-019).

05Decodificación binaria acotada y eficiencia

Comparación empírica

Comparación empírica de construcciones de decodificación verificada en EFCH Lang frente a C manual, Rust con Kani, Go y Dafny en tareas controladas.

CATÁLOGO AGRUPADO POR LÍNEA DE INVESTIGACIÓN

Preprints vinculados con sus artefactos reproducibles

En lugar de listar cuatro elementos inconexos, Venture Synaptic Labs agrupa cada investigación para que quien visite la página pueda leer el manuscrito, examinar sus resultados (positivos y negativos) y acceder al código y los datos que permiten reproducirlos.

Estructura de publicaciones (fechadas el 2 de noviembre de 2026): 2 Preprints en borrador público + 2 Paquetes de artefactos de software/datos publicados. Los resultados negativos y mixtos se reportan con igual visibilidad que los positivos.

[INVESTIGACIÓN P1 · EXP-019]Experimento EXP-019 · 2026-11-02

Persistencia de Evidencia Semántica, Reverificación Completa y Memoización Reforzada

Erik Fisher Cueva Huari (VentureSynaptic Labs)ORCID: 0000-0001-7268-5510

Preprint P1 · Manuscrito de InvestigaciónBorrador público (Sin revisión por pares)

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

Manuscrito en borrador (2026-11-01 / 2026-11-02) · 2026-11-02

Experimento controlado prerregistrado y auditado internamente sobre un dominio acotado de vectores de bits que compara tres condiciones a lo largo de 64 transiciones de revisión de software (576 obligaciones objetivo): reverificación completa (Condición A), memoización reforzada de consultas SMT (Condición B) y almacén de evidencia semántica (Condición C).

I. Respaldado en el dominio

La Condición C requirió 252 invocaciones al solucionador frente a 576 de la reverificación completa (reducción del 56,25%).
Los 8 controles adversariales de solidez pasaron en la Condición C sin reutilización inválida confirmada en las 576 obligaciones decididas.
Superó a la memoización reforzada (Condición B) únicamente en el estrato de cambios equivalentes (32 frente a 40 invocaciones).

II. Resultados negativos y límites

Resultado negativo de eficiencia global frente a línea base incremental fuerte: la Condición C requirió 2,625 veces más invocaciones (252) que la memoización reforzada de consultas SMT (Condición B, 96 invocaciones).
Un prototipo híbrido exploratorio posterior (P0/P1) redujo algunas llamadas pero incrementó el tiempo total y expuso los defectos de integridad D10–D13 y la limitación arquitectónica L-D14.

Acceso al preprint: El registro individual de Preprint P1 figura como borrador en Zenodo; el PDF completo compilado (paper/main.pdf) y su código fuente LaTeX (paper/main.tex) están disponibles públicamente en el repositorio inferior e incluidos dentro del paquete publicado en Zenodo v1.1-exp019 (10.5281/zenodo.23874125).

Manuscrito PDF (paper/main.pdf)LaTeX (paper/main.tex)

Artefactos P1 · Software y DatosPublicado en Zenodo y GitHub

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

Exportación inmodificada desde venture-synaptic/efch-research con manifiesto de protocolo congelado (tag exp019-protocolo), instrumento (tag exp019-instrumento), registros crudos (data/exp019-resultados.tar.gz) y auditoría interna.

DOI Conceptual (Zenodo):10.5281/zenodo.23873678 ↗

v1.1-exp019 (2026-11-02 · Última versión)10.5281/zenodo.23874125 ↗

Incluye el borrador actualizado del manuscrito en PDF/LaTeX, protocolo congelado y archivo crudo de evaluación (31,8 MB).

v1.0-exp019 (2026-11-02 · Versión inicial)10.5281/zenodo.23873679 ↗

Publicación inicial de artefactos con tarball determinista de evaluación y SHA256SUMS.

Protocolo de verificación y reproducción (SHA-256):

$ 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

[INVESTIGACIÓN P2 · EXP-004 A EXP-015]Experimentos EXP-004, EXP-005, EXP-007, EXP-008, EXP-009, EXP-010 y EXP-015 · 2026-11-02

Decodificación Binaria Verificada con EFCH Lang frente a C, Rust-Kani y Dafny

Erik Fisher Cueva Huari (VentureSynaptic Labs)ORCID: 0000-0001-7268-5510

Preprint P2 · Manuscrito de InvestigaciónBorrador público (Sin revisión por pares)

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

Manuscrito en borrador v0.2 (2026-11-02) · 2026-11-02

Estudio empírico de EFCH Lang 0.1 — un lenguaje específico de dominio restringido que traduce programas de procesamiento binario acotado a C y verifica su equivalencia frente a especificaciones funcionales en Z3 — comparado frente a C manual, Rust con Kani, Go y Dafny.

I. Respaldado en el dominio

EXP-005 (benchmark de 8 funciones): las 8 funciones binarias acotadas fueron verificadas bajo protocolo; el C generado alcanzó una media geométrica de tiempo de ejecución de 0,90 frente a C manual.
EXP-015 y EXP-004: los decodificadores de opciones IPv4 y varint sin signo superaron todas las pruebas diferenciales y verificaciones acotadas con razones de tiempo de 1,027 y 0,966 frente a C (reejecutados el 2 de noviembre de 2026 con 1,030 y 0,965).

II. Resultados negativos y límites

El análisis adversarial de EXP-005 demostró que las comparaciones de esfuerzo frente a Rust-Kani y Dafny eran sensibles a la representación, y que una especificación directa en Dafny eliminaba la ventaja aparente de esfuerzo.
EXP-007 y EXP-008 (Negativos): un decodificador de nombres DNS escrito como máquina de estados agotó el tiempo límite de 900 s en SMT y fue 5,6 veces más lento que C manual.
EXP-009 y EXP-010 (Mixtos): añadir un pliegue acotado permitió verificar DNS en 16,9 s (1,02× tiempo de C), pero Dafny lo verificó en 2,95 s con menos líneas; el analizador de opciones TCP solo superó el criterio registrado en tiempo de verificación.

Acceso al preprint: El registro individual de Preprint P2 figura como borrador en Zenodo; el PDF completo compilado (paper/main.pdf) y su código fuente LaTeX (paper/main.tex) están disponibles públicamente en el repositorio inferior e incluidos dentro del paquete publicado en Zenodo v1.0-lang (10.5281/zenodo.23874420).

Manuscrito PDF (paper/main.pdf)LaTeX (paper/main.tex)

Artefactos P2 · Software y DatosPublicado en Zenodo y GitHub

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

Contiene protocolos prerregistrados y resultados de EXP-004, EXP-005, EXP-007, EXP-008, EXP-009, EXP-010 y EXP-015, 178 pruebas unitarias y archivo de reejecución del 2 de noviembre de 2026.

DOI Conceptual (Zenodo):10.5281/zenodo.23874419 ↗

v1.0-lang (2026-11-02 · Última versión)10.5281/zenodo.23874420 ↗

Paquete publicado de 68,5 MB con código de EFCH Lang 0.1, corpus comparativo (C, Rust-Kani, Go, Dafny), experimentos negativos, reejecución del 2 de noviembre y manuscrito v0.2.

Protocolo de verificación y reproducción (SHA-256):

$ 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

ARQUITECTURA DE TRAZABILIDAD CIENTÍFICA

Cómo integramos Zenodo, GitHub, ORCID y Venture Synaptic Labs

Cada plataforma cumple una función específica y verificable para que cualquier investigador pueda pasar directamente de un manuscrito a sus registros crudos de evaluación y scripts de reproducción.

01 / ZenodoArchivo y DOI

Fuente principal de archivo científico donde se registran DOIs versionados, fechas de publicación, autoría y paquetes descargables.

El archivo en Zenodo garantiza permanencia y trazabilidad de versiones; no implica evaluación por pares de una revista.

Registro Zenodo 23873679

02 / GitHubCódigo y Versiones

Fuente técnica con repositorios, código, protocolos congelados, manifiestos SHA-256 y fuentes LaTeX/PDF de los manuscritos.

El trabajo continuo se realiza en venture-synaptic/efch-research; cada corte experimental congelado se exporta a su repositorio público de artefactos.

venture-synaptic/efch-research

03 / ORCIDIdentidad del Autor

Identificador persistente del investigador (Erik Fisher Cueva Huari · 0000-0001-7268-5510) vinculado en los metadatos de los preprints y DOIs.

ORCID acredita la identidad académica y atribución persistente del autor, sin confundirlo con una certificación de calidad científica.

ORCID 0000-0001-7268-5510

04 / Venture Synaptic LabsCatálogo Público

Portal institucional que organiza las publicaciones por línea de investigación y relaciona cada preprint con sus artefactos y resultados negativos.

Separa rigurosamente hipótesis, resultados empíricos acotados y limitaciones abiertas respecto de los productos comerciales.

Catálogo @venture-synaptic

Registros institucionales iniciales verificados

Repositorio de investigación EFCH (venture-synaptic/efch-research)

Repositorio matriz de investigación (actualmente privado; sus exportaciones inmodificadas y auditables son públicas en los repositorios de artefactos P1 y P2).

Identidad académica ORCID (0000-0001-7268-5510)

Erik Fisher Cueva Huari — Perfil académico de autor en VentureSynaptic Labs.

Registro de Zenodo compartido (10.5281/zenodo.23873679)

Paquete publicado de artefactos P1 (v1.0-exp019; actualizado en v1.1-exp019 bajo DOI 10.5281/zenodo.23874125).

§ 03 — Categorías de estado epistémico

Experimentos públicos auditables y resultados

Los experimentos negativos, inconclusos y refutados se publican con la misma visibilidad que los positivos.

[PRP]Propuesto (Proposed)

Formulado en un RFC o documento de diseño; protocolo experimental aún no ejecutado.

[INV]En investigación (Under investigation)

Línea experimental activa con instrumentación prototipo en evaluación.

[SUP]Respaldado dentro del alcance (Supported within scope)

La evidencia empírica o formal respalda la hipótesis estrictamente dentro del protocolo y dominio acotado evaluado.

[INC]Inconcluso (Inconclusive)

Los resultados muestran compromisos o métricas mixtas sin establecer una ventaja decisiva frente a los comparadores.

[REF]Refutado (Refuted)

La evaluación controlada contradijo la hipótesis inicial o no superó el criterio de compuerta predefinido.

[EXP-019][SUP]Respaldado dentro del alcance

EXP-019 — Persistencia de Evidencia Semántica frente a Reverificación Completa y Memoización Reforzada

efch-artifacts-p1-evidence-persistence DOI: 10.5281/zenodo.23873679

Pregunta y Protocolo

¿Cómo se comporta la persistencia de evidencia semántica frente a la reverificación total y la memoización reforzada ante cambios de especificación y de solucionador?

Protocolo congelado (tag exp019-protocolo) que compara reutilización de evidencia, solidez de invalidación y recálculo de auditoría en escenarios controlados.

Hallazgo y Límites Declarados

Demuestra compromisos controlados entre reutilización e invalidación segura dentro del corpus evaluado; documentado en el borrador 'Safe Reuse Is Not Enough'.

Los defectos de integridad D10–D13 y la limitación arquitectónica L-D14 permanecen abiertos; la auditoría interna fue ejecutada por un agente de IA (Codex) y no por un investigador humano externo independiente.

[EXP-004 / EXP-015][SUP]Respaldado dentro del alcance

EXP-004 y EXP-015 — Decodificación Binaria Acotada y Verificación de Equivalencia en EFCH Lang

efch-artifacts-p2-lang-binary-decoding DOI: 10.5281/zenodo.23874420

Pregunta y Protocolo

¿Puede un DSL restringido (EFCH Lang 0.1) demostrar obligaciones de seguridad y equivalencia en decodificadores binarios acotados generando C competitivo con código manual?

Evaluación empírica y reejecución del 2 de noviembre de 2026 de decodificadores binarios acotados con pruebas de equivalencia en Z3, vectores diferenciales y medición en C (gcc -O2).

Hallazgo y Límites Declarados

Ambos programas demostraron equivalencia en SMT, superaron todos los vectores diferenciales y reprodujeron las razones de tiempo M9 (1.030 y 0.965 frente a 1.027 y 0.966).

Restringido a dominios pequeños sin bucles (bytes <= 64); el traductor a C se contrasta mediante pruebas diferenciales, no está demostrado formalmente.

[EXP-005 / EXP-010][INC]Inconcluso (Compromisos dependientes del dominio)

EXP-005 y EXP-010 — Estudio Comparativo Multilenguaje (C, Rust-Kani, Go, Dafny)

efch-artifacts-p2-lang-binary-decoding DOI: 10.5281/zenodo.23874420

Pregunta y Protocolo

¿Cómo se compara EFCH Lang 0.1 frente a lenguajes establecidos y herramientas de verificación formal en esfuerzo de especificación, tiempo de prueba y ejecución?

Corpus comparativo entre C manual, Rust (Kani 0.68.0), Go 1.26 y Dafny 4.11.0 con revisiones adversariales de protocolo.

Hallazgo y Límites Declarados

Muestra ergonomía específica en decodificación de paquetes acotados, junto con límites claros de expresividad frente a sistemas generales como Dafny y Kani.

La instantánea de código en el paquete P2 corresponde al 1 de noviembre de 2026 en lugar del código exacto del 21–24 de octubre en 8 archivos evolucionados; documentado de forma transparente en la procedencia del repositorio.

[EXP-007 / EXP-008 / EXP-009][REF]Refutado / Resultados negativos preservados

EXP-007, EXP-008 y EXP-009 — Evaluaciones Negativas y Límites en EFCH Lang

efch-artifacts-p2-lang-binary-decoding DOI: 10.5281/zenodo.23874420

Pregunta y Protocolo

¿Dónde fallan o pierden eficacia las abstracciones de EFCH Lang 0.1 y las obligaciones SMT (incluyendo el análisis de mensajes DNS)?

Experimentos revisados adversarialmente para evaluar límites de complejidad de protocolos e hipótesis negativas.

Hallazgo y Límites Declarados

Archivados íntegramente en el paquete P2 para documentar dónde las restricciones de dominio actuales o los tiempos límite del solucionador impiden ventajas.

Evidencia los límites estructurales del modelo sin bucles ante compresión de punteros de longitud variable y protocolos con estado.

[EXP-001 / EXP-002 (Compuerta G4)][REF]Refutado (Compuerta G4 no superada)

EXP-001 y EXP-002 — Optimización frente a Compiladores Estándar (Compuerta G4)

README-efch-0.1.0a1.md

Pregunta y Protocolo

¿La búsqueda de candidatas sobre especificaciones EFCH descubre implementaciones más rápidas que un compilador optimizador estándar (gcc -O2) en primitivas escalares?

Evaluación de rutinas escalares (ej. popcount64, varint) materializadas en C y compiladas con gcc -O2.

Hallazgo y Límites Declarados

Sin ventaja de rendimiento frente a gcc -O2; la compuerta G4 ('Investigación estructural') figura explícitamente como no superada en EFCH v0.1.

Medición en una sola máquina; ciertas equivalencias algebraicas en vectores de 64 bits quedan como 'desconocido' en SMT.

[RFC-LIVE-0.1][PRP]Propuesto (Etapa RFC / Diseño)

EFCH Live Engineering y Contract Conformance Pack 0.1

README-efch-0.1.0a1.md

Pregunta y Protocolo

¿Pueden separarse la supervisión humana (H1) y la persistencia de evidencia (H2) mediante un contrato semántico mínimo para reconciliación asíncrona?

RFC documental y validador de esquemas sobre corpus sintético (Contract Conformance Pack 0.1).

Hallazgo y Límites Declarados

Recomienda reformular el alcance antes de autorizar un estudio P0; los chequeos de trazas no certifican autenticación, atomicidad ni corrección semántica.

Etapa documental y de validación sintética únicamente; no valida hipótesis empíricas.

Principios metodológicos

01 —

Comparadores justos y versiones fijadas

Los experimentos contrastan frente a líneas base reales (gcc -O2, Rust 1.93 + Kani 0.68.0, Go 1.26, Dafny 4.11.0, cvc5 1.4.2) con dependencias verificadas por SHA-256.

02 —

Protocolos prerregistrados y manifiestos congelados

Cuando aplica (como en EXP-019), los protocolos de evaluación y las huellas del instrumento se congelan antes de ejecutar el corpus de evaluación.

03 —

Igual visibilidad para resultados negativos

Las hipótesis refutadas (Compuerta G4, EXP-007–009) y los defectos de integridad abiertos (D10–D13, L-D14) se publican junto con los resultados favorables.

04 —

Procedencia explícita y declaración de agentes de IA

Los README de los artefactos documentan los commits exactos de origen, las limitaciones de las instantáneas y la participación de agentes de IA (Claude, Codex) bajo dirección y responsabilidad del autor.