Blog

By Topic

academia anecdote aosa book-reviews career
community conferences data-science diversity education
ethics favorite fiction humanities-writing humor
management noticed open-source opinion personal
politics programming proposal research retro
software-carpentry software-engineering student-projects technical-writing workshops

By Year

2020 2021 2022 2023 2024 2025 2026
2010 2011 2012 2013 2014 2015 2016 2017 2018 2019
2004 2005 2006 2007 2008 2009

Recent

Contracts in Frml

The first post in this series introduced Frml, a little procedural language I created so that I could learn how program verification works. The second explained how Frml checks simple scalar code; this one explains how it checks programs with multiple functions. As a reminder, the scalar prover owns the engine and leaves two hooks for higher levels:

def verify_function(self, fn):
    state = State()
    for p in fn.params:
        state.vars[p.name] = self._fresh_scalar(p.type, p.name)
    self._assume_spec(fn, state)
    end_states = self.exec_stmt_seq(fn.body, state)
    if fn.return_type is not None:
        if end_states:
            raise FrmlVerificationError(...)
    else:
        for s in end_states:
            self._check_ensures(fn, s, None)

_assume_spec and _check_ensures do nothing at the scalar level; the contracts prover overrides them:

class Prover(ScalarProver):
    def _assume_spec(self, fn, state):
        for req in fn.requires:
            state.path.append(self.eval_expr(req, state))
        if fn.decreases is not None:
            d = self.eval_expr(fn.decreases, state)
            self.entry_decreases = d
            self._emit(
                "decreases",
                f"decreases {fn.decreases.render()} >= 0",
                state.path,
                d >= 0,
                fn.decreases.pos,
            )

    def _check_ensures(self, fn, state, result):
        for ens in fn.ensures:
            self.check_postcondition(ens, state, result)

requires and ensures

Contracts are the source of most hypotheses and goals. At function entry, every requires clause is evaluated, the result is appended to the path, and later obligations may assume it. At every return, every ensures clause is evaluated, the result placeholder is replaced by the returned expression, and the result becomes a goal checked against the current path. Multiple requires clauses are and’ed, one fact per clause in the path, and multiple ensures clauses produce one obligation per clause. For example:

fn max(a: Int, b: Int) -> Int
  ensures result >= a
  ensures result >= b
  ensures result == a or result == b
{
  if a >= b {
    return a;
  } else {
    return b;
  }
}

The if produces two end states, and there are three ensures clauses, so there are six postcondition obligations, three per branch. The if branch goals are a >= a, a >= b, and a == a or a == b; the else branch goals are b >= a, b >= b, and b == a or b == b. Each is proved with the appropriate branch condition in the path.

check_postcondition turns an ensures clause into one obligation:

def check_postcondition(self, ens, state, result):
    goal = self.eval_expr(ens, state, result_term=result)
    self._emit("postcondition", ens.render(), state.path, goal, ens.pos)

result_term supplies the term that result denotes inside the clause.

A Complete Trace

Let’s trace a tiny function through the whole machine:

fn double(x: Int) -> Int
  ensures result == x + x
{
  return x + x;
}

fn main() -> Int
{
  return double(4);
}
  1. verify_program builds the Prover and calls verify().
  2. verify() sets current_fn = double and calls verify_function(double).
  3. verify_function builds the entry state:
    • state.vars["x"] = Int("x!1"): a fresh integer symbol.
    • state.old_vars["x"] = Int("x!1"): the old(...) snapshot.
    • No requires, no decreases, so _assume_spec leaves the path [].
  4. exec_stmt_seq([return x + x], state) starts with states = [state].
  5. The single statement is return x + x, so exec_stmt calls visit_StmtReturn.
  6. eval_rhs(x + x, state) falls through to eval_expr(x + x, state):
    • visit_ExprBinary sees the operator +.
    • The left x becomes Int("x!1"); the right x becomes Int("x!1").
    • It returns the Z3 term x!1 + x!1.
  7. Back in visit_StmtReturn, value = x!1 + x!1.
  8. _check_ensures runs for the single ensures result == x + x:
    • It calls check_postcondition, which evaluates result == x + x with result_term = x!1 + x!1.
    • result looks up result_term, giving x!1 + x!1.
    • Each x looks up state.vars["x"], giving x!1.
    • The goal is the Z3 term (x!1 + x!1) == (x!1 + x!1).
    • One obligation is emitted with the empty path [].
  9. visit_StmtReturn returns [], so states becomes [] and the loop breaks.
  10. end_states == []; double has a return type and no fall-through path, so no error is raised.
  11. verify() records ProverResult("double", [the one obligation]).
  12. verify_program hands the obligation to check_obligations, which asks Z3 to refute not (True => (x!1 + x!1) == (x!1 + x!1)). No value of x!1 makes it true, so Z3 answers unsat and the obligation is VERIFIED.

