GitHub - typescope/jo: Jo Secure Programming Language

Jo is a statically typed language that enables compile-time sandboxing. Instead of confining a running program from the outside, Jo proves — before the code runs — that it can only use the capabilities it was explicitly granted. Jo compiles to Ruby and Python.

Project status: Early-stage. The compiler, standard library, and toolchain are ready for serious experimentation. APIs and language details may still change.

Why compile-time sandboxing?

AI agents now generate code that runs inside your platform. That code can — unless you stop it — reach for the network, read arbitrary files, or query other users' data.

The usual defense is a runtime sandbox: a container, VM, or seccomp filter that wraps the running program and polices it from the outside. But runtime sandboxes operate at the wrong level. They can block a syscall or a filesystem path, but they cannot express "access only this user's rows" — that is application logic, invisible to the OS.

Jo moves the sandbox into the type system. A capability a function never received is one it cannot use, and the compiler proves this transitively across the entire call graph — before the program runs. The boundary is visible right in the code, there is nothing to escape at runtime, and "only this user's data" becomes an ordinary, checkable type.

Function parameters (capabilities) are the only door to the outside world.

Language Highlights

Static capability control

def foo() = println "foo"                     // inferred capability: stdout
def bar() = foo()                              // inferred capability: stdout

def qux() receives IO.stdout = println "qux" // explicit: only stdout

def main =
  allow none in bar()                         // error: no capabilities allowed
  allow IO.stdout in bar()                    // OK
  with IO.stdout = s => pass in qux()         // redirect output

---------- Error at main.jo:5:3 ---------------
|   allow none in bar()
|                 ^^^^^
|   Parameter not allowed: stdout

The following is the trace that leads to the problem:
├──   allow none in bar()     [ main.jo:5:3 ]
│                   ^^^^^
├── def bar() = foo()         [ main.jo:2:13 ]
│               ^^^^^
└── def foo() = println "foo" [ main.jo:1:13 ]
                ^^^^^^^

Pattern-oriented programming

Named, reusable pattern predicates compose with logical operators:

pattern Positive: Partial[Int] = case x if x > 0

match list
case [..positives while Positive, ..rest] =>
  println "pos = \{positives}, rest = \{rest}"

case _ => pass

if result is Some(code) && code > 0 then
  println "Success, code = \{code}"

// enable option "s" to allow . to match new line
if message is `(?s)<code>(?<prog>.*)</code>` then
  println prog

Confining AI-Generated Code

The two-world architecture separates confined code (no FFI, checked against capability interfaces only) from trusted code (FFI allowed, implements and provides capabilities):

//--- Interface library (confined, no FFI) ---
param ordersApi: OrdersApi
defer def aiMain(): Unit receives ordersApi, IO.stdout

//--- Framework harness (trusted, FFI allowed) ---
def frameworkMain() =
  val db = connect("orders.db")
  val userId = currentUser()
  val restricted = new UserScopedOrders(userId, db)  // attenuated: user-scoped, read-only
  val buffer = (s: String) => output += s

  allow none in
    with ordersApi = restricted, IO.stdout = buffer in aiMain()

//--- AI-generated code (confined, no FFI) ---
def aiMain(): Unit receives ordersApi, IO.stdout =
  val orders = ordersApi.query(30)
  printOrders: orders.select(o => o.state == "open")

allow none is a compile-time proof: aiMain() uses no capabilities beyond what it declared. The AI code cannot access the network, filesystem, or other users' data.

See the security documentation for the full model.

Try Jo

curl -sSf https://jo-lang.org/install.sh | sh

The installer downloads the compiler to ~/.jo/compilers/<version>/ and creates a launcher at ~/.local/bin/jo. Add ~/.local/bin to PATH if it is not already there.

Full installation instructions and a getting-started guide are at jo-lang.org.

Theoretical Foundations

Jo's capability model is grounded in λCC, a formally verified calculus of contextual capabilities. λCC provides a mathematical account of static capability tracking and the proof is mechanized in Coq.

Learn More

Contributing

See CONTRIBUTING.md for build instructions, contribution guidelines, and the DCO sign-off requirement. Bug reports, language design discussions, and pull requests are welcome.

Security issues should be reported privately — see SECURITY.md.

License

Apache 2.0 — see LICENSE.

Jo is developed and maintained by TypeScope.