diff --git a/compiler/node_modules/.vite/vitest/results.json b/compiler/node_modules/.vite/vitest/results.json
index a6ca69e..a12343a 100644
--- a/compiler/node_modules/.vite/vitest/results.json
+++ b/compiler/node_modules/.vite/vitest/results.json
@@ -1 +1 @@
-{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":40.638667,"failed":false}],[":__tests__/e2e-wasm.test.ts",{"duration":25.08648199999999,"failed":true}],[":src/__tests__/compiler.test.ts",{"duration":13.108581000000015,"failed":false}]]}
\ No newline at end of file
+{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":39.401257999999984,"failed":false}],[":__tests__/e2e-wasm.test.ts",{"duration":108.43775999999997,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":11.341655000000003,"failed":false}]]}
\ No newline at end of file
diff --git a/compiler/src/generators/typescript-state-machine.ts b/compiler/src/generators/typescript-state-machine.ts
index 508a1b0..08d23a5 100644
--- a/compiler/src/generators/typescript-state-machine.ts
+++ b/compiler/src/generators/typescript-state-machine.ts
@@ -175,6 +175,11 @@ function emitSpeck(speck: SpeckNode): string {
 
   const stateVarNames = new Set(stateVars.map(v => v.name));
 
+  // Collect which state variables are Map types (for bracket -> .get() translation)
+  const mapVarNames = new Set(stateVars
+    .filter(v => v.typeExpr?.type === 'map' || (v.typeExpr?.type === 'ident' && v.typeExpr?.name && /^Map/i.test(v.typeExpr.name)))
+    .map(v => v.name));
+
   const stateProperties = stateVars.map(v => {
     return `  ${v.name}: ${tsType(v.typeExpr, speck.name, enumMap)};`;
   }).join('\n');
@@ -195,7 +200,7 @@ function emitSpeck(speck: SpeckNode): string {
       }).join('\n')
     : '';
 
-  const actionMethods = actions.map(a => emitAction(a, stateVarNames, speck.name, stateEnumName, allKnownStateValues, enumMap)).join('\n\n');
+  const actionMethods = actions.map(a => emitAction(a, stateVarNames, mapVarNames, speck.name, stateEnumName, allKnownStateValues, enumMap)).join('\n\n');
 
   const constraintChecks = constraints.map((c, i) =>
     `  // C${i + 1}: ${c.expr}\n` +
@@ -245,7 +250,7 @@ ${verifyChecks}
   return file;
 }
 