old(...)

old(e) means “the value of e at the moment the function was entered”. The prover snapshots parameters at entry into old_vars; inside an ensures clause, old(x) reads that snapshot rather than the current value. For example:

fn bump(x: Int) -> Int
  ensures result == old(x) + 1
{
  x = x + 1;
  return x;
}

At entry, x is a fresh integer symbol x!1, and old_vars["x"] keeps that original x!1. After the assignment, state.vars["x"] is the term x!1 + 1, so x in the postcondition reads the updated value while old(x) reads the original x!1. The emitted postcondition goal looks like:

x!1 + 1 == x!1 + 1

Both sides are the same term, so Z3 proves it.

Function Calls

When one function calls another, the prover uses the callee’s contract. For a statement call f(args), the prover proves the callee’s requires clauses under the caller’s current path, assumes the callee’s ensures clauses, and adds those assumptions to the caller’s path. The caller never sees the callee’s body; it only sees the callee’s contract. For example:

fn inc(x: Int) -> Int
  requires x >= 0
  ensures result == x + 1
{ return x + 1; }

fn main() -> Int
{
  return inc(41);
}

For the call inc(41), the prover emits a precondition obligation 41 >= 0, creates a fresh result inc_result!N, and assumes inc_result!N == 41 + 1. main returns that result, and the postcondition is proved.

Recursion

Recursive functions need a decreases clause. At function entry, _assume_spec emits decreases >= 0. For factorial, that is n >= 0, proved from requires n >= 0. At a recursive call, the callee’s requires clauses are proved at the call site. For factorial(n - 1), the prover proves n - 1 >= 0.

model_call emits decreases_at_call < decreases_at_entry for a self-call. This applies to statement calls; for scalar self-calls inside expressions, such as the recursive call in factorial below, the current implementation proves the callee’s precondition but does not emit the strict-decrease obligation.

fn factorial(n: Int) -> Int
  requires n >= 0
  ensures result >= 1
  decreases n
{
  if n == 0 {
    return 1;
  } else {
    return n * factorial(n - 1);
  }
}

The prover emits four obligations: n >= 0 for the entry decreases n >= 0, 1 >= 1 for the base-case postcondition, n - 1 >= 0 for the recursive call’s precondition, and n * factorial_result >= 1 for the recursive postcondition.

Quantifiers

Frml supports forall and exists in specifications:

forall i: Int :: 0 <= i and i < 3 => i >= 0

The prover translates these to Z3 quantifiers: forall becomes z3.ForAll([var], body) and exists becomes z3.Exists([var], body). The quantified variable becomes a fresh symbol, and the body is evaluated with that variable added to the state. In the example above, the variable i becomes a fresh symbol added to the state, the body becomes the Z3 term Implies(And(0 <= i, i < 3), i >= 0), and the whole quantifier becomes z3.ForAll([i], body).

Similarly, if exists was used, the variable i would again become a fresh symbol, the body would become And(0 <= i, i < 3, i == 2), and the whole quantifier would become z3.Exists([i], body). Both forms can appear in an ensures clause:

fn f() -> Bool
  ensures result == (forall i: Int :: 0 <= i and i < 3 => i >= 0)
{ return true; }

fn g() -> Bool
  ensures result == (exists i: Int :: 0 <= i and i < 3 and i == 2)
{ return true; }

Anniversary Thoughts

