VENTURE SYNAPTIC
ENES
02 / Back to Foundry
FOUNDRY / EXPERIMENTAL TOOLCHAIN[EXP]Alpha 0.1.x · Experimental tooling

EFCH Lang — Language & Toolchain

EFCH Lang is an experimental programming language and toolchain exploring explicit contracts and verifiable behavior, initially within bounded program domains.

VERIFICATION SCOPE:Verification boundary: Discharging formal proof obligations in the EFCH core and specified bounded domains proves mathematical properties of the specification/candidate model in Z3. It does not formally verify the compiler implementation, the generated C code, or the final machine binary.

VERSION TRACKS // ARCHITECTURE

Version lines: 0.1.x (Alpha) vs. 0.2 (In development)

0.1.x — Alpha Maintenance & Tooling Line

Current Alpha (0.1.0a1 / 0.1.x)

Focused on bounded binary decoding, bit-vector computations, canonical evidence schemas, and editor/SDK integration.

  • Dual file model: formal S-expression specifications (.efch) paired with structured implementation modules (.efl)
  • Canonical JSON evidence schema (efch-evidencia/1.0) via efch export check and efch export lang
  • TypeScript SDK (efch-lang-sdk-ts) and .NET 8 SDK (EfchLang.Sdk) for CI/test integration
  • Language Server Protocol v3.17 server (efch-lang-lsp) and VS Code extension (v0.1.2)

0.2 — Semantic Evolution Line

In development · Unreleased

Exploratory design work investigating broader semantic constructs and addressing 0.1 domain limitations.

  • Under active internal research and engineering design
  • Not released, not packaged for public installation, and not claimed as an available product feature
VERIFIED CAPABILITIES

Verified capabilities in 0.1.x (within bounded domains)

  • +01Well-definedness checking (efch check): discharges type and domain safety obligations on .efch specifications using Z3.
  • +02Equivalence & property verification (efch verify): proves or refutes with concrete counterexamples whether an .efl/.efch candidate satisfies its formal specification.
  • +03C code generation (efch build): emits C implementations from verified candidates for compilation with gcc -O2 and differential testing.
  • +04Editor & CI diagnostics: surfaces concrete SMT counterexamples and specification-to-implementation navigation via LSP v3.17.
TRUST BOUNDARIES

Current limitations & domain restrictions

  • !01Bounded execution model only: no unbounded loops, recursion, dynamic memory allocation, or side effects.
  • !02Input size cap: byte-slice inputs (bytes) are restricted to a maximum of 64 bytes in the 0.1.0a1 core.
  • !03Unverified C backend: the translator from EFCH core to C is tested differentially, not formally verified.
  • !04Solver timeouts: complex bit-vector arithmetic properties may return 'unknown' when exceeding SMT solver resource limits.
  • !05Repository visibility: while the core EFCH Lang 0.1 compiler and tests are publicly archived in efch-artifacts-p2-lang-binary-decoding, the standalone SDK/LSP/VS Code repositories in @venture-synaptic are currently private pending public release approval.

COMMAND REPRODUCTION

Verified reproduction commands (Public P2 Artifact Package)

The following commands are verified against the public repository venture-synaptic/efch-artifacts-p2-lang-binary-decoding (requires Python >= 3.10 and gcc on Linux/POSIX):

$ git clone https://github.com/venture-synaptic/efch-artifacts-p2-lang-binary-decoding.git
$ cd efch-artifacts-p2-lang-binary-decoding
$ sha256sum -c SHA256SUMS
$ tar -xzf data/efch-lang-resultados.tar.gz
$ scripts/vendor_z3.sh
$ python3 -m unittest discover -s tests

EFCH Lang ecosystem components

venture-synaptic/efch-artifacts-p2-lang-binary-decoding
Python 3.10+, Z3 5.1.0.0, C (gcc)

Public archive containing the EFCH 0.1 core & EFCH Lang implementation, 178 unit tests, and reproducible scripts for EXP-004 to EXP-015.

PUBLICOpen public repository ↗
venture-synaptic/efch-lang-sdk-ts
TypeScript, Node.js (execFile)

Official TypeScript SDK for interacting with the EFCH 0.1.x compiler, formal verifier, and CLI diagnostics.

INTERNALView @venture-synaptic org ↗
venture-synaptic/efch-lang-sdk-dotnet
C#, .NET 8, xUnit

.NET 8 SDK (EfchLang.Sdk) consuming canonical efch-evidencia/1.0 JSON contracts for C# / xUnit CI integration.

INTERNALView @venture-synaptic org ↗
venture-synaptic/efch-lang-lsp
TypeScript, LSP v3.17 (stdio)

Language Server Protocol (v3.17) server for .efl and .efch specifications built on efch-lang-sdk-ts.

INTERNALView @venture-synaptic org ↗
venture-synaptic/efch-lang-vscode
TypeScript, VS Code Extension API

VS Code extension for syntax highlighting, formal verification commands, and LSP integration for .efl and .efch.

INTERNALView @venture-synaptic org ↗