Status: actively hardened, not formally proven. The ownership model prevents many classes of memory bugs by construction, and the full test suite is exercised under ASan (with leak detection disabled) and UBSan with zero errors. ASan validates invalid accesses, use-after-free, double-free, and buffer overflows — but not general leak freedom. Edge cases are still being found and fixed. This is not yet equivalent to a formally verified memory model.

Product version: 0.4.1.

Mako treats safety as a compiler and runtime contract, not a style guide. The goal: make memory corruption and common backend footguns hard to ship — by construction where possible, by hard errors where not.

Soundness program: SOUNDNESS.md · Memory model: MEMORY_MODEL.md.

1. Prevent, don't advise — illegal states should not compile or should abort with a clear diagnostic.
2. No GC — all packages stay on ownership, shares, and arenas for predictable latency. There is no collector mode that can weaken hold/share/move rules.
3. Secure defaults in the stdlib — parameterized DB APIs, header validation, constant-time token compare, and explicit secret wiping.
4. Speed is the name of the game — security features that cost cycles stay opt-in or debug-only; do not silently tax every release binary.

crew.kick(f(args…)) only accepts Send argument types: Copy scalars (including float and Uuid/ULID POD), deep-POD structs, string (heap-cloned), channels, ShareInt / AtomicInt (RC clone), locked handles (CMap / Mutex / RWMutex), and Option/Result/tuple of Send payloads (heap-boxed across spawn).
Rejected: arrays, maps, non-POD structs, Arena, nested Crew (examples/bad/kick_non_pod.mko, kick_array_arg.mko).

The compiler also analyzes every function value and lambda that crosses a kick boundary. Unsynchronized mutable captures are rejected, including captures hidden behind a function alias; unknown closure environments are rejected rather than guessed safe. fan mappers are required to be capture-free because their workers have no checked environment. Use Mutex/RWMutex/CMap/AtomicInt/ShareInt/channels for intentional shared state. The adversarial fixtures are examples/bad/kick_mutable_closure_capture.mko, kick_mutable_lambda_capture.mko, and fan_capture.mko. TSan remains a runtime smoke check (mako test --race) for the runtime and FFI boundary. Uuid is Copy — free re-read under hold, kick without move.

SMTP TLS: smtp_send_starttls uses SSL_connect. Set MAKO_SMTP_TLS_VERIFY=1 to enable peer certificate verification (SSL_VERIFY_PEER); default is off for dev soft paths.

Integer overflow leads to incorrect calculations, truncated values, and security vulnerabilities (e.g., buffer size calculations wrapping to small allocations). Mako provides two layers of protection:

Checked arithmetic functions return Result[int, string] on overflow:

match checked_add(a, b) {
    Ok(v) => use(v),
    Err(e) => log_error(e),
}

Compile-time overflow mode rewrites all +, -, * to abort on overflow:

mako build --overflow trap main.mko

Predicate functions let you test without performing the operation:

if would_overflow_mul(count, size) == 1 {
    return error("allocation too large")
}

Runtime: runtime/mako_overflow.h.

Mako includes a built-in leak detector for catching memory leaks in tests and during development. Scoped leak checking ensures that code under test frees everything it allocates:

fn TestNoLeaks() {
    leak_scope_enter()
    // ... code under test ...
    let leaked = leak_scope_exit()
    assert_eq(leaked, 0)
}

For detailed investigation, leak_bytes_since(mark) reports bytes allocated since a snapshot, and leak_report_json() produces structured output suitable for CI integration.

Runtime: runtime/mako_leak.h.

hold bindings move on rebind, into calls, and on full reads of non-Copy types. Use-after-move is a hard type error with a clear hint. See examples/bad/hold_use_after_move.mko and GUIDE § ownership.

let tok = secret_from_str(api_key)
// ... use ...
secret_drop(tok)   // explicit_bzero / memset_s / volatile wipe

Runtime: runtime/mako_security.h (MakoSecret, mako_secure_zero).

unsafe {
    let v = unsafe_index(xs, i)   // no debug bounds check — SAFETY: i in 0..len
}

Default indexing stays checked in both debug and release builds. unsafe_index is rejected unless it appears inside an explicit unsafe { } block. Use that escape only when you have proven the index is in range.

Writers reject CR/LF/NUL and illegal name tokens (http_header_ok, Content-Type in mako_http_reply_conn). Injection attempts fail closed.

• Unified sql_*: sql_exec / sql_query_int (int params), sql_exec_str4 / sql_query_str (string params), sql_query_rows / sql_query_rows_str (multi-row) bind placeholders — SQLite ?/$N, Postgres $N (with ? rewritten). Arg count must match placeholders.
• Legacy: sqlite_query_int / _params; pg_exec / pg_exec_params.
• Do not build SQL by string-concatenating user input.

if const_eq(got, want) == 1 { /* ok */ }
// alias: crypto_eq
if secret_eq_str(secret_from_str(token), presented) == 1 { /* ok */ }

Mako does not ship a full PKI product or “crypto framework.” It exposes building blocks so you implement protocols safely in Mako:

Secure defaults: TLS min 1.2; modern cipher suites; client verify and host name verification when using tls_client_new(ca) / https_*. Prefer Argon2id for new password storage. Use const_eq / secret_eq_str for tokens — never == on secrets in hot auth paths if you care about timing (language == is not constant-time).