Coming up on the anniversary of being laid off, I’m thinking about what I’d like to do differently in year 2:

  1. Find people in the east end of Toronto who want to play some jazz once a week. I’m currently commuting to the west end to do that: I enjoy playing, but the travel time is wearying. If you’re interested, I’m easy to reach.

  2. Find a small F&SF writers’ group, also in the east end, to swap crits with. I’m currently getting great feedback from a friend, but would like more perspectives and an excuse to drink coffee. (Scribophile has been moderately useful, Wattpad hardly at all.) Again, if you’re interested, please reach out.

  3. Go on long bike rides. A friend has been going on 50km+ rides this year; it’ll take me a long time (and probably a new bike) to get up to that, but it’s a shame not to be out on sunny days like today.

  4. Teach something that I’m interested in learning myself. I built a discrete event simulation framework last winter, and a little formal verifier this summer, with an eye to building lessons on top of them, but no-one seemed interested. The organizational change and project closure workshops have had a bit more traction, but aren’t about programming, and SDGC is stalled.

  5. I started working on CATMAID a few weeks ago; between teaching and other commitments I haven’t been able to immerse myself yet, but I’m hoping to do that in November. On the upside, fixing bugs in software that scientists use is pretty rewarding. On the other hand, it’s all remote work, and I miss being able to grab a cup of coffee with colleagues in person.

  6. Over (almost) 12 months I sent more than 60 job applications, which led to four interviews and three offers (one of which I now wish I’d taken). I don’t think I’m going to send CVs to people I don’t know any more, but if something interesting comes up in Toronto, see the note above about coffee with colleagues.

  7. I’m using Jon Udell’s Bram to experiment with AI coding, mostly so that I won’t just be recycling other people’s talking points in discussions about the subject. I expect I’ll keep doing this, and hope to start contributing to the tool itself.

  8. I’ve nominated myself for a seat on the Carpentries board. I dithered about this for a long time, but in the end decided that I’d regret not doing it. Let’s see how the voting goes…

  9. I’d like to run some undergraduate projects next semester. I have students lined up for one of the games, but am still looking for people for the others. As always, please reach out if you’re interested (or if you have students who might be).

  10. Most of all, I’d like to be happier in the coming year than I have been in the one gone past. Losing my job just a few weeks after my daughter left home for university put me in a tailspin. I’ve dealt with depression off and on for years; the last twelve months weren’t as bad as some dips, but the trough has lasted longer. Let’s see what the next year brings.

Scalar Code in Frml

The first post in this series introduced Frml, a little procedural language I created so that I could learn how program verification works. This post explains how Frml checks scalar-level programs that have straight-line and branching code over scalar values with no function calls, contracts, loops, or quantifiers.

The Prover’s Data Model

The prover tracks a program point with a State object. State.vars holds the symbolic values of scalar variables, and State.path holds every fact assumed to hold so far. The prover never stores concrete numbers in variables; it stores Z3 formulas about numbers. For example, x might hold the symbolic integer x!1 rather than the number 5, where x!1 means “the first fresh symbol named x”.

An Obligation records one claim to prove. Its kind can be assert or division at this level, its description is the human readable text of the claim, hyp is the list of hypothesis terms, goal is the goal term, and pos is the source position of the claim (shown in --trace output).

Fresh Names

The prover keeps a counter and calls _fresh(name) to get name!N with an increasing N, so x!1, x!2, and x!3 are different symbols even though they all relate to the source variable x. This matters because when x is reassigned, the old x!1 is not overwritten; the new value becomes a new symbol such as x!5, which keeps the symbolic execution correct. For example, after the statement:

x = x + 1;

the state maps x to the term x!1 + 1, not to a number.

Operation

The prover works in two phases: it generates obligations by walking the AST and collecting Obligation objects, then checks them by handing each obligation to Z3 and turning the answers into outcomes. verify() is the generation phase for the whole program:

def verify(self):
    results = []
    for fn in self.program.functions:
        self.obligations = []
        self.current_fn = fn
        self.verify_function(fn)
        results.append(ProverResult(fn.name, self.obligations))
    self.obligations = []
    return results

verify verifies one function at a time in source order; self.obligations is reset per function so obligations stay grouped by function. verify_function() handles one function:

