Orbis Specification Language: a type theory for zk-SNARK programming

Orbis Specification Language: a type theory for zk-SNARK programming

image

We are delighted to announce the second paper published by Orbis Labs, which is a major step in the development of Orbis. This paper “Orbis Specification Language: a type theory for zk-SNARK programming” by our CTO Morgan Thomas explains how OSL is a language for expressing statements to be proven by zk-SNARKs in a math-like notation.

OSL takes away the zk-SNARK engineer's burden of making a non-obvious translation of a statement into a form which can be proven by a zk-SNARK. OSL is similar to languages like Haskell and Coq, which can express statements in a math-like, machine-readable notation. The difference is that OSL is engineered to be amenable to translation into a form which can be used to make zk-SNARK proofs.

We look forward to our future publications which will further outline the techniques and technologies we are using to build Orbis, the first general purpose layer 2 scaling solution for Cardano.

Posts