Build an app that runs inside a TEE
A walkthrough, from an empty file to a service whose client verifies the code before sending anything — labels on, an attested identity, and the same checks running in CI with the development driver.
The example is deliberately small and completely real: a lender sends an applicant's score, the service answers yes or no, and nobody outside — including whoever runs the machine — gets to see the score. Every command and every line of output below is from a run on an ordinary laptop.
You need the binary and nothing else:
curl -fsSL https://synsema.org/install.sh | sh
1. The shape of a confidential service§
Before the syntax, the shape, because it is the part people get wrong. A confidential service has three moments:
1. Ingest — data arrives that you are not allowed to read as the operator. 2. Decide — the program computes with it, inside the box. 3. Publish — one small, deliberate value comes out, and you can say in a sentence why it may.
If step 3 is hard to state in a sentence, the design is not ready. The language will hold you to that sentence.
2. Write it, with the data marked§
intent: "score one applicant inside the enclave and publish only the decision"
require serve(8080)
require attest
let CUTOFF be 620
task verdict(payload)
let score be private(payload["score"], "applicant")
let approved be score >= CUTOFF
give declassify(approved, "the yes/no is what the lender asked for; the score stays inside")
serve on 8080
route "GET /identity"
give attestation_document()
route "POST /decide"
expect body {score: number}
give {"approved": verdict(json of request)}
Two lines carry the whole policy. private(…, "applicant") says who the value belongs to; declassify(…, "…") says what leaves and why. attestation_document() needs no capability and, run outside an attested server, fails with a clear error — so a route that serves the identity is honest by construction.
3. Run it with the wall up§
synsema serve app.syn --port 8080 --labels
Labels are off under a plain synsema run, and always on under serve --attested. Turning them on explicitly while developing is how you find out early. Try publishing the score instead of the decision and the response never leaves the machine:
{"error": "label_violation: response.score is private to applicant, the sink accepts (public);
declassify(<that value>, \"<why it may be published>\") the scalar you want to publish and build
the container outside the private branch", "status": 500}
The message names the value, the sink and the two fixes. Nine times out of ten the right one is the first: the destination should have been private too.
Before shipping, read what the program publishes — the list is produced before anything runs:
synsema code check app.syn --json
"declassify": [
{"file": "app.syn", "line": 11, "column": 20,
"reason": "the yes/no is what the lender asked for; the score stays inside"}
]
One entry, one sentence. That is the security review of this service.
4. Give it an identity§
synsema serve --attested app.syn --port 8443
Serving HTTPS on port 8443 (2 route(s))
Attested: driver=mock format=mock program_sha=d0e0701a3a80627ff0fa867ff2bf57b1d8367c5a68bc89448079b5e777ff3bc7
— GET /.well-known/attestation
The server generated a P-256 keypair, asked the platform for a document binding sha256(spki ‖ program_sha ‖ config_sha), terminated TLS with that same key, and published the document. If the platform had not answered, it would not have started: there is no degraded mode to fall into.
What it publishes:
{"format": "…", "driver": "…", "engine": "v0.6.24",
"public_key": "-----BEGIN PUBLIC KEY-----…", "public_key_hex": "3059301306072a8648…",
"program_sha": "d0e0701a…", "config_sha": "c684dde2…",
"config": {"ceiling": "unbounded", "engine": "v0.6.24", "labels": true,
"profile": "native", "tls_key": "attested"},
"document": "hEShATgioFkGwqlpbW9kdWxlX2lka2ktbW9jay1l…"}
Note config. It is the mode, not only the program: the ceiling, that labels were on, the profile, and that the TLS key is the attested one rather than an operator certificate. Its hash is inside the signed payload, so the configuration cannot be attested hard and served soft.
Two rules to keep in mind here: --attested and --watch are mutually exclusive (a restart would change the identity underneath live clients), and the program may not declare /.well-known/attestation, /openapi.json, /docs, /llms.txt, /sitemap.xml or /robots.txt — the server refuses to start rather than let one be shadowed silently.
5. The client, which is the point§
A confidential service nobody verifies is a confidential service in name only. The verifier is a program in the same language, and it needs no capability and no network beyond fetching the document:
let seen be json_decode(read_file("identity.json"))
let v be attestation_verify(bytes(seen["document"], "base64"),
{"format": seen["format"], "now": floor(now())})
let bound be sha256(bytes(seen["public_key_hex"], "hex")
+ bytes(seen["program_sha"], "hex")
+ bytes(seen["config_sha"], "hex"))
print("pcr0 " + v["measurements"]["pcr0"])
print("user_data " + decode(v["user_data"], "hex"))
print("recomputed " + decode(bound, "hex"))
print("it is the code it says it is: " + text(v["user_data"] == bound))
print("labels on: " + text(seen["config"]["labels"]))
pcr0 0000000000000000000000000000000000000000000000000000000000000000…
user_data f269f90cd8922005db59c98d20cc0de0331fee956da2f2f222fc0b58b6609617
recomputed f269f90cd8922005db59c98d20cc0de0331fee956da2f2f222fc0b58b6609617
it is the code it says it is: true
labels on: true
In production add "expect": {"measurements": {"pcr0": "<the hex you published>"}}, which compares and fails closed on a mismatch, and only pin the public key after the verdict. opts.now is mandatory on purpose: the validity window is checked against a timestamp the verifier chooses, not against a clock the host controls.
Then, and only then, send the data:
curl -X POST https://your-enclave/decide -d '{"score": 710}'
{"approved": true}
curl -X POST https://your-enclave/decide -d '{"score": 480}'
{"approved": false}
Two requests, two bits out. The score never appeared in a response, a log line or a console.
6. Keep it honest in CI§
The whole path — document, TLS key, verification, the client's recomputation — runs on any machine with the development driver:
SYNSEMA_ATTEST=mock SYNSEMA_ATTEST_MOCK_SEED=ci synsema serve --attested app.syn --port 8443
synsema: warning: SYNSEMA_ATTEST=mock: documents are FORGEABLE (deterministic test key),
never trust them outside CI
It says so on stderr, it announces format: "mock", and every document it produces carries "mock": true — so a development document cannot be mistaken for a platform's in a log, in a client or in a screenshot. It is never auto-selected: on Linux the driver is detected from the machine, and the mock one only appears when you ask for it by name.
7. Before you call it confidential§
1. Check the engine you are shipping. gh attestation verify synsema-linux-x86_64 --repo kitecosmic/synsema answers with the workflow, commit and tag that produced those exact bytes. Attesting a program built by an engine of unknown provenance attests the wrong half. 2. Run with labels on and read the declassify list; make sure each sentence is one you would send to a customer, because effectively you are. 3. serve --attested, no --watch. Decide TLS: the attested key (the client pins it) or your own certificate (it must not). 4. Publish program_sha and the expected measurements where your users will look — a status page, a repository, the contract. 5. Give the counterparty the twenty lines of verifier above. If they will not run it, the property you built is not the one they are buying.
The language part ends here: what is left is choosing the hardware the box runs on, and that choice is a separate conversation about price, region and operations. The manual has the details — Attestation, Labels, Capabilities — and every page is also Markdown: add .md to its URL.