def verify_function(self, fn):
    state = State()

    # Entry state: fresh constants for the parameters.
    for p in fn.params:
        state.vars[p.name] = self._fresh_scalar(p.type, p.name)

    # Snapshot for `old(...)` (unused at this level; higher levels read it).
    state.old_vars = dict(state.vars)

    self._assume_spec(fn, state)

    # Run the body.  Surviving states reached the end without `return`; for
    # a value-returning function that is an error.
    end_states = self.exec_stmt_seq(fn.body, state)
    if fn.return_type is not None:
        if end_states:
            raise FrmlVerificationError(
                f"function {fn.name!r} has a path that does not return", fn.pos
            )
    else:
        for s in end_states:
            self._check_ensures(fn, s, None)

_assume_spec and _check_ensures do nothing at this language level because there are no requires, ensures, or decreases clauses, so the entry path is empty and the body’s fall-through is simply checked. exec_stmt_seq returns the states of paths that fell off the end of the body. A return produces no end state (see below), so if a value-returning function has any end state, some path never returned, which is an error.

Statements

Statements are handled by three related methods:

def exec_stmt_seq(self, stmts, state):
    states = [state]
    for stmt in stmts:
        new_states = []
        for s in states:
            new_states.extend(self.exec_stmt(stmt, s))
        states = new_states
        if not states:
            break
    return states


def exec_block(self, stmts, state):
    before_vars = set(state.vars)
    states = self.exec_stmt_seq(stmts, state)
    for s in states:
        for name in list(s.vars):
            if name not in before_vars:
                del s.vars[name]
    return states


def exec_stmt(self, stmt, state):
    return stmt.accept(self, state)

In exec_stmt_seq, states is the set of live paths, starting with the single entry state, and each statement maps every live state to zero or more successor states (see below). exec_stmt calls stmt.accept(self, state), which dispatches to visit_StmtAssign, visit_StmtIf, visit_StmtLet, and so on. The “zero or more” matters because of return:

def visit_StmtReturn(self, stmt, state):
    value, state = self.eval_rhs(stmt.expr, state)
    self._check_ensures(self.current_fn, state, value)
    return []

A return returns the empty list. new_states.extend([]) adds nothing, so that path is dropped from states; execution stops there, exactly as it does at run time. This is also what makes the verify_function fall-through check work, since only paths that reach the end of the body survive in end_states.

exec_block is exec_stmt_seq plus scoping. After a nested block (i.e., an if body) runs, any variables introduced inside it are deleted from the resulting states, so local declarations do not leak outward.

Expressions

Expressions use the same visitor pattern as statements:

def eval_expr(self, expr, state, *, use_old=False, result_term=None):
    return expr.accept(self, state, use_old=use_old, result_term=result_term)

expr.accept(...) calls visit_ExprBinary, visit_ExprVar, and so on. Each visitor returns a Z3 term. eval_expr never actually computes anything; as noted above, it translates a Frml expression into the Z3 formula that describes it using the current symbolic state.

A Complete Trace

Let’s trace a complete verification:

fn main() -> Int
{
  let x: Int = 3;
  assert x > 0;
  return 0;
}
  1. verify_program builds the ScalarProver and calls verify().
  2. verify() sets current_fn = main and calls verify_function(main).
  3. verify_function builds the entry state: state.vars is empty (no parameters), and the path is empty.
  4. exec_stmt_seq([let, assert, return], state) starts with states = [state].
  5. let x: Int = 3; evaluates the literal 3 and stores it in state.vars["x"] as the Z3 integer 3 (not a fresh symbol).
  6. At assert x > 0;, the prover evaluates the assertion expression:
    • x looks up the stored term 3.
    • > builds the Z3 term 3 > 0.
  7. The prover emits one obligation:
    • kind: assert
    • description: assert (x > 0)
    • hypotheses: the current path (empty here)
    • goal: 3 > 0
  8. return 0 drops the path, so end_states is empty and no error is raised.
  9. verify() records ProverResult("main", [the one obligation]).
  10. verify_program hands the obligation to check_obligations, which builds the claim not (True => 3 > 0) and asks Z3 to satisfy it (see “The Z3 check loop” below).
  11. Z3 finds no assignment that makes not (3 > 0) true, so it returns unsat, and the obligation is VERIFIED.

uv run frml check --trace examples/scalar/ex01_assign_then_assert.frml prints:

