Silk

Systems language with formal verification built in.

Silk is designed for explicit modules, visible imports, clear ABI boundaries, target-aware code, and proofs that live with the program. Start with small programs, then move into packages, stdlib APIs, embedders, and Formal Silk.

Start learning Read the docs Wiki Spec (2026) GitHub

Small but representative

Guide

package hello;
import { println } from "std/io";
task fn score () -> int { return 21 * 2; }
async fn configured_name () -> string? { return Some("silk"); }

interface Greeter { fn write(n: string, s: int) -> void; }
struct ConsoleGreeter { label: string, }

impl ConsoleGreeter as Greeter {
  fn write (self: &ConsoleGreeter, n: string, s: int) -> void {
    println("[{s}] {s}: {d}", self.label, n, s);
  }
}
fn platform () -> string {
  if attr(target="wasm32-wasi") { return "wasi"; }
  if attr(os="linux") { return "linux"; }
  return "host";
}
async fn main () -> int {
  let raw = await configured_name();
  let name: Result(string, string) = Ok(raw ?? "world");
  let greeter = ConsoleGreeter{ label: platform() };
  match (name) {
    Ok(v) => greeter.write(v, yield score()),
    Err(e) => println("error: {s}", e),
  };
  return 0;
}