ETC Verify™ is the formal verification framework of Evolving Technologies Corporation, delivered as software and through the services described below. It is available as downloadable software. We take the behavioral claims your design documents make in prose and convert them into precise mathematical propositions. Then we prove them, with machine-checked rigor, using the Lean theorem prover.
Testing shows that a behavior held in the cases you tried. It says nothing about the cases you didn't. A machine-checked proof covers every case the model admits, and states its assumptions out loud. For systems where failure is expensive, that difference is the product.
Much of what the ETC Verify™ framework addresses lives at interfaces. When independently developed systems are integrated against shared interface specifications, maturity in each subsystem does not retire the risk between them. It concentrates it at the seams. Where an interface obligation cannot be discharged, the framework gives the gap a named location and a stated obligation, rather than leaving it as a general concern discovered during integration.
ETC Verify™ Services
Feasibility assessment. We determine which behavioral properties of your system can be formally characterized, classify each honestly (tractable now, pilot-scale, or research-scale), estimate the effort, and demonstrate the method on a worked example from your own design. Negative findings are treated as valuable results: a property that fails as stated, with a witness, is discovered on your terms rather than a customer's.
Formal specification. We translate design narratives, configuration inventories, and engineering documentation into precise candidate definitions, assumptions, and invariants, producing a formalization-ready register mapped to your own code and constants. Inconsistencies, gaps, and ambiguities in the source material are surfaced as findings.
Machine-checked verification. We state and prove properties of algorithm models in the Lean theorem prover, delivering compiling, machine-certified artifacts together with a documented correspondence between the model and your implementation.
Empirical and statistical validation. We analyze your system's behavior against real operational data, characterizing input patterns statistically and pairing that empirical layer with formal conditional proofs, so that each proven guarantee rests on a validated model of the environment it assumes.
Software
The ETC Verify™ substrate is published as downloadable software under the Apache 2.0 license, with tagged releases available at https://github.com/evolvingtech. It provides the contract algebra and verification machinery on which the services above are built.
Where We Work
We work where the cost of being wrong is high and the interfaces are many. Our center of gravity is interface and interoperability verification between independently developed systems. The surrounding terrain includes communication systems and protocols, distributed algorithms, timing- and ordering-critical components, and numerical and floating-point interoperability, with much of our work bound for high-assurance domains including aerospace and government applications.
How Engagements Are Structured
Engagements are phased so that each phase buys the next one's clarity: a short feasibility assessment establishes what can be proved and at what cost, a pilot delivers the first machine-checked results on the properties that matter most, and a broader program extends coverage across the system. Every finding is stated relative to its model and assumptions, which are documented for your review.
Contact
Evolving Technologies Corporation Brooklyn, New York