fn main
--- assert:4:3: assert (x > 0)
    prove: (> 3 0)
    => VERIFIED
VERIFIED

Translating expressions to Z3

eval_expr maps each Frml expression node to a Z3 term.

Division by zero is undefined, the verifier turns it into another proof obligation. n the prover evaluates a / b or a % b, it first emits:

hypotheses:  current path
goal:        b != 0

and then returns the Z3 division or modulo term. For example:

fn main() -> Int
{
  let x: Int = 10;
  let y: Int = 2;
  if y != 0 {
    assert x / y == 5;
  }
  return 0;
}

The if y != 0 guard puts y != 0 on the path before the division. The division emits y != 0, which the path already contains, so Z3 proves it immediately.

Branching

A conditional statement forks the symbolic execution. The condition is evaluated once, then the then branch continues with the condition added to the path, while the else branch continues with not condition added to the path. (If there is no else, the fall-through branch still gets not condition.)

The prover tracks a list of states, one per path through the code. Here is the code that does the forking:

def visit_StmtIf(self, stmt, state):
    cond, state = self.eval_rhs(stmt.cond, state)
    then_state = state.copy()
    then_state.path.append(cond)
    then_ends = self.exec_block(stmt.then, then_state)
    ends = list(then_ends)
    if stmt.else_ is not None:
        else_state = state.copy()
        else_state.path.append(z3.Not(cond))
        ends.extend(self.exec_block(stmt.else_, else_state))
    else:
        else_state = state.copy()
        else_state.path.append(z3.Not(cond))
        ends.append(else_state)
    return ends

assert

An assert statement produces a goal from the current path:

assert 1 < 2;

The prover evaluates the condition, emits an obligation with the current path as hypotheses and the condition as goal, and if Z3 proves it, execution continues with the fact now guaranteed.

The prover does not add the assertion to the path after checking because assert is a check, not an assumption. The programmer asserts what should already be true, so the verifier must prove it from what came before.

The Z3 Check Loop

check_obligations is where Z3 is actually called:

solver = z3.Solver()
solver.set(timeout=timeout_ms)

for ob in obligations:
    solver.push()
    hyp = z3.And(*ob.hyp) if ob.hyp else z3.BoolVal(True)
    solver.add(z3.Not(z3.Implies(hyp, ob.goal)))
    result = solver.check()

    if result == z3.unsat:
        -> VERIFIED
    elif result == z3.sat:
        -> FAILED with the counterexample model
    else:
        -> UNKNOWN

    solver.pop()

Each obligation gets a fresh solver context via push and pop. The empty hypothesis list becomes True. With no hypotheses, the claim is goal alone, i.e. True => goal. The code writes z3.BoolVal(True) so z3.And(*ob.hyp) always has a value, because Z3’s And() is not defined over an empty argument list. Z3 is asked to satisfy not (hyp => goal). unsat means the claim holds, sat means a counterexample exists, and anything else is unknown.

Introducing Frml

A few months ago I set out to learn how program verification works. I tried Lean and Dafny, but kept wondering how verification actually worked. To find out, DeepSeek and I built Frml, which is a very simple imperative language with its own verifier.

This post walks through the Frml verification engine, explaining how a Frml program becomes Boolean logic that the Z3 solver can check, and what Z3 does with that logic. The language and its verifier are layered: the scalar level handles straight-line and branching code with no functions or loops, while successive levels add features one by one.

Frml is aimed at experienced programmers: you should understand basic Boolean logic (and, or, not, implication) and already know what a lexer, parser, and abstract syntax tree (AST) are, but you need no prior background in formal verification.

The big picture

Frml’s lexer and parser turn program text into an AST, and the typechecker rejects programs with type errors. The prover then turns the AST into verification conditions of the form:

hypotheses => goal

The prover asks Z3 to confirm every verification condition, and if Z3 confirms all of them, the program is verified.

OK, so what’s a verifier? To start, a proof obligation is a claim:

from these hypotheses, this goal always follows

Symbolically:

h1 and h2 and ... and hn  =>  goal

The h1 ... hn are facts known at some point in the program, and goal is a fact that must hold at that point. Example claims from a real program are “knowing x >= 0, prove 0 <= x”, “knowing i < n, prove i + 1 <= n”, and “knowing nothing, prove x > x”, where the last one is false. The prover’s job is to produce claims in this shape.