Mako ships the RFC 5802 / 7677 crypto schedule, not a full SASL state machine. Applications (e.g. Postgres wire servers) own nonces, base64, and message framing.

pull "crypto"

// salt = base64_decode(wire_s); auth = bare + "," + server_first + "," + final_wo_proof
let salted = crypto.scram_salted_password(password, salt, iterations)
let stored = crypto.scram_stored_key(crypto.scram_client_key(salted))
if crypto.scram_verify_proof(stored, auth, client_proof) == 1 {
    let v = crypto.scram_server_signature(crypto.scram_server_key(salted), auth)
    // AuthenticationSASLFinal: "v=" + base64_encode(v)
}

API table: BUILTINS.md § SCRAM-SHA-256. Std recipe: STDLIB.md. Vector test: examples/testing/scram_test.mko. Channel-binding helpers: examples/testing/security_residuals_test.mko, security_product_test.mko.

AES-128-GCM with a random 12-byte nonce prepended (nonce || ct || tag):

Pack wrappers: crypto.seal / crypto.open. Test: security_residuals_test.

Process-local registry; pass the token over the wire for multi-node cancel:

Pack wrappers: crypto.tls.server_new_mtls / client_new_mtls / unique / server_reload / make_self_signed / make_csr; crypto.x509.* for PEM + cert lab; crypto.scram_tls_unique_c / scram_plus_final_bare.

Crypto core only: high-level SASL state machines (full AuthenticationSASL* framing, multi-round negotiation) stay application code — Mako ships digests, HMAC, PBKDF2, SCRAM schedule + channel-binding helpers, not a SASL framework.

Still out of scope (product): full CA/HSM/ACME product, WebPKI store beyond CA PEM paths, DTLS/WebRTC as first-class products.

Tests: security_test.mko, security_crypto_test.mko, password_hash_test.mko, bcrypt_test.mko, scram_test.mko, tls_aead_test.mko, tls_server_test.mko, crypto_srtp_blocks_test.mko, security_residuals_test.mko, security_product_test.mko.

Mako's session management, authentication, and authorization toolkit uses defense-in-depth to prevent common web security vulnerabilities.

Constant-time token-bearing checks. Cookie, CSRF, bearer, basic-header, and signed-token verification use const_eq internally, preventing timing side-channel attacks for those secret comparisons:

// All of these are constant-time by construction:
auth_session_cookie(cookie_hdr, "sid", expected)  // session cookie check
auth_check_bearer(auth_hdr, expected_token)       // bearer token check
auth_check_basic(auth_hdr, user, pass)            // basic auth check
auth_token_check(token, secret)                   // HMAC-SHA256 token verify
csrf_check(expected, submitted)                   // CSRF token verify

HttpOnly cookie defaults. cookie_make validates the name/value and always sets HttpOnly (prevents JavaScript access via document.cookie), SameSite=Lax (blocks cross-site POST requests from carrying the cookie), and Path=/. Invalid delimiter/control input fails closed.

Cryptographic session IDs. session_id_new uses mako_random_bytes (backed by the OS CSPRNG) to generate 16 random bytes, formatted as 32 hex characters. This provides 128 bits of entropy -- brute-force guessing is computationally infeasible.

CSRF token generation and verification. csrf_token generates a random token for embedding in forms or response headers. csrf_check verifies it with constant-time comparison. Combined with SameSite=Lax cookies, this provides layered CSRF protection.

Secret wiping. Signing keys used with auth_token_sign and API tokens can be stored via secret_from_str and explicitly zeroed with secret_drop. This prevents key material from persisting in freed memory:

let key = secret_from_str("my-hmac-key")
let token = auth_token_sign("user:42", "my-hmac-key")
// ... after use ...
secret_drop(key)   // zeroes memory via mako_secure_zero

HMAC-SHA256 signed tokens. auth_token_sign produces tokens in the form subject.signature using HMAC-SHA256. The signature is verified by auth_token_check in constant time. The subject can be extracted with auth_token_subject without verification (always verify first).

Runtime: runtime/mako_security.h (MakoSession, MakoCSRF, MakoAuth).

crew exit calls mako_nursery_cancel_join — cancel flag set, then all tasks joined. Cancellation is cooperative for already-running work; a blocked C/FFI call can delay the join. New kicks after cancel() do not start threads. Tests: examples/testing/cancel_policy_test.mko.

Mako has no tracing garbage collector in the compiler, generated C, runtime, or standard-library API. The ownership rules are therefore not a mode that can be weakened by package configuration. A legacy [package] gc = true setting is rejected, and removed gc_* calls are compile errors.

Fingerprints cover full safety-relevant inputs; NLL never skipped on a partial fingerprint. See BUILD.md.

A Result used as a bare statement is an error.

Debug and release (-O3 -flto -DNDEBUG): abort on OOB. Generated code defines MAKO_SAFE_DEFAULT. Explicit opt-out: unsafe / unsafe_index only.

Lexer/parser/type errors print file:line:col, caret, and help: hints.

Mako does not claim "memory safe like a proof assistant." It claims active prevention of the failures that hurt backends most: ignored errors, overruns, leaked tasks, use-after-move, header/SQL injection footguns — with ownership rules that every Mako package keeps.