EFCH — Property-Oriented Computing Research
EFCH explores whether software systems can be engineered from explicit properties and constraints, with synthesis, verification and execution organized around those specifications.
TECHNICAL SCHEMATIC // VERIFICATION PIPELINE
Experimental pipeline in EFCH 0.1.0a1
In the EFCH prototype, the source of truth is a formal definition (.efch) rather than handwritten implementation code. Implementations are treated as candidates that must pass independent formal verification before C materialization.
definition (.efch) ──► typed core ──► semantic identity (SHA-256)
│
candidates (.efl / LLM / SyGuS) ──────┼──► SMT (Z3 5.1.0.0): well-defined + equivalent ──► proved | refuted | unknown
│
└──► C (gcc -O2) ──► differential vectors ──► interleaved timing ──► evidencia.json1. Formal Definition (.efch)
Declares exact semantics, mathematical properties, bounded input domain, workload distribution, optimization objective, and resource budget.
2. Typed Core & Semantic Identity
Normalizes the specification into a typed core and computes a deterministic SHA-256 semantic identity.
3. Candidate Implementations
Candidates may come from human authors, EFCH Lang (.efl), enumerative SyGuS search (cvc5), or LLM-guided synthesis — all treated as untrusted proposals.
4. Independent SMT Verification (Z3)
Checks well-definedness and semantic equivalence against the specification, emitting proved, refuted (with counterexample), or unknown.
5. C Materialization & Differential Testing
Proved candidates are translated to C (compiled with gcc -O2), tested against differential vectors, measured via interleaved execution, and logged to evidencia.json.
HYPOTHESIS LEDGER // H1–H6
Research gates & experimental ledger
Semantic evidence persistence vs. full reverification and strengthened memoization under controlled specification and solver changes.
Evaluated under frozen protocol (tag exp019-protocolo); artifacts and draft manuscript archived at Zenodo (10.5281/zenodo.23873679). Defects D10–D13 and limitation L-D14 remain open.
Bounded binary decoding in EFCH Lang 0.1 with SMT equivalence verification and C code generation.
Equivalence proved in Z3 and reproduced on Nov 2, 2026 re-execution (M9 runtime ratios 1.030 and 0.965 vs C baselines). Archived at Zenodo (10.5281/zenodo.23874420).
Empirical comparison of EFCH Lang 0.1 against handwritten C, Rust-Kani 0.68.0, Go 1.26, and Dafny 4.11.0.
Demonstrates domain-specific conciseness for bounded packet decoding alongside clear expressiveness trade-offs vs general-purpose verification tools.
Protocol complexity stress tests (including DNS message parsing) and negative boundary evaluations.
Preserved in full in the P2 artifact archive to document where current bounded-domain restrictions and solver limits prevent effectiveness.
Structural performance advantage of synthesized/selected candidates over standard optimizing compilers (gcc -O2).
EXP-001 and EXP-002 showed no performance advantage over gcc -O2 on tested primitives; documented in README-efch-0.1.0a1.md.
Decoupling human oversight (H1) from semantic evidence persistence (H2) via minimal semantic contracts.
Documented in RFC and Contract Conformance Pack 0.1; does not authorize P0 implementation or validate empirical hypotheses.
METHODOLOGICAL BOUNDARIES
Explicit limitations of EFCH 0.1.0a1
- L-01Small, strictly bounded domain: no unbounded loops, no general recursion, no mutable heap memory, and no I/O side effects. Byte-slice inputs (bytes) are bounded to at most 64 bytes.
- L-02Unverified C translation: translation from the verified core to C is validated through differential testing, not formally proved.
- L-03SMT solver decidability & timeout limits: certain algebraic bit-vector equivalences (such as equivalence between two 64-bit adder trees in popcount.efch) return 'unknown' within the solver budget.
- L-04Non-deterministic LLM candidate generation: LLM-proposed candidates are non-deterministic, though once saved they are deterministically re-verified via efch verify.
- L-05Single-machine timing & open integrity defects: timing metrics depend on the host machine, and evidence store defects D10–D13 / limitation L-D14 remain open research items.
VERIFICATION & REPRODUCIBILITY
Public artifacts & informed reproduction
All public EFCH artifacts include SHA-256 manifests and scripts to pin Z3 5.1.0.0 so external researchers can inspect and re-run the experiments.
EFCH P1 Artifacts — Semantic Evidence Persistence (EXP-019)
Draft manuscript — not peer reviewed, not submitted. Research software (0.1.0a1).
EFCH P2 Artifacts — Verified Binary Decoding with EFCH Lang (EXP-004 to EXP-015)
Draft manuscript (v0.2) — not peer reviewed, not submitted. Research software (0.1.0a1).