What Z3 is and what it does

Z3 is an SMT solver, where SMT means Satisfiability Modulo Theories. It knows the theory of integers, arrays, strings, and Boolean logic. A formula is satisfiable when some assignment of values to its variables makes it true. Given a formula, Z3 returns one of three answers: sat, meaning a satisfying assignment exists and Z3 can show you one; unsat, meaning no satisfying assignment exists; or unknown, meaning Z3 gave up or timed out. An example that can be satisfied:

formula:  x > 3 and x < 5
answer:   sat          (x = 4 works)

An example that cannot:

formula:  x > 3 and x < 4
answer:   unsat        (no integer fits)

From “is it valid?” to “is it unsatisfiable?”

The prover wants to prove that hypotheses => goal is valid, meaning true for every possible assignment of the variables. Z3 does not directly check validity; it checks satisfiability. The two are connected, because A => B is valid exactly when not (A => B) is unsatisfiable. So the prover asks Z3 about:

not (hypotheses => goal)

If Z3 says unsat, then no counterexample exists, so the goal is proved. If Z3 says sat, it found a counterexample, so the goal is false. If Z3 says unknown, the proof is inconclusive. That is the entire proof mechanism, and everything else is just building the hypotheses and goals, for a rather large value of “just”.

Z3 in Python

The package manager lesson in Software Design by Example used Z3 to find compatible versions of packages. Here’s a simple example of its use:

from z3 import Bool, Solver

A = Bool("A")
B = Bool("B")
C = Bool("C")

A, B, and C do not have specific values. Each instead represents the set of possible Boolean values, so we can specify constraints like A == B.

solver = Solver()
solver.add(A == B)
solver.add(B == C)
report("A == B & B == C", solver.check())

We can then ask Z3 to find a model that satisfies those constraints:

A == B & B == C: sat
A False
B False
C False

To see unsatisfiability, require A to equal B and B to equal C but A and C to be unequal:

A = Bool("A")
B = Bool("B")
C = Bool("C")
solver = Solver()
solver.add(A == B)
solver.add(B == C)
solver.add(A != C)
report("A == B & B == C & B != C", solver.check())

A == B & B == C & B != C: unsat

The next post in this series will show how Frml builds proof obligations for simple programs that manipulate scalar variables without loops or conditionals.

Heroes and Villains

Earlier this week I asked a question on Mastodon: “Who are the Jane Goodalls and David Attenboroughs of software?” Goodall was a primatologist best known for decades of research on chimpanzees, and Attenborough has been making nature documentaries longer than I’ve been alive. Both are well-known to the general public (at least in the English speaking world) and have been powerful forces for good.

Which means that the answer to my question is, “We don’t have any.” If you ask someone who isn’t in tech to name people who are, they will say Gates or Musk or Zuckerberg. They know our corporate super-villains, not the people who have been trying to make the world a better place. It’s as if the only people you knew who had something to do with the environment were the presidents of oil companies, none of whom I could name without doing an online search.

I don’t know why this is, how to change it, or whether changing it would matter. Now that I’ve noticed it, though, I can’t stop thinking about it. If there’s someone outside the Anglosphere who fits the bill, I’d be grateful for a pointer.

12 Tips for Making Your Startup Fail

Mission-driven startups fail in predictable ways every year because good intentions are no substitute for a theory of change, money, and community involvement. As I found out the hard way, “At least we’re trying to do good” is the most dangerous sentence in social entrepreneurship, because it lets founders skip the boring, specific work that decides whether a venture actually helps anyone. I wrote the first version of this almost twenty years ago for undergraduate students starting their first socially-conscious nonprofit or mission-driven company. I hope this update is still useful, and would welcome feedback.

Tip 1: Fall in love with your mission, not the actual problem.

Tip 2: Assume that good intentions guarantee good outcomes.

Tip 3: Choose a team that shares your passion and nothing else.

Tip 4: Treat the people you serve as an afterthought.

Tip 5: Never charge, because it’s a good cause.

Tip 6: Measure what’s easy and flattering.

Tip 7: Chase the grant money wherever it leads.

Tip 8: Ignore every organization already working on this.

