Tsubasa — OA / Hackathon Judging System
Tsubasa is an online assessment and hackathon judging system. The contest runs for two hours, and all candidates compete at the same time. The design assumes that every candidate uses an agentic AI, so submitted code is no longer evidence of understanding. The system scores the judgement of the candidate instead. A candidate predicts how the code behaves and declares a confidence value, and the platform executes the reference implementation to get the ground truth. The authoring method is the main innovation. A bug is not N bugs in N code bases. A bug is one perturbation of a formal specification, written in IMP with bounded loops and machine integers. The tool then decides equivalence between the original program and the mutant by exhaustive evaluation over a declared domain. Difficulty becomes a computed number, and cross-language fairness becomes a machine-checked assertion. The scoring rules and the offline authoring tools work today, and the contest platform is under implementation.
Highlights
- A bug is a perturbation of a specification. Each item has one IMP specification, and five operator classes rewrite the syntax to enumerate all candidate bugs: relational, arithmetic, logical, constant offset, and call removal. No generative model takes part.
- The tool decides equivalence, and does not estimate it. For the paging item, exhaustive evaluation covers a declared domain of 14,322 points in less than one second. The domain is printed on the item, so a candidate can repeat the decision. This is the answer to an appeal in a contest that has no human grading.
- Equivalent mutants become the items with the highest discrimination. A candidate who only reads the difference answers that the behaviour changes. A candidate who understands the semantics answers that the two programs are equivalent on the declared domain. The confidence score rewards the second answer.
- The tool computes the difficulty of each perturbation from the differential rate, the minimal witness size, and the number of public tests that kill it. A rate of 5 to 20 percent makes a debug item. A rate of 0 percent makes an equivalence question. A rate above 30 percent is too easy.
- Bounded exhaustive verification has a known limit, which Marinov et al. show with a SearchTree mutant. Each item therefore includes a stability log. The tool decides equivalence again on a larger domain, and no decision may change. A fixture that holds the known counterexample proves that the check still works. The tool also groups the mutants by output vector and removes the duplicates.
- Cross-language fairness is a machine-checked property. One emitter and one syntax table of approximately 30 lines per language generate the code. An assertion then compares each generated language with the reference interpreter at every point of the domain. An item ships only after this comparison passes. Python, TypeScript, and Rust pass today. The IR fixes the semantics of truncating division, modulo sign, slice clamping, and integer width, so the languages cannot disagree.
- No person grades the contest, and the scores use proper scoring rules instead of raw accuracy. The Brier skill score measures the declared confidence. The d-prime measure scores defect detection on a corpus that also holds clean samples. The Spearman rho measures how well a candidate ranks competing AI implementations by readiness.
- Budgets are the strongest constraint against an agent. A token bucket limits judge submissions to three, and adds one submission every fifteen minutes. A candidate also gets one guess of the line number, three bisect queries, and a hard limit on the size of the difference. The same budget shapes the traffic to the judge machines.
- The judging backend uses Rust and Hotaru. A Postgres queue with SKIP LOCKED holds the jobs, and one binary runs as the web server or as the worker. The runners are sandboxed and stay separate from the web tier. The submission id keys the score, so a retry cannot count twice.