Taran.Space has delivered 3 formal-methods research projects for JetBrains across Coq, Agda, Homotopy Type Theory, formal specifications, verified code generation, and Operational Transformation proofs. The work connected theorem-proving research with practical developer tooling, including a Coq-to-Java generation project, a Visual HoTT interpreter prototype, and Coq/Agda proofs for collaborative-editing transformations.
Verification Transpiler was a JetBrains research project exploring how formally verified specifications could move closer to production software. The work extended Coq so Java code could be generated directly from Coq specifications, connecting proof-oriented development with a mainstream application runtime.
The project focused on preserving the value of mathematical specification and proof while making verified logic easier to integrate into larger software systems. It combined formal methods, language tooling, and practical compiler-style engineering around Coq and Java.
This JetBrains research project focused on formal reasoning about Operational Transformations, a core technique behind collaborative editing systems. Taran Space developed Coq and Agda proofs for transformation behavior, using proof assistants to model correctness properties in systems where multiple users edit shared state concurrently.
Proof work centered on consistency guarantees, transformation rules, and edge cases that determine whether concurrent edits converge correctly. The project applied formal verification techniques to a problem space normally hidden inside real-time collaboration software.
The Visual HoTT Interpreter was a JetBrains research project for exploring Homotopy Type Theory through an interactive interpreter interface. Taran Space prototyped tooling that made abstract type-theory concepts easier to inspect, experiment with, and reason about visually.
The work connected formal methods, programming-language research, and developer tooling. It focused on interpreter behavior, interactive representation of HoTT concepts, and practical experimentation with proof-oriented ideas outside a purely textual proof-assistant workflow.
Tell us what you’re building and what kind of security support you need. Telegram is usually the fastest way to reach us. For formal inquiries, you can also use email.