Tip 9: Skip the boring structure and compliance.

Tip 10: Believe a well-meaning app can fix a structural problem.

Tip 11: Let moral weight burn you out.

Tip 12: Never learn to sell, because selling is for profiteers.

Actually…

Every one of these is a documented way socially-conscious ventures actually die. Reverse the list and you have the real advice:

  1. Fall in love with the problem the community names, and design with them, not for them.
  2. Build a theory of change and study what’s already been tried.
  3. Assemble complementary skills, and include people with lived experience of the problem.
  4. Serve the people you’re helping first; let funders follow.
  5. Earn revenue or build durable funding so the mission outlives the grant.
  6. Measure outcomes, honestly, with a baseline.
  7. Let the mission drive funding, not the other way around.
  8. Map the ecosystem and partner rather than duplicate.
  9. Choose the right legal form and take safeguarding and compliance seriously.
  10. Attack root causes and respect the systems you’re working within.
  11. Protect your own sustainability — a burned-out founder helps no one.
  12. Learn to fundraise, build a real board, and make the organization outlast you.

Student Projects

Autumn always makes me feel like I ought to be back in school, either to learn or to teach. In turn, that makes me think about student projects I would like to run.

Tools

Bram
Bram (“Bram runs agents mindfully”) is a desktop app that embeds Claude Code and Codex in a GUI that provides structured, audited workflows. This project will add several new features, including support for other families of models such as DeepSeek.
A Little Program Verifier
Where the previous project would build a simple editor, this project would build a verifier for a very simple programming language in order to teach people how those tools work. (See here for preliminary work.)
XKCD Charts
Chart.xkcd creates charts in the hand-drawn style of XKCD. This project will fix outstanding issues, add new features such as axis limits and stable coloring schemes, and create wrappers in one or both of Gleam or Dafny.
An I/O Library for Dafny
I want to translate Software Design by Example in Python into Dafny to see and show how verifiability changes the way we build software tools, but Dafny’s I/O and systems programming libraries don’t offer what the examples need. This project will build those libraries, starting with what’s listed in this blog post.

Games

Stardew Valley Murders
A mod that turns Stardew Valley into a murder mystery game. Grow vegetables, then trade them for gossip and clues until you figure out who murdered Clint and why.
This project now has a team for Winter 2027.
Rewind
A first-person shooter with a science-fiction theme in which each player has a limited “temporal battery” that can be spent to reverse the flow of time by a few seconds. If you just got shot, rewind and take cover instead; if you missed a shot, rewind and aim lower. The twist is that your opponent knows you can do this, turning every rewind into a battle of wits.
Save the Humans!
The zombies have attacked. The people at the zoo have panicked, and it’s up to the animals to save them in this tongue-in-cheek game. The tiger can chase people away from danger, but they might run straight into the arms of the ravenous horde. The bunny is so cute that people will chase it, but if they catch it they’ll just stand there petting it until they’re eaten, and so on.
Tower Support Game
A tower defense game is one in which the player builds fixed defenses against incoming waves of attackers. The objective of this game is to prototype a simple tower support game, in which the player builds bridges, first aid stations, and so on to help travelers reach their destination.

IO for Software Design

Last winter I wrote a discrete event simulation framework in Python to keep myself busy, have something to put on my CV, experiment with LLM-assisted coding, and learn how async and await actually work. Over the summer, for similar reasons, I played around a bit with Lean and Gleam, thinking that I might translate the Software Design by Example books from JavaScript and Python into one or the other. Lean defeated me, and I quickly grew frustrated with the gaps in Gleam’s standard library, but my noodling around left me wanting to learn more about formal verification of programs.

After poking around a bit I decided to give Dafny a try, only to find that its standard library has gaps too. Depending on whether or not I’m able to find work, I might try to recruit some undergrads to fill those in. What follows is a spec for what I would need them to build in order to be able to replicate the examples in the existing books.

In brief: Dafny’s standard library provides only whole-file I/O (Std.FileIO) and JSON (Std.JSON). Std.FileIO reads or writes an entire file in a single call; there are no functions to open and close file handles and no streaming reads. It also has no networking, hashing, SQLite, CSV/YAML, temporary-file, or path-manipulation support.