About Lingenic

Lingenic LLC, Wyoming · [email protected] · 1-888-312-5771

Lingenic builds solutions centered on logic, linguistics, and formal methods.

Lingenic-Text is the first public, formally verified, Unicode text processing library, proven in SPARK/Ada: every algorithm in the Unicode standard encoded as a specification, and proven — proof that the code matches the specification, and conformance tests that the specification matches the standard.

Lingenic was co-founded by Danslav Slavenskoj, who was asked to teach his class programming while in the third grade, and while still in high school, received a scholarship to take Introduction to Logic at Harvard University, where he later received a graduate degree.

Lingenic works on the recovery and completion of exceptional historic designs that went dormant for contingent reasons rather than flaws in the design itself. Lingenic Compose modernizes Multics Compose (1972–1985): the document model was right, but the system it ran on disappeared. Buran recovers Pāṇini's grammatical transformation model (~4th c. BCE) and Refal's pattern-matching core (1966) for computational linguistics. These are not revivals for their own sake; in each case the original design solved the problem correctly, and what has changed is the surrounding conditions that blocked adoption.

The company's founding notation, Lingenic, embeds extensible formal systems — propositional logic, probability, type theory, dependent types — directly into documents whose surrounding content is unmodified natural language, for a new type of reader: AI models.