-function emitAction(action: ActionNode, stateVarNames: Set<string>, speckName: string, stateEnumName: string, knownStateValues: string[], enumMap: Map<string, string[]>): string {
+function emitAction(action: ActionNode, stateVarNames: Set<string>, mapVarNames: Set<string>, speckName: string, stateEnumName: string, knownStateValues: string[], enumMap: Map<string, string[]>): string {
   // Collect local parameter names so we DON'T prefix them with this.
   const localNames = new Set(action.params.map(p => p.name));
 
@@ -256,7 +261,7 @@ function emitAction(action: ActionNode, stateVarNames: Set<string>, speckName: s
   const preconditions = action.statements
     .filter(s => s.type === 'precondition')
     .map(s => {
-      const expr = rewriteExpr(s.expr, stateVarNames, localNames, stateEnumName, knownStateValues);
+      const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
       return `    // precondition: ${expr}\n    if (!(${expr})) throw new Error('Precondition failed: ${expr.replace(/'/g, "\\'")}');`;
     })
     .join('\n');
@@ -264,7 +269,7 @@ function emitAction(action: ActionNode, stateVarNames: Set<string>, speckName: s
   const requires = action.statements
     .filter(s => s.type === 'require')
     .map(s => {
-      const expr = rewriteExpr(s.expr, stateVarNames, localNames, stateEnumName, knownStateValues);
+      const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
       return `    if (!(${expr})) throw new Error('Guard failed: ${expr.replace(/'/g, "\\'")}');`;
     })
     .join('\n');
@@ -273,7 +278,7 @@ function emitAction(action: ActionNode, stateVarNames: Set<string>, speckName: s
     .filter(s => s.type === 'assign')
     .map(s => {
       const target = cleanName(s.target);
-      const expr = rewriteExpr(s.expr, stateVarNames, localNames, stateEnumName, knownStateValues);
+      const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
       return `    this.${target} = ${expr};`;
     })
     .join('\n');
@@ -284,7 +289,7 @@ function emitAction(action: ActionNode, stateVarNames: Set<string>, speckName: s
       const fields = s.fields
         .map(f => {
           const name = cleanName(f.name);
-          const val = rewriteExpr(f.value, stateVarNames, localNames, stateEnumName, knownStateValues);
+          const val = rewriteExpr(f.value, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
           return `      ${name}: ${val}`;
         })
         .join(',\n');
@@ -295,7 +300,7 @@ function emitAction(action: ActionNode, stateVarNames: Set<string>, speckName: s
   const postconditions = action.statements
     .filter(s => s.type === 'postcondition')
     .map(s => {
-      const expr = rewriteExpr(s.expr, stateVarNames, localNames, stateEnumName, knownStateValues);
+      const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
       return `    // postcondition: ${expr}\n    if (!(${expr})) throw new Error('Postcondition failed: ${expr.replace(/'/g, "\\'")}');`;
     })
     .join('\n');
@@ -309,7 +314,7 @@ function emitAction(action: ActionNode, stateVarNames: Set<string>, speckName: s
 
 // Rewrite SpeckDL expressions to valid TypeScript
 // Only prefix identifiers with `this.` if they are state variables AND not local params
-function rewriteExpr(expr: string, stateVarNames: Set<string>, localNames: Set<string>, stateEnumName: string, knownStateValues: string[]): string {
+function rewriteExpr(expr: string, stateVarNames: Set<string>, mapVarNames: Set<string>, localNames: Set<string>, stateEnumName: string, knownStateValues: string[]): string {
   function shouldPrefix(id: string): boolean {
     return stateVarNames.has(id) && !localNames.has(id);
   }
@@ -363,6 +368,14 @@ function rewriteExpr(expr: string, stateVarNames: Set<string>, localNames: Set<s
 
   // 5a: notIn -> !<map>.has(<key>)  (e.g. "t.id notIn transfers.keys" -> "!transfers.has(t.id)")
   ts = ts.replace(/(\S+)\s+notIn\s+(\S+)\.keys/g, '!$2.has($1)');
+  // 5a2: x in <map>.keys -> <map>.has(x)  (e.g. "t.from in accounts.keys" -> "accounts.has(t.from)")
+  ts = ts.replace(/(\S+)\s+in\s+(\S+)\.keys/g, '$2.has($1)');
+  // 5a3: x in <set> -> <set>.has(x)  (e.g. "id in pending" -> "pending.has(id)")
+  ts = ts.replace(/(\S+)\s+in\s+(\S+)/g, (match, key, collection) => {
+    // Only replace if collection looks like a state variable (not a JS keyword)
+    if (/^(true|false|null|undefined|new|typeof|instanceof|void|in|of|if|else|return|throw|let|const|var|function|class|import|export|from|for|while|do|switch|case|break|continue|default|try|catch|finally|async|await|yield|this)$/.test(collection)) return match;
+    return `${collection}.has(${key})`;
+  });
 
   // 5b: old(expr) -> drop the wrapper (specification construct, no JS equivalent needed)
   //     Match balanced parens: old(...). The inner expr can contain parens.
@@ -377,11 +390,22 @@ function rewriteExpr(expr: string, stateVarNames: Set<string>, localNames: Set<s
   ts = ts.replace(/(\S+)\s+\\\\\s+\{([^}]+)\}/g, 'new Set([...$1].filter(x => x !== $2))');
 
   // 5e: Clean up trailing empty comparisons (===) — expression has no RHS after old() removal
-  //     The template wraps as (!(expr)) — so trailing === becomes ===) in output.
-  //     We need to handle the === at end-of-string within the expression.
   //     "accounts[t.from].debits_posted ===" -> "accounts[t.from].debits_posted === accounts[t.from].debits_posted"
   ts = ts.replace(/(\S+)\s*===\s*$/g, '$1 === $1');
 
+  // 5f: Map access via bracket -> .get()  (e.g. "transfers[id]" -> "transfers.get(id)")
+  //     Only applies to state variables that are Map types
+  for (const mapVar of mapVarNames) {
+    // Match: mapVar[expr] where mapVar is a known Map state variable
+    // Handle both bare mapVar[...] and this.mapVar[...]
+    const barePattern = new RegExp('\\b(' + mapVar + ')\\[([^\\]]+)\\]', 'g');
+    ts = ts.replace(barePattern, '$1.get($2)');
+    const thisPattern = new RegExp('\\b(this\\.' + mapVar + ')\\[([^\\]]+)\\]', 'g');
+    ts = ts.replace(thisPattern, '$1.get($2)');
+  }
+  // 5g: .size() -> .size  (Set/Map size property, not a method in JS)
+  ts = ts.replace(/\.size\(\)/g, '.size');
+
   return ts.trim();
 }
 
diff --git a/compiler/test-output/RetryHandler.prov.jsonld b/compiler/test-output/RetryHandler.prov.jsonld
index e99a4da..0817433 100644
--- a/compiler/test-output/RetryHandler.prov.jsonld
+++ b/compiler/test-output/RetryHandler.prov.jsonld
@@ -12,7 +12,7 @@
         "@type": "prov:Generation",
         "prov:activity": {
           "@type": "prov:Activity",
-          "prov:startTime": "2026-05-05T10:11:33.422Z"
+          "prov:startTime": "2026-05-10T05:07:15.423Z"
         }
       },
       "rdfs:label": "RetryHandler",
diff --git a/compiler/test-output/RetryHandler.specbom.cdx.json b/compiler/test-output/RetryHandler.specbom.cdx.json
index 4216014..a691b56 100644
--- a/compiler/test-output/RetryHandler.specbom.cdx.json
+++ b/compiler/test-output/RetryHandler.specbom.cdx.json
@@ -38,7 +38,7 @@
         "name": "Scott Scoble",
         "email": "scott@scoble.me"
       },
-      "timestamp": "2026-05-05T10:11:33.425Z"
+      "timestamp": "2026-05-10T05:07:15.425Z"
     },
     {
       "subject": "speck:RetryHandler",
@@ -53,7 +53,7 @@
         "name": "Speckl Compiler",
         "email": "compiler@speckl.scoble.me"
       },
-      "timestamp": "2026-05-05T10:11:33.425Z"
+      "timestamp": "2026-05-10T05:07:15.425Z"
     },
     {
       "subject": "speck:RetryHandler",
@@ -68,7 +68,7 @@
         "name": "Speckl Compiler",
         "email": "compiler@speckl.scoble.me"
       },
-      "timestamp": "2026-05-05T10:11:33.425Z"
+      "timestamp": "2026-05-10T05:07:15.425Z"
     }
   ]
 }
\ No newline at end of file
diff --git a/compiler/test-output/RetryHandler.specbom.spdx.json b/compiler/test-output/RetryHandler.specbom.spdx.json
index 81b791e..48a83a5 100644
--- a/compiler/test-output/RetryHandler.specbom.spdx.json
+++ b/compiler/test-output/RetryHandler.specbom.spdx.json
@@ -13,7 +13,7 @@
     "spdxVersion": "3.0.1",
     "dataLicense": "CC0-1.0",
     "creationInfo": {
-      "created": "2026-05-05T10:11:33.426Z",
+      "created": "2026-05-10T05:07:15.426Z",
       "createdBy": [
         "Organization: Speckl",
         "tool: speckl-compile-0.2.0"
@@ -27,7 +27,7 @@
           "@type": "spdx:Tool",
           "name": "speckl-compile"
         },
-        "timestamp": "2026-05-05T10:11:33.426Z",
+        "timestamp": "2026-05-10T05:07:15.427Z",
         "comment": "Review type: manual"
       }
     ]
diff --git a/out/OAuth2AuthorizationCode.prov.jsonld b/out/OAuth2AuthorizationCode.prov.jsonld
new file mode 100644
index 0000000..7144d96
--- /dev/null
+++ b/out/OAuth2AuthorizationCode.prov.jsonld
@@ -0,0 +1,21 @@
+{
+  "@context": {
+    "prov": "http://www.w3.org/ns/prov#",
+    "speckl": "https://speckl.scoble.me/ns/v0.2#",
+    "rdfs": "http://www.w3.org/2000/01/rdf-schema#"
+  },
+  "@graph": [
+    {
+      "@type": "prov:Entity",
+      "@id": "speck:OAuth2AuthorizationCode",
+      "prov:qualifiedGeneration": {
+        "@type": "prov:Generation",
+        "prov:activity": {
+          "@type": "prov:Activity",
+          "prov:startTime": "2026-05-10T04:51:39.510Z"
+        }
+      },
+      "rdfs:label": "OAuth2AuthorizationCode"
+    }
+  ]
+}
\ No newline at end of file
diff --git a/out/OAuth2AuthorizationCode.specbom.cdx.json b/out/OAuth2AuthorizationCode.specbom.cdx.json
new file mode 100644
index 0000000..1d6ddc4
--- /dev/null
+++ b/out/OAuth2AuthorizationCode.specbom.cdx.json
@@ -0,0 +1,15 @@
+{
+  "bomFormat": "CycloneDX",
+  "specVersion": "1.6",
+  "components": [],
+  "metadata": {
+    "tools": [],
+    "component": {
+      "type": "application",
+      "name": "OAuth2AuthorizationCode",
+      "version": "0.2.0",
+      "properties": []
+    }
+  },
+  "annotations": []
+}
\ No newline at end of file
diff --git a/out/OAuth2AuthorizationCode.specbom.spdx.json b/out/OAuth2AuthorizationCode.specbom.spdx.json
new file mode 100644
index 0000000..97cdbb1
--- /dev/null
+++ b/out/OAuth2AuthorizationCode.specbom.spdx.json
@@ -0,0 +1,26 @@
+{
+  "@context": [
+    "https://spdx.github.io/spdx-v3/spdx-context.jsonld",
+    {
+      "speckl": "https://speckl.scoble.me/ns/v0.2#"
+    }
+  ],
+  "@type": "spdx:Document",
+  "spdx": {
+    "@id": "spdx:OAuth2AuthorizationCode",
+    "@type": "spdx:Snippet",
+    "name": "OAuth2AuthorizationCode",
+    "spdxVersion": "3.0.1",
+    "dataLicense": "CC0-1.0",
+    "creationInfo": {
+      "created": "2026-05-10T04:51:39.520Z",
+      "createdBy": [
+        "Organization: Speckl",
+        "tool: speckl-compile-0.2.0"
+      ]
+    }
+  },
+  "builtBy": [],
+  "relationships": [],
+  "elements": []
+}
\ No newline at end of file
diff --git a/out/OAuth2AuthorizationCode.ts b/out/OAuth2AuthorizationCode.ts
new file mode 100644
index 0000000..b108af7
--- /dev/null
+++ b/out/OAuth2AuthorizationCode.ts
@@ -0,0 +1,120 @@
+// Auto-generated by speckl-compile from OAuth2AuthorizationCode
+// DO NOT EDIT MANUALLY — regenerate from .speckdl source
+
+export const OAuth2AuthorizationCodeState = {
+  Open: 'open',
+  Closed: 'closed',
+} as const;
+export type OAuth2AuthorizationCodeState = typeof OAuth2AuthorizationCodeState[keyof typeof OAuth2AuthorizationCodeState];
+
+
+
+
+export class OAuth2AuthorizationCodeMachine {
+  clients: Map<ClientId, { redirect_uris: Set<RedirectUri>; client_secret: ClientSecret }>;
+  authorizationCodes: Map(AuthorizationCode, {;
+  client_id: ClientId;
+  redirect_uri: RedirectUri;
+  state: OAuth2AuthorizationCodeState;
+  code_challenge: CodeChallenge;
+  code_challenge_method: String;
+  scope: Scope;
+  user_id: UserId;
+  session_id: SessionId;
+  created_at: number;
+  used: boolean;
+  accessTokens: Map(AccessToken, {;
+  client_id: ClientId;
+  user_id: UserId;
+  scope: Scope;
+  expires_at: number;
+  session_id: SessionId;
+  refresh_token: RefreshToken;
+  refreshTokens: Map(RefreshToken, {;
+  client_id: ClientId;
+  user_id: UserId;
+  scope: Scope;
+  access_token: AccessToken;
+  created_at: number;
+  sessions: Map<SessionId, { user_id: UserId }>;
+  stateNonces: Map<OAuth2AuthorizationCodeState, { client_id: ClientId; redirect_uri: RedirectUri }>;
+  pkceChallenges: Map<CodeChallenge, { code_verifier_hash: string; method: string }>;
+  currentTime: number;
+  decisionLog: any[] = [];
+
+  constructor() {
+    this.clients = new Map();
+    this.used = false;
+    this.created_at = 0;
+    this.sessions = new Map();
+    this.stateNonces = new Map();
+    this.pkceChallenges = new Map();
+    this.currentTime = 0;
+  }
+
+  Authorize(client: ClientId, redirectUri: RedirectUri, scope: Scope, userId: UserId, sessionId: SessionId) {
+    if (!(this.clients.has(client))) throw new Error('Guard failed: this.clients.has(client)');
+    if (!(this.clients.has(redirectUri).client.redirect_uris)) throw new Error('Guard failed: this.clients.has(redirectUri).client.redirect_uris');
+    if (!(this.sessions.has(sessionId))) throw new Error('Guard failed: this.sessions.has(sessionId)');
+    if (!(this.sessions.get(sessionId)!.user_id == userId)) throw new Error('Guard failed: this.sessions.get(sessionId)!.user_id == userId');
+    this.stateNonces[state] = { this.client_id: client, this.redirect_uri: redirectUri };
+    this.pkceChallenges[codeChallenge] = { code_verifier_hash: hash(codeVerifier, "S256"), method: "S256" };
+    this.authorizationCodes[authCode] = {;
+  }
+
+  ApproveAuthorization(code: AuthorizationCode, userId: UserId) {
+    if (!(this.authorizationCodes.has(code))) throw new Error('Guard failed: this.authorizationCodes.has(code)');
+    if (!(c.this.user_id == userId)) throw new Error('Guard failed: c.this.user_id == userId');
+    if (!(c.this.used == false)) throw new Error('Guard failed: c.this.used == false');
+  }
+
+  ExchangeCode(req: TokenRequest) {
+    if (!(this.clients.has(req.this.client_id))) throw new Error('Guard failed: this.clients.has(req.this.client_id)');
+    if (!(this.authorizationCodes.has(req.code))) throw new Error('Guard failed: this.authorizationCodes.has(req.code)');
+    if (!(c.this.used == false)) throw new Error('Guard failed: c.this.used == false');
+    if (!(c.this.client_id == req.this.client_id)) throw new Error('Guard failed: c.this.client_id == req.this.client_id');
+    if (!(c.this.redirect_uri == req.this.redirect_uri)) throw new Error('Guard failed: c.this.redirect_uri == req.this.redirect_uri');
+    if (!(expectedChallenge == c.this.code_challenge)) throw new Error('Guard failed: expectedChallenge == c.this.code_challenge');
+    this.pkceChallenges[c.code_challenge] = null;
+    this.stateNonces[c.state] = null;
+    this.accessTokens[accessToken] = {;
+    this.refreshTokens[refreshToken] = {;
+  }
+
+  RefreshToken(req: RefreshRequest) {
+    if (!(this.clients.has(req.this.client_id))) throw new Error('Guard failed: this.clients.has(req.this.client_id)');
+    if (!(this.refreshTokens.has(req.this.refresh_token))) throw new Error('Guard failed: this.refreshTokens.has(req.this.refresh_token)');
+    if (!(r.this.client_id == req.this.client_id)) throw new Error('Guard failed: r.this.client_id == req.this.client_id');
+    this.accessTokens[r.access_token] = null;
+    this.accessTokens[newAccessToken] = {;
+    this.refreshTokens[newRefreshToken] = {;
+    this.refreshTokens[req.refresh_token] = null;
+  }
+
+  RevokeToken(client: ClientId, token: string, tokenType: string) {
+    if (!(this.clients.has(client))) throw new Error('Guard failed: this.clients.has(client)');
+    if (!(this.accessTokens.has(token))) throw new Error('Guard failed: this.accessTokens.has(token)');
+    if (!(t.this.client_id == client)) throw new Error('Guard failed: t.this.client_id == client');
+    if (!(this.refreshTokens.has(token))) throw new Error('Guard failed: this.refreshTokens.has(token)');
+    if (!(r.this.client_id == client)) throw new Error('Guard failed: r.this.client_id == client');
+    this.accessTokens[token] = null;
+    this.refreshTokens[t.refresh_token] = null;
+    this.refreshTokens[token] = null;
+    this.accessTokens[r.access_token] = null;
+  }
+
+  VerifyPKCE(code: AuthorizationCode, verifier: CodeVerifier) {
+    if (!(this.authorizationCodes.has(code))) throw new Error('Guard failed: this.authorizationCodes.has(code)');
+    if (!(c.this.used == false)) throw new Error('Guard failed: c.this.used == false');
+    if (!(expectedChallenge == c.this.code_challenge)) throw new Error('Guard failed: expectedChallenge == c.this.code_challenge');
+  }
+
+
+
+  // V1: Always(NoTokenLeakage)
+  async verify1(): Promise<boolean> {
+    // TODO: Model-check or monitor
+    // Temporal: Always(NoTokenLeakage)
+    return true;
+  }
+}
diff --git a/out/OAuth2AuthorizationCode.wat b/out/OAuth2AuthorizationCode.wat
new file mode 100644
index 0000000..844f3fc
--- /dev/null
+++ b/out/OAuth2AuthorizationCode.wat
@@ -0,0 +1,211 @@
+;; Auto-generated by speckl-compile from OAuth2AuthorizationCode
+;; Compile: wat2wasm OAuth2AuthorizationCode.wat -o OAuth2AuthorizationCode.wasm
+
+(module
+  ;; Host imports for Map/Set/alloc
+  (import "speckl" "map_create" (func $map_create (result i32)))
+  (import "speckl" "map_set" (func $map_set (param i32 i32 i32)))
+  (import "speckl" "map_get" (func $map_get (param i32 i32) (result i32)))
+  (import "speckl" "map_has" (func $map_has (param i32 i32) (result i32)))
+  (import "speckl" "map_remove" (func $map_remove (param i32 i32)))
+  (import "speckl" "set_create" (func $set_create (result i32)))
+  (import "speckl" "set_add" (func $set_add (param i32 i32)))
+  (import "speckl" "set_has" (func $set_has (param i32 i32) (result i32)))
+  (import "speckl" "set_size" (func $set_size (param i32) (result i32)))
+  (import "speckl" "alloc" (func $alloc (param i32) (result i32)))
+  (import "speckl" "write_i32" (func $write_i32 (param i32 i32)))
+  (import "speckl" "write_f64" (func $write_f64 (param i32 f64)))
+
+  ;; Linear memory (exported so host can read state)
+  (memory (export "memory") 1)
+
+  ;; State globals
+  
+
+  ;; ---- init ----
+  (func $init (export "init")
+    
+  )
+
+  ;; ---- Actions ----
+    ;; action: Authorize
+  (func $Authorize (export "Authorize") (param $client i32) (param $redirectUri i32) (param $scope i32) (param $userId i32) (param $sessionId i32) (result i32)
+    
+    (local $state i32)
+    (local $codeVerifier i32)
+    (local $codeChallenge i32)
+    (local $authCode i32)
+    ;; require: client in clients.keys
+    ;; Complex guard not compiled: client in clients.keys
+    ;; require: redirectUri in clients.client.redirect_uris
+    ;; Complex guard not compiled: redirectUri in clients.client.redirect_uris
+    ;; require: sessionId in sessions.keys
+    ;; Complex guard not compiled: sessionId in sessions.keys
+    ;; require: sessions[sessionId].user_id == userId
+    ;; Complex guard not compiled: sessions[sessionId].user_id == userId
+    (i32.const 0) ;; uncompiled expr: "state_" + hash(client + redirectUri + currentTime)
+    (local.set $state)
+    (i32.const 0) ;; uncompiled expr: "verifier_" + hash(client + userId + currentTime)
+    (local.set $codeVerifier)
+    (i32.const 0) ;; uncompiled expr: hash(codeVerifier, "S256")
+    (local.set $codeChallenge)
+    ;; stateNonces[state] := { client_id: client, redirect_uri: redirectUri }
+    ;; Unrecognized assignment target: stateNonces[state]
+    ;; pkceChallenges[codeChallenge] := { code_verifier_hash: hash(codeVerifier, "S256"), method: "S256" }
+    ;; Unrecognized assignment target: pkceChallenges[codeChallenge]
+    (i32.const 0) ;; uncompiled expr: "code_" + hash(client + userId + currentTime)
+    (local.set $authCode)
+    ;; authorizationCodes[authCode] := {
+    ;; Unrecognized assignment target: authorizationCodes[authCode]
+    (i32.const 1)
+  )
+
+  ;; action: ApproveAuthorization
+  (func $ApproveAuthorization (export "ApproveAuthorization") (param $code i32) (param $userId i32) (result i32)
+    
+    (local $c i32)
+    ;; require: code in authorizationCodes.keys
+    ;; Complex guard not compiled: code in authorizationCodes.keys
+    (i32.const 0) ;; uncompiled expr: authorizationCodes[code]
+    (local.set $c)
+    ;; require: c.user_id == userId
+    ;; Complex guard not compiled: c.user_id == userId
+    ;; require: c.used == false
+    ;; Complex guard not compiled: c.used == false
+    (i32.const 1)
+  )
+
+  ;; action: ExchangeCode
+  (func $ExchangeCode (export "ExchangeCode") (param $req i32) (result i32)
+    
+    (local $c i32)
+    (local $expectedChallenge i32)
+    (local $accessToken i32)
+    (local $refreshToken i32)
+    (local $expiresAt i32)
+    ;; require: req.client_id in clients.keys
+    ;; Complex guard not compiled: req.client_id in clients.keys
+    ;; require: req.code in authorizationCodes.keys
+    ;; Complex guard not compiled: req.code in authorizationCodes.keys
+    (i32.const 0) ;; uncompiled expr: authorizationCodes[req.code]
+    (local.set $c)
+    ;; require: c.used == false
+    ;; Complex guard not compiled: c.used == false
+    ;; require: c.client_id == req.client_id
+    ;; Complex guard not compiled: c.client_id == req.client_id
+    ;; require: c.redirect_uri == req.redirect_uri
+    ;; Complex guard not compiled: c.redirect_uri == req.redirect_uri
+    (i32.const 0) ;; uncompiled expr: hash(req.code_verifier, c.code_challenge_method)
+    (local.set $expectedChallenge)
+    ;; require: expectedChallenge == c.code_challenge
+    ;; Guard on non-scalar not compiled: expectedChallenge == c.code_challenge
+    ;; pkceChallenges[c.code_challenge] := null
+    ;; Unrecognized assignment target: pkceChallenges[c.code_challenge]
+    ;; stateNonces[c.state] := null
+    ;; Unrecognized assignment target: stateNonces[c.state]
+    (i32.const 0) ;; uncompiled expr: "access_" + hash(req.client_id + c.user_id + currentTime)
+    (local.set $accessToken)
+    (i32.const 0) ;; uncompiled expr: "refresh_" + hash(req.client_id + c.user_id + currentTime)
+    (local.set $refreshToken)
+    (i32.add (i32.const NaN) (i32.const 3600))
+    (local.set $expiresAt)
+    ;; accessTokens[accessToken] := {
+    ;; Unrecognized assignment target: accessTokens[accessToken]
+    ;; refreshTokens[refreshToken] := {
+    ;; Unrecognized assignment target: refreshTokens[refreshToken]
+    (i32.const 1)
+  )
+
+  ;; action: RefreshToken
+  (func $RefreshToken (export "RefreshToken") (param $req i32) (result i32)
+    
+    (local $r i32)
+    (local $newAccessToken i32)
+    (local $newRefreshToken i32)
+    (local $expiresAt i32)
+    ;; require: req.client_id in clients.keys
+    ;; Complex guard not compiled: req.client_id in clients.keys
+    ;; require: req.refresh_token in refreshTokens.keys
+    ;; Complex guard not compiled: req.refresh_token in refreshTokens.keys
+    (i32.const 0) ;; uncompiled expr: refreshTokens[req.refresh_token]
+    (local.set $r)
+    ;; require: r.client_id == req.client_id
+    ;; Complex guard not compiled: r.client_id == req.client_id
+    ;; accessTokens[r.access_token] := null
+    ;; Unrecognized assignment target: accessTokens[r.access_token]
+    (i32.const 0) ;; uncompiled expr: "access_" + hash(req.client_id + r.user_id + currentTime)
+    (local.set $newAccessToken)
+    (i32.const 0) ;; uncompiled expr: "refresh_" + hash(req.client_id + r.user_id + currentTime)
+    (local.set $newRefreshToken)
+    (i32.add (i32.const NaN) (i32.const 3600))
+    (local.set $expiresAt)
+    ;; accessTokens[newAccessToken] := {
+    ;; Unrecognized assignment target: accessTokens[newAccessToken]
+    ;; refreshTokens[newRefreshToken] := {
+    ;; Unrecognized assignment target: refreshTokens[newRefreshToken]
+    ;; refreshTokens[req.refresh_token] := null
+    ;; Unrecognized assignment target: refreshTokens[req.refresh_token]
+    (i32.const 1)
+  )
+
+  ;; action: RevokeToken
+  (func $RevokeToken (export "RevokeToken") (param $client i32) (param $token i32) (param $tokenType i32) (result i32)
+    
+    (local $t i32)
+    (local $r i32)
+    ;; require: client in clients.keys
+    ;; Complex guard not compiled: client in clients.keys
+    ;; require: token in accessTokens.keys
+    ;; Complex guard not compiled: token in accessTokens.keys
+    (i32.const 0) ;; uncompiled expr: accessTokens[token]
+    (local.set $t)
+    ;; require: t.client_id == client
+    ;; Complex guard not compiled: t.client_id == client
+    ;; accessTokens[token] := null
+    ;; Unrecognized assignment target: accessTokens[token]
+    ;; refreshTokens[t.refresh_token] := null
+    ;; Unrecognized assignment target: refreshTokens[t.refresh_token]
+    ;; require: token in refreshTokens.keys
+    ;; Complex guard not compiled: token in refreshTokens.keys
+    (i32.const 0) ;; uncompiled expr: refreshTokens[token]
+    (local.set $r)
+    ;; require: r.client_id == client
+    ;; Complex guard not compiled: r.client_id == client
+    ;; refreshTokens[token] := null
+    ;; Unrecognized assignment target: refreshTokens[token]
+    ;; accessTokens[r.access_token] := null
+    ;; Unrecognized assignment target: accessTokens[r.access_token]
+    (i32.const 1)
+  )
+
+  ;; action: VerifyPKCE
+  (func $VerifyPKCE (export "VerifyPKCE") (param $code i32) (param $verifier i32) (result i32)
+    
+    (local $c i32)
+    (local $expectedChallenge i32)
+    ;; require: code in authorizationCodes.keys
+    ;; Complex guard not compiled: code in authorizationCodes.keys
+    (i32.const 0) ;; uncompiled expr: authorizationCodes[code]
+    (local.set $c)
+    ;; require: c.used == false
+    ;; Complex guard not compiled: c.used == false
+    (i32.const 0) ;; uncompiled expr: hash(verifier, c.code_challenge_method)
+    (local.set $expectedChallenge)
+    ;; require: expectedChallenge == c.code_challenge
+    ;; Guard on non-scalar not compiled: expectedChallenge == c.code_challenge
+    (i32.const 1)
+  )
+
+  ;; ---- getState ----
+  (func $getState (export "getState") (result i32 i32)
+    (i32.const 0)
+    (i32.const 0)
+  )
+
+  
+  ;; checkConstraints — runtime constraint evaluation stub
+  (func $checkConstraints (export "checkConstraints") (result i32)
+    ;; TODO: evaluate constraint expressions at runtime
+    (i32.const 1)
+  )
+)
\ No newline at end of file
diff --git a/out/TigerBeetleLedger.prov.jsonld b/out/TigerBeetleLedger.prov.jsonld
new file mode 100644
index 0000000..0771fee
--- /dev/null
+++ b/out/TigerBeetleLedger.prov.jsonld
@@ -0,0 +1,21 @@
+{
+  "@context": {
+    "prov": "http://www.w3.org/ns/prov#",
+    "speckl": "https://speckl.scoble.me/ns/v0.2#",
+    "rdfs": "http://www.w3.org/2000/01/rdf-schema#"
+  },
+  "@graph": [
+    {
+      "@type": "prov:Entity",
+      "@id": "speck:TigerBeetleLedger",
+      "prov:qualifiedGeneration": {
+        "@type": "prov:Generation",
+        "prov:activity": {
+          "@type": "prov:Activity",
+          "prov:startTime": "2026-05-10T05:07:04.778Z"
+        }
+      },
+      "rdfs:label": "TigerBeetleLedger"
+    }
+  ]
+}
\ No newline at end of file
diff --git a/out/TigerBeetleLedger.specbom.cdx.json b/out/TigerBeetleLedger.specbom.cdx.json
new file mode 100644
index 0000000..8f5f7d0
--- /dev/null
+++ b/out/TigerBeetleLedger.specbom.cdx.json
@@ -0,0 +1,15 @@
+{
+  "bomFormat": "CycloneDX",
+  "specVersion": "1.6",
+  "components": [],
+  "metadata": {
+    "tools": [],
+    "component": {
+      "type": "application",
+      "name": "TigerBeetleLedger",
+      "version": "0.2.0",
+      "properties": []
+    }
+  },
+  "annotations": []
+}
\ No newline at end of file
diff --git a/out/TigerBeetleLedger.specbom.spdx.json b/out/TigerBeetleLedger.specbom.spdx.json
new file mode 100644
index 0000000..5541ede
--- /dev/null
+++ b/out/TigerBeetleLedger.specbom.spdx.json
@@ -0,0 +1,26 @@
+{
+  "@context": [
+    "https://spdx.github.io/spdx-v3/spdx-context.jsonld",
+    {
+      "speckl": "https://speckl.scoble.me/ns/v0.2#"
+    }
+  ],
+  "@type": "spdx:Document",
+  "spdx": {
+    "@id": "spdx:TigerBeetleLedger",
+    "@type": "spdx:Snippet",
+    "name": "TigerBeetleLedger",
+    "spdxVersion": "3.0.1",
+    "dataLicense": "CC0-1.0",
+    "creationInfo": {
+      "created": "2026-05-10T05:07:04.787Z",
+      "createdBy": [
+        "Organization: Speckl",
+        "tool: speckl-compile-0.2.0"
+      ]
+    }
+  },
+  "builtBy": [],
+  "relationships": [],
+  "elements": []
+}
\ No newline at end of file
diff --git a/out/TigerBeetleLedger.ts b/out/TigerBeetleLedger.ts
new file mode 100644
index 0000000..fee25fc
--- /dev/null
+++ b/out/TigerBeetleLedger.ts
@@ -0,0 +1,143 @@
+// Auto-generated by speckl-compile from TigerBeetleLedger
+// DO NOT EDIT MANUALLY — regenerate from .speckdl source
+
+export const TigerBeetleLedgerState = {
+  Open: 'open',
+  Closed: 'closed',
+} as const;
+export type TigerBeetleLedgerState = typeof TigerBeetleLedgerState[keyof typeof TigerBeetleLedgerState];
+
+
+
+
+export class TigerBeetleLedgerMachine {
+  accounts: Map<number, Account>;
+  transfers: Map<number, Transfer>;
+  pending: Set<number>;
+  replicaState: Map<number, Replica>;
+  log: LogEntry[];
+  commitIndex: number;
+  leader: number;
+  decisionLog: any[] = [];
+
+  constructor() {
+    // No init block defined
+  }
+
+  CreateTransfer(t: Transfer) {
+    // precondition: !this.transfers.has(t.id)
+    if (!(!this.transfers.has(t.id))) throw new Error('Precondition failed: !this.transfers.has(t.id)');
+    // precondition: this.accounts.has(t.from)
+    if (!(this.accounts.has(t.from))) throw new Error('Precondition failed: this.accounts.has(t.from)');
+    // precondition: this.accounts.has(t.to)
+    if (!(this.accounts.has(t.to))) throw new Error('Precondition failed: this.accounts.has(t.to)');
+    // precondition: t.from != t.to
+    if (!(t.from != t.to)) throw new Error('Precondition failed: t.from != t.to');
+    // precondition: this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft
+    if (!(this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft)) throw new Error('Precondition failed: this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft');
+    // postcondition: this.transfers.get(t.id) == t
+    if (!(this.transfers.get(t.id) == t)) throw new Error('Postcondition failed: this.transfers.get(t.id) == t');
+    // postcondition: this.pending == new Set([...this.pending, t.id])
+    if (!(this.pending == new Set([...this.pending, t.id]))) throw new Error('Postcondition failed: this.pending == new Set([...this.pending, t.id])');
+    // postcondition: this.accounts.get(t.from).debits_pending == this.accounts.get(t.from).debits_pending + t.amount
+    if (!(this.accounts.get(t.from).debits_pending == this.accounts.get(t.from).debits_pending + t.amount)) throw new Error('Postcondition failed: this.accounts.get(t.from).debits_pending == this.accounts.get(t.from).debits_pending + t.amount');
+    // postcondition: this.accounts.get(t.to).credits_pending == this.accounts.get(t.to).credits_pending + t.amount
+    if (!(this.accounts.get(t.to).credits_pending == this.accounts.get(t.to).credits_pending + t.amount)) throw new Error('Postcondition failed: this.accounts.get(t.to).credits_pending == this.accounts.get(t.to).credits_pending + t.amount');
+  }
+
+  CommitTransfer(id: number) {
+    // precondition: this.pending.has(id)
+    if (!(this.pending.has(id))) throw new Error('Precondition failed: this.pending.has(id)');
+    // precondition: this.transfers.has(id)
+    if (!(this.transfers.has(id))) throw new Error('Precondition failed: this.transfers.has(id)');
+    // precondition: this.transfers.get(id).pending == true
+    if (!(this.transfers.get(id).pending == true)) throw new Error('Precondition failed: this.transfers.get(id).pending == true');
+    // postcondition: this.pending == new Set([...this.pending].filter(x => x !== id))
+    if (!(this.pending == new Set([...this.pending].filter(x => x !== id)))) throw new Error('Postcondition failed: this.pending == new Set([...this.pending].filter(x => x !== id))');
+    // postcondition: this.transfers.get(id).pending == false
+    if (!(this.transfers.get(id).pending == false)) throw new Error('Postcondition failed: this.transfers.get(id).pending == false');
+    // postcondition: this.transfers.get(id).posted == true
+    if (!(this.transfers.get(id).posted == true)) throw new Error('Postcondition failed: this.transfers.get(id).posted == true');
+    // postcondition: this.accounts.get(this.transfers.get(id).from).debits_posted === this.accounts.get(this.transfers.get(id).from).debits_posted
+    if (!(this.accounts.get(this.transfers.get(id).from).debits_posted === this.accounts.get(this.transfers.get(id).from).debits_posted)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).from).debits_posted === this.accounts.get(this.transfers.get(id).from).debits_posted');
+    // postcondition: this.accounts.get(this.transfers.get(id).to).credits_posted === this.accounts.get(this.transfers.get(id).to).credits_posted
+    if (!(this.accounts.get(this.transfers.get(id).to).credits_posted === this.accounts.get(this.transfers.get(id).to).credits_posted)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).to).credits_posted === this.accounts.get(this.transfers.get(id).to).credits_posted');
+    // postcondition: this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending
+    if (!(this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending');
+    // postcondition: this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending
+    if (!(this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending');
+  }
+
+  VoidTransfer(id: number) {
+    // precondition: this.pending.has(id)
+    if (!(this.pending.has(id))) throw new Error('Precondition failed: this.pending.has(id)');
+    // precondition: this.transfers.has(id)
+    if (!(this.transfers.has(id))) throw new Error('Precondition failed: this.transfers.has(id)');
+    // precondition: this.transfers.get(id).pending == true
+    if (!(this.transfers.get(id).pending == true)) throw new Error('Precondition failed: this.transfers.get(id).pending == true');
+    // postcondition: this.pending == new Set([...this.pending].filter(x => x !== id))
+    if (!(this.pending == new Set([...this.pending].filter(x => x !== id)))) throw new Error('Postcondition failed: this.pending == new Set([...this.pending].filter(x => x !== id))');
+    // postcondition: this.transfers.get(id).pending == false
+    if (!(this.transfers.get(id).pending == false)) throw new Error('Postcondition failed: this.transfers.get(id).pending == false');
+    // postcondition: this.transfers.get(id).voided == true
+    if (!(this.transfers.get(id).voided == true)) throw new Error('Postcondition failed: this.transfers.get(id).voided == true');
+    // postcondition: this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending
+    if (!(this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending');
+    // postcondition: this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending
+    if (!(this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending');
+  }
+
+  PostTransfer(t: Transfer) {
+    // precondition: !this.transfers.has(t.id)
+    if (!(!this.transfers.has(t.id))) throw new Error('Precondition failed: !this.transfers.has(t.id)');
+    // precondition: this.accounts.has(t.from)
+    if (!(this.accounts.has(t.from))) throw new Error('Precondition failed: this.accounts.has(t.from)');
+    // precondition: this.accounts.has(t.to)
+    if (!(this.accounts.has(t.to))) throw new Error('Precondition failed: this.accounts.has(t.to)');
+    // precondition: t.from != t.to
+    if (!(t.from != t.to)) throw new Error('Precondition failed: t.from != t.to');
+    // precondition: this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft
+    if (!(this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft)) throw new Error('Precondition failed: this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft');
+    // postcondition: this.transfers.get(t.id) == { ...t, pending: false, posted: true, voided: false }
+    if (!(this.transfers.get(t.id) == { ...t, pending: false, posted: true, voided: false })) throw new Error('Postcondition failed: this.transfers.get(t.id) == { ...t, pending: false, posted: true, voided: false }');
+    // postcondition: this.accounts.get(t.from).debits_posted == this.accounts.get(t.from).debits_posted + t.amount
+    if (!(this.accounts.get(t.from).debits_posted == this.accounts.get(t.from).debits_posted + t.amount)) throw new Error('Postcondition failed: this.accounts.get(t.from).debits_posted == this.accounts.get(t.from).debits_posted + t.amount');
+    // postcondition: this.accounts.get(t.to).credits_posted == this.accounts.get(t.to).credits_posted + t.amount
+    if (!(this.accounts.get(t.to).credits_posted == this.accounts.get(t.to).credits_posted + t.amount)) throw new Error('Postcondition failed: this.accounts.get(t.to).credits_posted == this.accounts.get(t.to).credits_posted + t.amount');
+  }
+
+  BecomeLeader(replica: number, term: number) {
+    // precondition: this.replicaState.has(replica)
+    if (!(this.replicaState.has(replica))) throw new Error('Precondition failed: this.replicaState.has(replica)');
+    // precondition: this.replicaState.get(replica).role == "candidate"
+    if (!(this.replicaState.get(replica).role == "candidate")) throw new Error('Precondition failed: this.replicaState.get(replica).role == "candidate"');
+    // precondition: this.replicaState.get(replica).currentTerm < term
+    if (!(this.replicaState.get(replica).currentTerm < term)) throw new Error('Precondition failed: this.replicaState.get(replica).currentTerm < term');
+    // postcondition: this.leader == replica
+    if (!(this.leader == replica)) throw new Error('Postcondition failed: this.leader == replica');
+    // postcondition: this.replicaState.get(replica).role == "this.leader"
+    if (!(this.replicaState.get(replica).role == "this.leader")) throw new Error('Postcondition failed: this.replicaState.get(replica).role == "this.leader"');
+    // postcondition: this.replicaState.get(replica).currentTerm == term
+    if (!(this.replicaState.get(replica).currentTerm == term)) throw new Error('Postcondition failed: this.replicaState.get(replica).currentTerm == term');
+  }
+
+  AppendEntry(entry: LogEntry, term: number) {
+    // precondition: entry.index == length(this.log) + 1
+    if (!(entry.index == length(this.log) + 1)) throw new Error('Precondition failed: entry.index == length(this.log) + 1');
+    // precondition: term >= this.commitIndex
+    if (!(term >= this.commitIndex)) throw new Error('Precondition failed: term >= this.commitIndex');
+    // postcondition: this.log == append(this.log, entry)
+    if (!(this.log == append(this.log, entry))) throw new Error('Postcondition failed: this.log == append(this.log, entry)');
+    // postcondition: this.commitIndex == entry.index
+    if (!(this.commitIndex == entry.index)) throw new Error('Postcondition failed: this.commitIndex == entry.index');
+  }
+
+
+
+  // V1: Always(AccountBalanceInvariant)
+  async verify1(): Promise<boolean> {
+    // TODO: Model-check or monitor
+    // Temporal: Always(AccountBalanceInvariant)
+    return true;
+  }
+}
diff --git a/out/TigerBeetleLedger.wat b/out/TigerBeetleLedger.wat
new file mode 100644
index 0000000..6555562
--- /dev/null
+++ b/out/TigerBeetleLedger.wat
@@ -0,0 +1,102 @@
+;; Auto-generated by speckl-compile from TigerBeetleLedger
+;; Compile: wat2wasm TigerBeetleLedger.wat -o TigerBeetleLedger.wasm
+
+(module
+  ;; Host imports for Map/Set/alloc
+  (import "speckl" "map_create" (func $map_create (result i32)))
+  (import "speckl" "map_set" (func $map_set (param i32 i32 i32)))
+  (import "speckl" "map_get" (func $map_get (param i32 i32) (result i32)))
+  (import "speckl" "map_has" (func $map_has (param i32 i32) (result i32)))
+  (import "speckl" "map_remove" (func $map_remove (param i32 i32)))
+  (import "speckl" "set_create" (func $set_create (result i32)))
+  (import "speckl" "set_add" (func $set_add (param i32 i32)))
+  (import "speckl" "set_has" (func $set_has (param i32 i32) (result i32)))
+  (import "speckl" "set_size" (func $set_size (param i32) (result i32)))
+  (import "speckl" "alloc" (func $alloc (param i32) (result i32)))
+  (import "speckl" "write_i32" (func $write_i32 (param i32 i32)))
+  (import "speckl" "write_f64" (func $write_f64 (param i32 f64)))
+
+  ;; Linear memory (exported so host can read state)
+  (memory (export "memory") 1)
+
+  ;; State globals
+  (global $accounts (mut i32) (i32.const 0))
+(global $transfers (mut i32) (i32.const 0))
+(global $pending (mut i32) (i32.const 0))
+(global $replicaState (mut i32) (i32.const 0))
+(global $log (mut i32) (i32.const 0))
+(global $commitIndex (mut i32) (i32.const 0))
+(global $leader (mut i32) (i32.const 0))
+
+  ;; ---- init ----
+  (func $init (export "init")
+    (call $map_create)
+    (global.set $accounts)
+    (call $map_create)
+    (global.set $transfers)
+    (call $set_create)
+    (global.set $pending)
+    (call $map_create)
+    (global.set $replicaState)
+    (i32.const 0)
+    (global.set $commitIndex)
+    (i32.const 0)
+    (global.set $leader)
+  )
+
+  ;; ---- Actions ----
+    ;; action: CreateTransfer
+  (func $CreateTransfer (export "CreateTransfer") (param $t i32) (result i32)
+    
+    (i32.const 1)
+  )
+
+  ;; action: CommitTransfer
+  (func $CommitTransfer (export "CommitTransfer") (param $id i32) (result i32)
+    
+    (i32.const 1)
+  )
+
+  ;; action: VoidTransfer
+  (func $VoidTransfer (export "VoidTransfer") (param $id i32) (result i32)
+    
+    (i32.const 1)
+  )
+
+  ;; action: PostTransfer
+  (func $PostTransfer (export "PostTransfer") (param $t i32) (result i32)
+    
+    (i32.const 1)
+  )
+
+  ;; action: BecomeLeader
+  (func $BecomeLeader (export "BecomeLeader") (param $replica i32) (param $term i32) (result i32)
+    
+    (i32.const 1)
+  )
+
+  ;; action: AppendEntry
+  (func $AppendEntry (export "AppendEntry") (param $entry i32) (param $term i32) (result i32)
+    
+    (i32.const 1)
+  )
+
+  ;; ---- getState ----
+  (func $getState (export "getState") (result i32 i32)
+    (i32.const 0)
+    (global.get $commitIndex)
+    (i32.store)
+    (i32.const 4)
+    (global.get $leader)
+    (i32.store)
+    (i32.const 0)
+    (i32.const 8)
+  )
+
+  
+  ;; checkConstraints — runtime constraint evaluation stub
+  (func $checkConstraints (export "checkConstraints") (result i32)
+    ;; TODO: evaluate constraint expressions at runtime
+    (i32.const 1)
+  )
+)
\ No newline at end of file
diff --git a/out/ToggleSwitch.prov.jsonld b/out/ToggleSwitch.prov.jsonld
new file mode 100644
index 0000000..3e8e779
--- /dev/null
+++ b/out/ToggleSwitch.prov.jsonld
@@ -0,0 +1,21 @@
+{
+  "@context": {
+    "prov": "http://www.w3.org/ns/prov#",
+    "speckl": "https://speckl.scoble.me/ns/v0.2#",
+    "rdfs": "http://www.w3.org/2000/01/rdf-schema#"
+  },
+  "@graph": [
+    {
+      "@type": "prov:Entity",
+      "@id": "speck:ToggleSwitch",
+      "prov:qualifiedGeneration": {
+        "@type": "prov:Generation",
+        "prov:activity": {
+          "@type": "prov:Activity",
+          "prov:startTime": "2026-05-10T05:04:07.209Z"
+        }
+      },
+      "rdfs:label": "ToggleSwitch"
+    }
+  ]
+}
\ No newline at end of file
diff --git a/out/ToggleSwitch.specbom.cdx.json b/out/ToggleSwitch.specbom.cdx.json
new file mode 100644
index 0000000..0a54d18
--- /dev/null
+++ b/out/ToggleSwitch.specbom.cdx.json
@@ -0,0 +1,15 @@
+{
+  "bomFormat": "CycloneDX",
+  "specVersion": "1.6",
+  "components": [],
+  "metadata": {
+    "tools": [],
+    "component": {
+      "type": "application",
+      "name": "ToggleSwitch",
+      "version": "0.2.0",
+      "properties": []
+    }
+  },
+  "annotations": []
+}
\ No newline at end of file
diff --git a/out/ToggleSwitch.specbom.spdx.json b/out/ToggleSwitch.specbom.spdx.json
new file mode 100644
index 0000000..be9bd34
--- /dev/null
+++ b/out/ToggleSwitch.specbom.spdx.json
@@ -0,0 +1,26 @@
+{
+  "@context": [
+    "https://spdx.github.io/spdx-v3/spdx-context.jsonld",
+    {
+      "speckl": "https://speckl.scoble.me/ns/v0.2#"
+    }
+  ],
+  "@type": "spdx:Document",
+  "spdx": {
+    "@id": "spdx:ToggleSwitch",
+    "@type": "spdx:Snippet",
+    "name": "ToggleSwitch",
+    "spdxVersion": "3.0.1",
+    "dataLicense": "CC0-1.0",
+    "creationInfo": {
+      "created": "2026-05-10T05:04:07.215Z",
+      "createdBy": [
+        "Organization: Speckl",
+        "tool: speckl-compile-0.2.0"
+      ]
+    }
+  },
+  "builtBy": [],
+  "relationships": [],
+  "elements": []
+}
\ No newline at end of file
diff --git a/out/ToggleSwitch.ts b/out/ToggleSwitch.ts
new file mode 100644
index 0000000..5f86204
--- /dev/null
+++ b/out/ToggleSwitch.ts
@@ -0,0 +1,34 @@
+// Auto-generated by speckl-compile from ToggleSwitch
+// DO NOT EDIT MANUALLY — regenerate from .speckdl source
+
+export const ToggleSwitchState = {
+  Open: 'open',
+  Closed: 'closed',
+} as const;
+export type ToggleSwitchState = typeof ToggleSwitchState[keyof typeof ToggleSwitchState];
+
+
+
+
+export class ToggleSwitchMachine {
+  isOn: boolean;
+  decisionLog: any[] = [];
+
+  constructor() {
+    // No init block defined
+  }
+
+  TurnOn() {
+    if (!(not this.isOn)) throw new Error('Guard failed: not this.isOn');
+    this.isOn = true;
+  }
+
+  TurnOff() {
+    if (!(this.isOn)) throw new Error('Guard failed: this.isOn');
+    this.isOn = false;
+  }
+
+
+
+
+}
diff --git a/out/ToggleSwitch.wat b/out/ToggleSwitch.wat
new file mode 100644
index 0000000..57cb5a1
--- /dev/null
+++ b/out/ToggleSwitch.wat
@@ -0,0 +1,71 @@
+;; Auto-generated by speckl-compile from ToggleSwitch
+;; Compile: wat2wasm ToggleSwitch.wat -o ToggleSwitch.wasm
+
+(module
+  ;; Host imports for Map/Set/alloc
+  (import "speckl" "map_create" (func $map_create (result i32)))
+  (import "speckl" "map_set" (func $map_set (param i32 i32 i32)))
+  (import "speckl" "map_get" (func $map_get (param i32 i32) (result i32)))
+  (import "speckl" "map_has" (func $map_has (param i32 i32) (result i32)))
+  (import "speckl" "map_remove" (func $map_remove (param i32 i32)))
+  (import "speckl" "set_create" (func $set_create (result i32)))
+  (import "speckl" "set_add" (func $set_add (param i32 i32)))
+  (import "speckl" "set_has" (func $set_has (param i32 i32) (result i32)))
+  (import "speckl" "set_size" (func $set_size (param i32) (result i32)))
+  (import "speckl" "alloc" (func $alloc (param i32) (result i32)))
+  (import "speckl" "write_i32" (func $write_i32 (param i32 i32)))
+  (import "speckl" "write_f64" (func $write_f64 (param i32 f64)))
+
+  ;; Linear memory (exported so host can read state)
+  (memory (export "memory") 1)
+
+  ;; State globals
+  (global $isOn (mut i32) (i32.const 0))
+
+  ;; ---- init ----
+  (func $init (export "init")
+    (i32.const 0)
+    (global.set $isOn)
+  )
+
+  ;; ---- Actions ----
+    ;; action: TurnOn
+  (func $TurnOn (export "TurnOn")  (result i32)
+    
+    ;; require: not isOn
+    ;; Complex guard not compiled: not isOn
+    ;; isOn := true
+    (i32.const 0) ;; uncompiled expr: true
+    (global.set $isOn)
+    (global.get $isOn)
+    (return)
+  )
+
+  ;; action: TurnOff
+  (func $TurnOff (export "TurnOff")  (result i32)
+    
+    ;; require: isOn
+    ;; Complex guard not compiled: isOn
+    ;; isOn := false
+    (i32.const 0) ;; uncompiled expr: false
+    (global.set $isOn)
+    (global.get $isOn)
+    (return)
+  )
+
+  ;; ---- getState ----
+  (func $getState (export "getState") (result i32 i32)
+    (i32.const 0)
+    (global.get $isOn)
+    (i32.store)
+    (i32.const 0)
+    (i32.const 4)
+  )
+
+  
+  ;; checkConstraints — runtime constraint evaluation stub
+  (func $checkConstraints (export "checkConstraints") (result i32)
+    ;; TODO: evaluate constraint expressions at runtime
+    (i32.const 1)
+  )
+)
\ No newline at end of file